1 files changed, 0 insertions, 167 deletions
diff --git a/proofs/signatures/th_lra_test.plf b/proofs/signatures/th_lra_test.plf
deleted file mode 100644
index fb3ca828c..000000000
--- a/proofs/signatures/th_lra_test.plf
+++ /dev/null
@@ -1,167 +0,0 @@
-; Depends On: th_lra.plf
-;; Proof (from predicates on linear polynomials) that the following imply bottom
-;
-; -x - 1/2 y + 2 >= 0
-;  x +     y - 8 >= 0
-;  x -     y + 0 >= 0
-;
-(check
-  ; Variables
-  (% x var_real
-  (% y var_real
-  ; linear monomials (combinations)
-  (@ m1 (lmonc (~ 1/1) x (lmonc (~ 1/2) y lmonn))
-  (@ m2 (lmonc 1/1 x (lmonc 1/1 y lmonn))
-  (@ m3 (lmonc 1/1 x (lmonc (~ 1/1) y lmonn))
-  ; linear polynomials (affine)
-  (@ p1 (polyc 2/1 m1)
-  (@ p2 (polyc (~ 8/1) m2)
-  (@ p3 (polyc 0/1 m3)
-  (% pf_nonneg_1 (th_holds (>=0_poly p1))
-  (% pf_nonneg_2 (th_holds (>=0_poly p2))
-  (% pf_nonneg_3 (th_holds (>=0_poly p3))
-     (:
-       (holds cln)
-       (lra_contra_>=
-         _
-         (lra_add_>=_>= _ _ _
-           (lra_mul_c_>= _ _ 4/1 pf_nonneg_1)
-           (lra_add_>=_>= _ _ _
-             (lra_mul_c_>= _ _ 3/1 pf_nonneg_2)
-             (lra_add_>=_>= _ _ _
-               (lra_mul_c_>= _ _ 1/1 pf_nonneg_3)
-               (lra_axiom_>= 0/1))))))
-  )))))
-  ))))
-  ))
-)
-
-;; Proof (from predicates on real terms) that the following imply bottom
-;
-; -x - 1/2 y >= 2
-;  x +     y >= 8
-;  x -     y >= 0
-;
-(check
-  ; Declarations
-  ; Variables
-  (% x var_real
-  (% y var_real
-  ; real predicates
-  (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (a_var_real x)) (*_Real (a_real (~ 1/2)) (a_var_real y))) (a_real (~ 2/1)))
-  (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (a_var_real x)) (*_Real (a_real 1/1) (a_var_real y))) (a_real 8/1))
-  (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (a_var_real x)) (*_Real (a_real (~ 1/1)) (a_var_real y))) (a_real 0/1))
-  ; proof of real predicates
-  (% pf_f1 (th_holds f1)
-  (% pf_f2 (th_holds f2)
-  (% pf_f3 (th_holds f3)
-
-
-  ; Normalization
-  ; real term -> linear polynomial normalization witnesses
-  (@ n1 (poly_formula_norm_>=  _ _ _
-        (pn_- _ _ _ _ _
-          (pn_+ _ _ _ _ _
-            (pn_mul_c_L _ _ _ (~ 1/1) (pn_var x))
-            (pn_mul_c_L _ _ _ (~ 1/2) (pn_var y)))
-          (pn_const (~ 2/1))))
-  (@ n2 (poly_formula_norm_>=  _ _ _
-        (pn_- _ _ _ _ _
-          (pn_+ _ _ _ _ _
-            (pn_mul_c_L _ _ _ 1/1 (pn_var x))
-            (pn_mul_c_L _ _ _ 1/1 (pn_var y)))
-          (pn_const 8/1)))
-  (@ n3 (poly_formula_norm_>=  _ _ _
-        (pn_- _ _ _ _ _
-          (pn_+ _ _ _ _ _
-            (pn_mul_c_L _ _ _ 1/1 (pn_var x))
-            (pn_mul_c_L _ _ _ (~ 1/1) (pn_var y)))
-          (pn_const 0/1)))
-  ; proof of linear polynomial predicates
-  (@ pf_n1 (poly_form _ _ n1 pf_f1)
-  (@ pf_n2 (poly_form _ _ n2 pf_f2)
-  (@ pf_n3 (poly_form _ _ n3 pf_f3)
-
-  ; derivation of a contradiction using farkas coefficients
-    (:
-      (holds cln)
-      (lra_contra_>= _
-       (lra_add_>=_>= _ _ _
-         (lra_mul_c_>= _ _ 4/1 pf_n1)
-         (lra_add_>=_>= _ _ _
-           (lra_mul_c_>= _ _ 3/1 pf_n2)
-           (lra_add_>=_>= _ _ _
-             (lra_mul_c_>= _ _ 1/1 pf_n3)
-             (lra_axiom_>= 0/1))))))
-  )))
-  )))
-  )))
-  )))
-  ))
-)
-
-;; Term proof, 2 (>=), one (not >=)
-;; Proof (from predicates on real terms) that the following imply bottom
-;
-;        -x +     y >=  2
-;         x +     y >=  2
-;     not[        y >= -2] => [y < -2] => [-y > 2]
-;
-(check
-  ; Declarations
-  ; Variables
-  (% x var_real
-  (% y var_real
-  ; real predicates
-  (@ f1 (>=_Real
-          (+_Real (*_Real (a_real (~ 1/1)) (a_var_real x)) (a_var_real y))
-          (a_real 2/1))
-  (@ f2 (>=_Real
-          (+_Real (a_var_real x) (a_var_real y))
-          (a_real 2/1))
-  (@ f3 (not (>=_Real (a_var_real y) (a_real (~ 2/1))))
-
-  ; Normalization
-  ; proof of real predicates
-  (% pf_f1 (th_holds f1)
-  (% pf_f2 (th_holds f2)
-  (% pf_f3 (th_holds f3)
-  ; real term -> linear polynomial normalization witnesses
-  (@ n1 (poly_formula_norm_>=  _ _ _
-        (pn_- _ _ _ _ _
-          (pn_+ _ _ _ _ _
-            (pn_mul_c_L _ _ _ (~ 1/1) (pn_var x))
-            (pn_var y))
-          (pn_const 2/1)))
-  (@ n2 (poly_formula_norm_>=  _ _ _
-        (pn_- _ _ _ _ _
-          (pn_+ _ _ _ _ _
-            (pn_var x)
-            (pn_var y))
-          (pn_const 2/1)))
-  (@ n3 (poly_formula_norm_>=  _ _ _
-        (pn_- _ _ _ _ _
-          (pn_var y)
-          (pn_const (~ 2/1))))
-  ; proof of linear polynomial predicates
-  (@ pf_n1 (poly_form _ _ n1 pf_f1)
-  (@ pf_n2 (poly_form _ _ n2 pf_f2)
-  (@ pf_n3 (poly_flip_not_>= _ _ (poly_form_not _ _ n3 pf_f3))
-
-  ; derivation of a contradiction using farkas coefficients
-    (:
-      (holds cln)
-      (lra_contra_> _
-       (lra_add_>=_> _ _ _
-         (lra_mul_c_>= _ _ 1/1 pf_n1)
-         (lra_add_>=_> _ _ _
-           (lra_mul_c_>= _ _ 1/1 pf_n2)
-           (lra_add_>_>= _ _ _
-             (lra_mul_c_> _ _ 2/1 pf_n3)
-             (lra_axiom_>= 0/1))))))
-  )))
-  )))
-  )))
-  )))
-  ))
-)