squash-merge from proof branch

7 files changed, 558 insertions, 23 deletions

diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am
index 82d8c2caa..2b6d16cfd 100644
--- a/proofs/signatures/Makefile.am
+++ b/proofs/signatures/Makefile.am
@@ -3,7 +3,7 @@
 # add support for more theories, just list them here in the same order
 # you would to the LFSC proof-checker binary.
 #
-CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf
+CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_real.plf th_int.plf
 
 noinst_LTLIBRARIES = libsignatures.la
 
diff --git a/proofs/signatures/example-arrays.plf b/proofs/signatures/example-arrays.plf
index 600fc11c9..c454a6dfe 100755
--- a/proofs/signatures/example-arrays.plf
+++ b/proofs/signatures/example-arrays.plf
@@ -9,7 +9,7 @@
 ; input :
 ; ~L1
 
-; (extenstionality) lemma : 
+; (extenstionality) lemma :
 ; L1 or ~L2
 
 ; theory conflicts :
@@ -26,13 +26,13 @@
 (check
 (% I sort
 (% E sort
-(% a (term (array I E))
+(% a (term (Array I E))
 (% i (term I)
 
 
 ; (1) -------------------- input formula -----------------------------------
 
-(% A1 (th_holds (not (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))))
+(% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))))
 
 
 
@@ -57,7 +57,7 @@
 ; (4) -------------------- map theory literals to boolean variables
 ;     --- maps all theory literals involved in proof to boolean literals
 
-(decl_atom (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1
+(decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1
 (decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2
 (decl_atom (= I i k) (\ v3 (\ a3
 
@@ -73,7 +73,7 @@
 
    ; use read over write rule "row"
    (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2)
-   
+
 ))))) (\ CT1
 ; CT1 is the clause ( v2 V v3 )
 
@@ -83,9 +83,9 @@
 (clausify_false
 
    ; use read over write rule "row1"
-   (contra _ (symm _ _ _ 
-   	     (trans _ _ _ _ 
-               (symm _ _ _ (cong _ _ _ _ _ _ 
+   (contra _ (symm _ _ _
+   	     (trans _ _ _ _
+               (symm _ _ _ (cong _ _ _ _ _ _
                	 (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))
                	 l3))
                (trans _ _ _ _
@@ -93,7 +93,7 @@
                  (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3)
                  )))
             l2)
-   
+
 ))))) (\ CT2
 ; CT2 is the clause ( v2 V ~v3 )
 
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index 8334f51de..5ed3d2f6f 100755
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -7,44 +7,56 @@
 
 ; sorts
 
-(declare array (! s1 sort (! s2 sort sort)))	; s1 is index, s2 is element
+(declare Array (! s1 sort (! s2 sort sort)))	; s1 is index, s2 is element
 
 ; functions
 (declare write (! s1 sort
                (! s2 sort
-                 (term (arrow (array s1 s2)
+                 (term (arrow (Array s1 s2)
                        (arrow s1
-                       (arrow s2 (array s1 s2))))))))
+                       (arrow s2 (Array s1 s2))))))))
 
 (declare read (! s1 sort
               (! s2 sort
-              	(term (arrow (array s1 s2)
+              	(term (arrow (Array s1 s2)
                	      (arrow s1 s2))))))
 
 ; inference rules
+
+; read( a[i] = b, i ) == b
 (declare row1 (! s1 sort
               (! s2 sort
-              (! t1 (term (array s1 s2))
+              (! t1 (term (Array s1 s2))
               (! t2 (term s1)
               (! t3 (term s2)
-              	(th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2)
-              		       t3))))))))
-              	
+              	(th_holds (= _
+		(apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) t3))))))))
 
 (declare row (! s1 sort
              (! s2 sort
              (! t2 (term s1)
              (! t3 (term s1)
-             (! t1 (term (array s1 s2))
+             (! t1 (term (Array s1 s2))
              (! t4 (term s2)
              (! u (th_holds (not (= _ t2 t3)))
                (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3)
                		      (apply _ _ (apply _ _ (read s1 s2) t1) t3)))))))))))
 
