20120126 
Helmut Grohne  started proving lemma2

commit  commitdiff  tree 
20120126 
Helmut Grohne  reduce imports to speed up agdamode

commit  commitdiff  tree 
20120126 
Helmut Grohne  split Bidir.agda to FinMap.agda

commit  commitdiff  tree 
20120126 
Helmut Grohne  improve readability using spaces

commit  commitdiff  tree 
20120126 
Helmut Grohne  reduce usage of sym

commit  commitdiff  tree 
20120126 
Helmut Grohne  open \==Reasoning at top level

commit  commitdiff  tree 
20120126 
Helmut Grohne  prove the remaining parts of lemmacheckInsertgenerate

commit  commitdiff  tree 
20120126 
Helmut Grohne  complete the yes part of lemmacheckInsertgenerate...

commit  commitdiff  tree 
20120126 
Helmut Grohne  change lemmainsertsame to work with \== proofs

commit  commitdiff  tree 
20120123 
Helmut Grohne  base case of lemma2

commit  commitdiff  tree 
20120123 
Helmut Grohne  rewrite lemma1 using propositional equality

commit  commitdiff  tree 
20120122 
Helmut Grohne  actually fmap is what I meant instead of >>=

commit  commitdiff  tree 
20120122 
Helmut Grohne  introduce >>= on Maybe to improve readability

commit  commitdiff  tree 
20120122 
Helmut Grohne  improve readability by introducing EqInst

commit  commitdiff  tree 
20120122 
Helmut Grohne  formulate theorem1

commit  commitdiff  tree 
20120122 
Helmut Grohne  formulate lemma2

commit  commitdiff  tree 
20120122 
Helmut Grohne  attempt to prove lemma1

commit  commitdiff  tree 
20120121 
Helmut Grohne  rewrite generate using zip and fromAscList

commit  commitdiff  tree 
20120121 
Helmut Grohne  split FinMap to FinMapMaybe

commit  commitdiff  tree 
20120119 
Helmut Grohne  replaced NatMap with FinMap

commit  commitdiff  tree 
20120119 
Helmut Grohne  first attempt to define bff (with holes)

commit  commitdiff  tree 
20120119 
Helmut Grohne  employ standard library of agda where possible

commit  commitdiff  tree 
20120119 
Helmut Grohne  first attempt to model lemma1

commit  commitdiff  tree 
20120119 
Helmut Grohne  added .gitignore

commit  commitdiff  tree 
