diff options
Diffstat (limited to 'proofs/signatures/th_lra_test.plf')
-rw-r--r-- | proofs/signatures/th_lra_test.plf | 32 |
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))))) + ))))) + )))) + )) +) + + + |