+(declare negativerow (! s1 sort
+                     (! s2 sort
+                     (! t2 (term s1)
+                     (! t3 (term s1)
+                     (! t1 (term (Array s1 s2))
+                     (! t4 (term s2)
+		     (! u (th_holds (not (= _
+                        (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3)
+                        (apply _ _ (apply _ _ (read s1 s2) t1) t3))))
+                     (th_holds (= _ t2 t3))))))))))
+
 (declare ext (! s1 sort
              (! s2 sort
-             (! t1 (term (array s1 s2))
-             (! t2 (term (array s1 s2))
+             (! t1 (term (Array s1 s2))
+             (! t2 (term (Array s1 s2))
              (! u1 (! k (term s1)
                    (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))
                      (holds cln)))
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))
diff --git a/proofs/signatures/th_int.plf b/proofs/signatures/th_int.plf
new file mode 100644
index 000000000..9a0a2d63c
--- /dev/null
+++ b/proofs/signatures/th_int.plf
@@ -0,0 +1,25 @@
+(declare Int sort)
+
+(define arithpred_Int (! x (term Int)
+                      (! y (term Int)
+                        formula)))
+
+(declare >_Int arithpred_Int)
+(declare >=_Int arithpred_Int)
+(declare <_Int  arithpred_Int)
+(declare <=_Int arithpred_Int)
+
+(define arithterm_Int (! x (term Int)
+		      (! y (term Int)
+		        (term Int))))
+
+(declare +_Int arithterm_Int)
+(declare -_Int arithterm_Int)
+(declare *_Int arithterm_Int)  ; is * ok to use?
+(declare /_Int arithterm_Int)  ; is / ok to use?
+
+; a constant term
+(declare a_int (! x mpz (term Int)))
+
+; unary negation
+(declare u-_Int (! t (term Int) (term Int)))
diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf
new file mode 100644
index 000000000..88118e8d1
--- /dev/null
+++ b/proofs/signatures/th_lra.plf
@@ -0,0 +1,451 @@
+; 59 loc in side conditions

+

+(program mpq_ifpos ((x mpq)) bool

+  (mp_ifneg x ff (mp_ifzero x ff tt)))

+

+; a real variable

+(declare var_real type)

+; a real variable term

+(declare a_var_real (! v var_real (term Real)))

+

+;; linear polynomials in the form a_1*x_1 + a_2*x_2 .... + a_n*x_n

+

+(declare lmon type)

+(declare lmonn lmon)

+(declare lmonc (! c mpq (! v var_real (! l lmon lmon))))

+

+(program lmon_neg ((l lmon)) lmon 

+  (match l

+    (lmonn l)

+    ((lmonc c' v' l') (lmonc (mp_neg c') v' (lmon_neg l')))))

+

+(program lmon_add ((l1 lmon) (l2 lmon)) lmon

+  (match l1

+    (lmonn l2)

+    ((lmonc c' v' l') 

+      (match l2

+        (lmonn l1)

+        ((lmonc c'' v'' l'')

+          (compare v' v'' 

+            (lmonc c' v' (lmon_add l' l2))

+            (lmonc c'' v'' (lmon_add l1 l''))))))))

+

+(program lmon_mul_c ((l lmon) (c mpq)) lmon

+  (match l

+    (lmonn l)

+    ((lmonc c' v' l') (lmonc (mp_mul c c') v' (lmon_mul_c l' c)))))

+

+;; linear polynomials in the form (a_1*x_1 + a_2*x_2 .... + a_n*x_n) + c 

+

+(declare poly type)

+(declare polyc (! c mpq (! l lmon poly)))

+

+(program poly_neg ((p poly)) poly

+  (match p

+    ((polyc m' p') (polyc (mp_neg m') (lmon_neg p')))))

+

+(program poly_add ((p1 poly) (p2 poly)) poly

+  (match p1

+    ((polyc c1 l1)

+      (match p2

+        ((polyc c2 l2) (polyc (mp_add c1 c2) (lmon_add l1 l2)))))))

+

+(program poly_sub ((p1 poly) (p2 poly)) poly

+  (poly_add p1 (poly_neg p2)))

+  

+(program poly_mul_c ((p poly) (c mpq)) poly

+  (match p

+    ((polyc c' l') (polyc (mp_mul c' c) (lmon_mul_c l' c)))))

+    

+;; code to isolate a variable from a term

+;; if (isolate v l) returns (c,l'), this means l = c*v + l', where v is not in FV(t').

+

+(declare isol type)

+(declare isolc (! r mpq (! l lmon isol)))

+

+(program isolate_h ((v var_real) (l lmon) (e bool)) isol

+  (match l

+    (lmonn (isolc 0/1 l))

+    ((lmonc c' v' l') 

+      (ifmarked v'

+        (match (isolate_h v l' tt) 

+          ((isolc ci li) (isolc (mp_add c' ci) li)))

+        (match e 

+          (tt (isolc 0/1 l))

+          (ff (match (isolate_h v l' ff) 

+                ((isolc ci li) (isolc ci (lmonc c' v' li))))))))))

+

+(program isolate ((v var_real) (l lmon)) isol

+  (do (markvar v)

+  (let i (isolate_h v l ff)

+  (do (markvar v) i))))

+

+;; determine if a monomial list is constant

+

+(program is_lmon_zero ((l lmon)) bool

+  (match l

+    (lmonn tt)

+    ((lmonc c v l')

+      (match (isolate v l)

+        ((isolc ci li) 

+          (mp_ifzero ci (is_lmon_zero li) ff))))))

+                

+;; return the constant that p is equal to.  If p is not constant, fail.

+                

+(program is_poly_const ((p poly)) mpq

+  (match p

+    ((polyc c' l')

+      (match (is_lmon_zero l')

+        (tt c')

+        (ff (fail mpq))))))

+

+;; conversion to use polynomials in term formulas

+

+(declare poly_term (! p poly (term Real)))

+    

+;; create new equality out of inequality

+

+(declare lra_>=_>=_to_=

+  (! p1 poly

+  (! p2 poly

+  (! f1 (th_holds (>=0_Real (poly_term p1)))

+  (! f2 (th_holds (>=0_Real (poly_term p2)))

+  (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)

+    (th_holds (=0_Real (poly_term p2))))))))))

+    

+;; axioms

+

+(declare lra_axiom_=

+   (th_holds (=0_Real (poly_term (polyc 0/1 lmonn)))))

+   

+(declare lra_axiom_>

+  (! c mpq 

+  (! i (^ (mpq_ifpos c) tt)

+    (th_holds (>0_Real (poly_term (polyc c lmonn)))))))

+    

+(declare lra_axiom_>=

+  (! c mpq 

+  (! i (^ (mp_ifneg c tt ff) ff)

+    (th_holds (>=0_Real (poly_term (polyc c lmonn)))))))

+    

+(declare lra_axiom_distinct

+  (! c mpq 

+  (! i (^ (mp_ifzero c tt ff) ff)

+    (th_holds (distinct0_Real (poly_term (polyc c lmonn)))))))

+

+;; contradiction rules

+

+(declare lra_contra_=

+  (! p poly

+  (! f (th_holds (=0_Real (poly_term p)))

+  (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)

+    (holds cln)))))

+    

+(declare lra_contra_>

+  (! p poly

+  (! f (th_holds (>0_Real (poly_term p)))

+  (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)

+    (holds cln)))))

+    

+(declare lra_contra_>=

+  (! p poly

+  (! f (th_holds (>=0_Real (poly_term p)))

+  (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)

+    (holds cln)))))

+    

+(declare lra_contra_distinct

+  (! p poly

+  (! f (th_holds (distinct0_Real (poly_term p)))

+  (! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt)

+    (holds cln)))))

+

+;; muliplication by a constant

+

+(declare lra_mul_c_=

+  (! p poly

+  (! p' poly

+  (! c mpq

+  (! f (th_holds (=0_Real (poly_term p)))

+  (! i (^ (poly_mul_c p c) p')

+    (th_holds (=0_Real (poly_term p')))))))))

+

+(declare lra_mul_c_>

+  (! p poly

+  (! p' poly

+  (! c mpq

+  (! f (th_holds (>0_Real (poly_term p)))

+  (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')

+    (th_holds (>0_Real (poly_term p')))))))));)

+    

+(declare lra_mul_c_>=

+  (! p poly

+  (! p' poly

+  (! c mpq

+  (! f (th_holds (>=0_Real (poly_term p)))

+  (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')

+    (th_holds (>=0_Real (poly_term p')))))))));)

+    

+(declare lra_mul_c_distinct

+  (! p poly

+  (! p' poly

+  (! c mpq

+  (! f (th_holds (distinct0_Real (poly_term p)))

+  (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')

+    (th_holds (distinct0_Real (poly_term p')))))))));)

+

+;; adding equations

+

+(declare lra_add_=_=

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (=0_Real (poly_term p1)))

+  (! f2 (th_holds (=0_Real (poly_term p2)))

+  (! i (^ (poly_add p1 p2) p3)

+    (th_holds (=0_Real (poly_term p3)))))))))))

+    

+(declare lra_add_>_>

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (>0_Real (poly_term p1)))

+  (! f2 (th_holds (>0_Real (poly_term p2)))

+  (! i (^ (poly_add p1 p2) p3)

+    (th_holds (>0_Real (poly_term p3))))))))))

+    

+(declare lra_add_>=_>=

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (>=0_Real (poly_term p1)))

+  (! f2 (th_holds (>=0_Real (poly_term p2)))

+  (! i (^ (poly_add p1 p2) p3)

+    (th_holds (>=0_Real (poly_term p3))))))))))

+

+(declare lra_add_=_>

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (=0_Real (poly_term p1)))

+  (! f2 (th_holds (>0_Real (poly_term p2)))

+  (! i (^ (poly_add p1 p2) p3)

+    (th_holds (>0_Real (poly_term p3))))))))))

+    

+(declare lra_add_=_>=

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (=0_Real (poly_term p1)))

+  (! f2 (th_holds (>=0_Real (poly_term p2)))

+  (! i (^ (poly_add p1 p2) p3)

+    (th_holds (>=0_Real (poly_term p3))))))))))

+

+(declare lra_add_>_>=

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (>0_Real (poly_term p1)))

+  (! f2 (th_holds (>=0_Real (poly_term p2)))

+  (! i (^ (poly_add p1 p2) p3)

+    (th_holds (>0_Real (poly_term p3))))))))))

+    

+(declare lra_add_=_distinct

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (=0_Real (poly_term p1)))

+  (! f2 (th_holds (distinct0_Real (poly_term p2)))

+  (! i (^ (poly_add p1 p2) p3)

+    (th_holds (distinct0_Real (poly_term p3)))))))))))

+    

+;; substracting equations

+

+(declare lra_sub_=_=

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (=0_Real (poly_term p1)))

+  (! f2 (th_holds (=0_Real (poly_term p2)))

+  (! i (^ (poly_sub p1 p2) p3)

+    (th_holds (=0_Real (poly_term p3)))))))))))

+    

+(declare lra_sub_>_=

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (>0_Real (poly_term p1)))

+  (! f2 (th_holds (=0_Real (poly_term p2)))

+  (! i (^ (poly_sub p1 p2) p3)

+    (th_holds (>0_Real (poly_term p3))))))))))

