20120914 
Helmut Grohne  employ rewrite in lemmamaplookupMassoc

commit  commitdiff  tree 
20120914 
Helmut Grohne  \::subst is a special case of substcong

commit  commitdiff  tree 
20120914 
Helmut Grohne  veclenvialist and lengthtoList are the same

commit  commitdiff  tree 
20120914 
Helmut Grohne  complete missing parts of LiftGet

commit  commitdiff  tree 
20120911 
Helmut Grohne  show fromListtoList in the subst form

commit  commitdiff  tree 
20120911 
Helmut Grohne  LiftGet: replace veclengthsame with toListsubst

commit  commitdiff  tree 
20120910 
Helmut Grohne  LiftGet: veclength is also known as subst (Vec A)

commit  commitdiff  tree 
20120904 
Helmut Grohne  formulate List <> Vec isomorphism problems

commit  commitdiff  tree 
20120830 
Helmut Grohne  prove LiftGet.gettrafo2getlen

commit  commitdiff  tree 
20120830 
Helmut Grohne  phrase other half of bijection in LiftGet

commit  commitdiff  tree 
20120830 
Helmut Grohne  prove half of the bijection in LiftGet

commit  commitdiff  tree 
20120830 
Helmut Grohne  give the type of different gets a name

commit  commitdiff  tree 
20120806 
Helmut Grohne  attempt isomorphism between get on List and on Vec

commit  commitdiff  tree 
20120619 
Helmut Grohne  third definition of bff

commit  commitdiff  tree 
20120605 
Helmut Grohne  make the Vec bff more similar to the List version

commit  commitdiff  tree 
20120605 
Helmut Grohne  define a bff over Vec

commit  commitdiff  tree 
20120605 
Helmut Grohne  move bff and friends to submodule ListBFF

commit  commitdiff  tree 
20120605 
Helmut Grohne  move checkInsert and related properties to CheckInsert...

commit  commitdiff  tree 
20120427 
Helmut Grohne  lemma2: do not confuse lookup with lookupM

commit  commitdiff  tree 
20120427 
Helmut Grohne  use fromFunc to define union

commit  commitdiff  tree 
20120427 
Helmut Grohne  prove the theorem2

commit  commitdiff  tree 
20120420 
Helmut Grohne  remove lemma\inlookupMassoc

commit  commitdiff  tree 
20120420 
Helmut Grohne  complete lemma2 using new property _indomainof_

commit  commitdiff  tree 
20120419 
Helmut Grohne  reduce hole in lemma2

commit  commitdiff  tree 
20120419 
Helmut Grohne  FinMap: lemmalookupMrestrict drop useless implicit

commit  commitdiff  tree 
20120419 
Helmut Grohne  move lemmajust!=nothing to FinMap and use it there

commit  commitdiff  tree 
20120417 
Helmut Grohne  inline botelim into lemmajustnothing

commit  commitdiff  tree 
20120404 
Helmut Grohne  abstract proofs over checkInsert

commit  commitdiff  tree 
20120316 
Helmut Grohne  fix wrong function name in lemma2

commit  commitdiff  tree 
20120209 
Helmut Grohne  remove useless braces

commit  commitdiff  tree 
20120209 
Helmut Grohne  avoid a sym in lemmaunionrestrict

commit  commitdiff  tree 
20120209 
Helmut Grohne  s/generate/restrict/g

commit  commitdiff  tree 
20120209 
Helmut Grohne  rephrase freetheoremlistlist using pointwise equality

commit  commitdiff  tree 
20120209 
Helmut Grohne  formulate theorem2

commit  commitdiff  tree 
20120209 
Helmut Grohne  prove lemmauniongenerate

commit  commitdiff  tree 
20120209 
Helmut Grohne  prove theorem1 assuming a lemmauniongenerate

commit  commitdiff  tree 
20120209 
Helmut Grohne  started proving theorem1

commit  commitdiff  tree 
20120209 
Helmut Grohne  introduce denumerate

commit  commitdiff  tree 
20120131 
Helmut Grohne  replace idrange with enumerate

commit  commitdiff  tree 
20120131 
Helmut Grohne  postulate free theorem for List a > List a

commit  commitdiff  tree 
20120126 
Helmut Grohne  recursion of lemma2

commit  commitdiff  tree 
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 
