blob: 687ff988b323bf2dd97bcffa251f8498fbcdcb1b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
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)))))
)))))
))))
))
)
|
