update from the master

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))