Reverting two files encoding with DOS linebreaks back into using unix linebreaks.

1 files changed, 449 insertions, 451 deletions

diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf
index 88118e8d1..d67fdc84f 100644
--- a/proofs/signatures/th_lra.plf
+++ b/proofs/signatures/th_lra.plf
@@ -1,451 +1,449 @@
-; 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))))))))

-    

-    

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