prove assoc-enough in the presence of delete
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 27 Jan 2014 08:02:45 +0000 (09:02 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 27 Jan 2014 08:02:45 +0000 (09:02 +0100)
commitd2521627834713a651be0ac22aab0a1cd78df920
tree0dcc208b6b824af20f4f7971dcaeb14d1d5ebdb2
parent2d7db0d8c48c41ecef78ef9f18253632a80f4710
prove assoc-enough in the presence of delete

The old definition of bff had a single failure mode - assoc - and its
proof was a single cong. Now we need to show that the other failure mode
- mapM (flip lookupM ...) - is eliminated by the success of the former
resulting in a larger proof.
Precond.agda