+    

+(declare lra_sub_>=_=

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (>=0_Real (poly_term p1)))

+  (! f2 (th_holds (=0_Real (poly_term p2)))

+  (! i (^ (poly_sub p1 p2) p3)

+    (th_holds (>=0_Real (poly_term p3))))))))))

+    

+(declare lra_sub_distinct_=

+  (! p1 poly

+  (! p2 poly

+  (! p3 poly

+  (! f1 (th_holds (distinct0_Real (poly_term p1)))

+  (! f2 (th_holds (=0_Real (poly_term p2)))

+  (! i (^ (poly_sub p1 p2) p3)

+    (th_holds (distinct0_Real (poly_term p3)))))))))))

+

+ ;; converting between terms and polynomials

+

+(declare poly_norm (! t (term Real) (! p poly type))) 

+

+(declare pn_let 

+  (! t (term Real)

+  (! p poly

+  (! pn (poly_norm t p)

+

+  (! u (! pnt (poly_norm t p)

+         (holds cln))

+    (holds cln))))))

+

+(declare pn_const

+  (! x mpq

+    (poly_norm (a_real x) (polyc x lmonn))))

+  

+(declare pn_var

+  (! v var_real

+    (poly_norm (a_var_real v) (polyc 0/1 (lmonc 1/1 v lmonn)))))

