1 files changed, 32 insertions, 0 deletions
diff --git a/proofs/signatures/th_lra_test.plf b/proofs/signatures/th_lra_test.plf
new file mode 100644
index 000000000..687ff988b
--- /dev/null
+++ b/proofs/signatures/th_lra_test.plf
@@ -0,0 +1,32 @@
+; Depends On: th_lra.plf
+(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_Real (poly_term p1)))
+  (% pf_nonneg_2 (th_holds (>=0_Real (poly_term p2)))
+  (% pf_nonneg_3 (th_holds (>=0_Real (poly_term p3)))
+     (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)))))
+  )))))
+  ))))
+  ))
+)
+
+
+