---

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