+

+

+(declare pn_+

+  (! x (term Real)

+  (! px poly

+  (! y (term Real)

+  (! py poly

+  (! pz poly

+  (! pnx (poly_norm x px)

+  (! pny (poly_norm y py)

+  (! a (^ (poly_add px py) pz)

+    (poly_norm (+_Real x y) pz))))))))))

+    

+(declare pn_-

+  (! x (term Real)

+  (! px poly

+  (! y (term Real)

+  (! py poly

+  (! pz poly

+  (! pnx (poly_norm x px)

+  (! pny (poly_norm y py)

+  (! a (^ (poly_sub px py) pz)

+    (poly_norm (-_Real x y) pz))))))))))

+    

+(declare pn_mul_c_L

+  (! y (term Real)

+  (! py poly

+  (! pz poly

+  (! x mpq

+  (! pny (poly_norm y py)

+  (! a (^ (poly_mul_c py x) pz)

+    (poly_norm (*_Real (a_real x) y) pz))))))))

+    

+(declare pn_mul_c_R

+  (! y (term Real)

+  (! py poly

+  (! pz poly

+  (! x mpq

+  (! pny (poly_norm y py)

+  (! a (^ (poly_mul_c py x) pz)

+    (poly_norm (*_Real y (a_real x)) pz))))))))

