diff options
Diffstat (limited to 'proofs/signatures/th_base.plf')
-rwxr-xr-x | proofs/signatures/th_base.plf | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index 9dd950b5b..d6b283752 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -18,8 +18,8 @@ (! t1 (term (arrow s1 s2)) (! t2 (term s1) (term s2)))))) - - + + ; inference rules : (declare trust (th_holds false)) ; temporary @@ -44,6 +44,28 @@ (! u (th_holds (= _ y z)) (th_holds (= _ x z))))))))) +(declare negsymm (! s sort + (! x (term s) + (! y (term s) + (! u (th_holds (not (= _ x y))) + (th_holds (not (= _ y x)))))))) + +(declare negtrans1 (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (not (= _ x y))) + (! u (th_holds (= _ y z)) + (th_holds (not (= _ x z)))))))))) + +(declare negtrans2 (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (= _ x y)) + (! u (th_holds (not (= _ y z))) + (th_holds (not (= _ x z)))))))))) + (declare cong (! s1 sort (! s2 sort (! a1 (term (arrow s1 s2)) |