generalize BFF and theorem-2 to arbitrary Setoids
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 23 Jan 2014 12:19:02 +0000 (13:19 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 23 Jan 2014 12:19:02 +0000 (13:19 +0100)
commitaf1ea86b6e817a85d4d160833fc5d4bb89e2df7b
tree1a634eae43fb1656bda3f5a3bb856b744131c73d
parent9cb635bb49c1846da7f9c00cc475b0fac9a2fa42
generalize BFF and theorem-2 to arbitrary Setoids

Since the generalization of lemma-checkInsert-restrict there is nothing
to show for theorem-1. So everything works with Setoids now yielding the
same results as the paper proofs.
BFF.agda
Bidir.agda
Precond.agda