+

+;; for polynomializing other terms, in particular ite's

+

+(declare term_atom (! v var_real (! t (term Real) type)))

+

+(declare decl_term_atom

+  (! t (term Real)

+  (! u (! v var_real

+       (! a (term_atom v t)

+         (holds cln)))

+    (holds cln))))

+    

+(declare pn_var_atom

+  (! v var_real

+  (! t (term Real)

+  (! a (term_atom v t)

+    (poly_norm t (polyc 0/1 (lmonc 1/1 v lmonn)))))))

+

+

+;; conversion between term formulas and polynomial formulas

+

+(declare poly_formula_norm (! ft formula (! fp formula type))) 

+

+; convert between term formulas and polynomial formulas

+

+(declare poly_form

+  (! ft formula

+  (! fp formula

+  (! p (poly_formula_norm ft fp)

+  (! u (th_holds ft)

+    (th_holds fp))))))

+    

+(declare poly_form_not

+  (! ft formula

+  (! fp formula

+  (! p (poly_formula_norm ft fp)

+  (! u (th_holds (not ft))

+    (th_holds (not fp)))))))

+ 

+; form equivalence between term formula and polynomial formula 

+   

+(declare poly_norm_=

+  (! x (term Real)

+  (! y (term Real)

+  (! p poly

+  (! h (th_holds (= Real x y))

+  (! n (poly_norm (-_Real x y) p)

+  (! u (! pn (th_holds (=0_Real (poly_term p)))

+         (holds cln))

+    (holds cln))))))))

+ 

+(declare poly_norm_>

+  (! x (term Real)

+  (! y (term Real)

+  (! p poly

+  (! h (th_holds (>_Real x y))

+  (! n (poly_norm (-_Real x y) p)

+  (! u (! pn (th_holds (>0_Real (poly_term p)))

+         (holds cln))

+    (holds cln))))))))

+    

+(declare poly_norm_<

+  (! x (term Real)

+  (! y (term Real)

+  (! p poly

+  (! h (th_holds (<_Real x y))

+  (! n (poly_norm (-_Real y x) p)

+  (! u (! pn (th_holds (>0_Real (poly_term p)))

+         (holds cln))

+    (holds cln))))))))

+    

+(declare poly_norm_>=

+  (! x (term Real)

+  (! y (term Real)

+  (! p poly

+  (! h (th_holds (>=_Real x y))

+  (! n (poly_norm (-_Real x y) p)

+  (! u (! pn (th_holds (>=0_Real (poly_term p)))

+         (holds cln))

+    (holds cln))))))))

+    

+(declare poly_norm_<=

+  (! x (term Real)

+  (! y (term Real)

+  (! p poly

+  (! h (th_holds (<=_Real x y))

+  (! n (poly_norm (-_Real y x) p)

+  (! u (! pn (th_holds (>=0_Real (poly_term p)))

+         (holds cln))

+    (holds cln))))))))

+    

+    

diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf
new file mode 100644
index 000000000..3478e23ef
--- /dev/null
+++ b/proofs/signatures/th_real.plf
@@ -0,0 +1,25 @@
+(declare Real sort)
+
+(define arithpred_Real (! x (term Real)
+                       (! y (term Real)
+                         formula)))
+
+(declare >_Real arithpred_Real)
+(declare >=_Real arithpred_Real)
+(declare <_Real  arithpred_Real)
+(declare <=_Real arithpred_Real)
+
+(define arithterm_Real (! x (term Real)
+                       (! y (term Real)
+                         (term Real))))
+
+(declare +_Real arithterm_Real)
+(declare -_Real arithterm_Real)
+(declare *_Real arithterm_Real)  ; is * ok to use?
+(declare /_Real arithterm_Real)  ; is / ok to use?
+
+; a constant term
+(declare a_real (! x mpq (term Real)))
+
+; unary negation
+(declare u-_Real (! t (term Real) (term Real)))