update bff implementation to use delete
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 17 Dec 2013 07:22:12 +0000 (08:22 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 17 Dec 2013 07:35:23 +0000 (08:35 +0100)
commit066861f9cdde4ded6c5442508bef1a27576c68d7
tree3e199fdfd1cb746d3c637b5b2817ec53b17a6d67
parent2c37e0c2f32b4c6b5c121827a4abddf7fc1dd7e0
update bff implementation to use delete

In the presence of shape-changing updates, bff needs to shrink one of
the mappings before unifying them. As long the shape does not change,
the union becomes a disjoint union. With this insight we can adapt the
proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately
theorem-2 requires more work and assoc-enough becomes non-trivial due to
the introduction of mapMV.
BFF.agda
Bidir.agda
FinMap.agda
Precond.agda