20120209 
Helmut Grohne  formulate theorem2 
blob  commitdiff 
20120209 
Helmut Grohne  prove lemmauniongenerate 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  prove theorem1 assuming a lemmauniongenerate 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  started proving theorem1 
blob  commitdiff  diff to current 
20120209 
Helmut Grohne  introduce denumerate 
blob  commitdiff  diff to current 
20120131 
Helmut Grohne  replace idrange with enumerate 
blob  commitdiff  diff to current 
20120131 
Helmut Grohne  postulate free theorem for List a > List a 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  recursion of lemma2 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  started proving lemma2 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  reduce imports to speed up agdamode 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  split Bidir.agda to FinMap.agda 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  improve readability using spaces 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  reduce usage of sym 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  open \==Reasoning at top level 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  prove the remaining parts of lemmacheckInsertgenerate 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  complete the yes part of lemmacheckInsertgenerate... 
blob  commitdiff  diff to current 
20120126 
Helmut Grohne  change lemmainsertsame to work with \== proofs 
blob  commitdiff  diff to current 
20120123 
Helmut Grohne  base case of lemma2 
blob  commitdiff  diff to current 
20120123 
Helmut Grohne  rewrite lemma1 using propositional equality 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  actually fmap is what I meant instead of >>= 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  introduce >>= on Maybe to improve readability 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  improve readability by introducing EqInst 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  formulate theorem1 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  formulate lemma2 
blob  commitdiff  diff to current 
20120122 
Helmut Grohne  attempt to prove lemma1 
blob  commitdiff  diff to current 
20120121 
Helmut Grohne  rewrite generate using zip and fromAscList 
blob  commitdiff  diff to current 
20120121 
Helmut Grohne  split FinMap to FinMapMaybe 
blob  commitdiff  diff to current 
20120119 
Helmut Grohne  replaced NatMap with FinMap 
blob  commitdiff  diff to current 
20120119 
Helmut Grohne  first attempt to define bff (with holes) 
blob  commitdiff  diff to current 
20120119 
Helmut Grohne  employ standard library of agda where possible 
blob  commitdiff  diff to current 
20120119 
Helmut Grohne  first attempt to model lemma1 
blob  commitdiff  diff to current 
