prove the remaining parts of lemma-checkInsert-generate
authorHelmut Grohne <helmut@subdivi.de>
Thu, 26 Jan 2012 13:51:21 +0000 (14:51 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 26 Jan 2012 13:51:21 +0000 (14:51 +0100)
commit53e656496f0dfc6b5d6b8b6e5caf5efc0e7ee404
tree70e2a12871b68c63c01462c0f0c5f636a0d340e6
parent024635440449c8249cdff9d5637fcb7e02b5d293
prove the remaining parts of lemma-checkInsert-generate

Introducing the following lemmata:
 * lemma-lookupM-empty : nothing \== lookupM i empty
 * lemma-from-just : just x \== just y -> x \== y
 * lemma-lookupM-insert : just a \== lookupM i (insert i a m)
 * lemma-lookupM-insert-other : \neg (i \== j) ->
   lookupM i m \== lookupM i (insert j a m)
 * lemma-lookupM-generate : just a = lookupM i (generate f is) -> a \== f i
Bidir.agda