diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /proofs/signatures/th_base.plf | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
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)) |