Step * of Lemma satisfiable-pcs-to-integer-problem

`∀X:polynomial-constraints()`
`  (satisfiable_polynomial_constraints(X) `` satisfiable(fst(pcs-to-integer-problem(X));snd(pcs-to-integer-problem(X))))`
BY
`{ (Auto`
`   THEN D -1`
`   THEN Unfold `pcs-to-integer-problem` 0`
`   THEN (InstLemma `hd-rev-pcs-mon-vars` [⌜X⌝]⋅ THENA Auto)`
`   THEN MoveToConcl (-1)`
`   THEN (GenConclTerm ⌜rev(pcs-mon-vars(X))⌝⋅ THENA Auto)`
`   THEN (CallByValueReduce 0 THENA Auto)`
`   THEN (D 1 THEN Reduce 0)`
`   THEN RepUR ``satisfies-poly-constraints`` 4`
`   THEN RWO "eager-map-is-map" 0`
`   THEN Auto`
`   THEN RWO "evalall-reduce" 0`
`   THEN Auto`
`   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))`
`   THEN Reduce 0) }`

1
`1. X1 : iPolynomial() List`
`2. X2 : iPolynomial() List`
`3. f : ℤ ⟶ ℤ`
`4. (∀p∈X1.int_term_value(f;ipolynomial-term(p)) = 0 ∈ ℤ)`
`5. (∀p∈X2.0 ≤ int_term_value(f;ipolynomial-term(p)))`
`6. v : ℤ List List`
`7. rev(pcs-mon-vars(<X1, X2>)) = v ∈ (ℤ List List)`
`8. 0 < ||v||`
`9. hd(v) = [] ∈ (ℤ List)`
`⊢ satisfiable(map(λp.linearization(p;v);X1);map(λp.linearization(p;v);X2))`

Latex:

Latex:
\mforall{}X:polynomial-constraints()
(satisfiable\_polynomial\_constraints(X)
{}\mRightarrow{}  satisfiable(fst(pcs-to-integer-problem(X));snd(pcs-to-integer-problem(X))))

By

Latex:
(Auto
THEN  D  -1
THEN  Unfold  `pcs-to-integer-problem`  0
THEN  (InstLemma  `hd-rev-pcs-mon-vars`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)
THEN  MoveToConcl  (-1)
THEN  (GenConclTerm  \mkleeneopen{}rev(pcs-mon-vars(X))\mkleeneclose{}\mcdot{}  THENA  Auto)
THEN  (CallByValueReduce  0  THENA  Auto)
THEN  (D  1  THEN  Reduce  0)
THEN  RepUR  ``satisfies-poly-constraints``  4
THEN  RWO  "eager-map-is-map"  0
THEN  Auto
THEN  RWO  "evalall-reduce"  0
THEN  Auto
THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
THEN  Reduce  0)

Home Index