---

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


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)
10. ∀[p:iPolynomial()]
      (((p ∈ X1) ∨ (p ∈ X2))
      ⇒ (int_term_value(f;ipolynomial-term(p))
         = linearization(p;v) ⋅ map(λvs.accumulate (with value x and list item v):
                                         x * (f v)
                                        over list:
                                          vs
                                        with starting value:
                                         1);v)
         ∈ ℤ))
11. i : ℕ||map(λp.linearization(p;v);X1)||
12. ||map(λvs.accumulate (with value x and list item v):
               x * (f v)
              over list:
                vs
              with starting value:
               1);v)||
= ||linearization(X1[i];v)||
∈ ℤ
13. 0 < ||map(λvs.accumulate (with value x and list item v):
                   x * (f v)
                  over list:
                    vs
                  with starting value:
                   1);v)||
⊢ hd(map(λvs.accumulate (with value x and list item v): x * (f v)over list:  vswith starting value: 1);v)) = 1 ∈ ℤ
BY
{ ((DVar `v' THEN All Reduce⋅) THEN Auto THEN DVar `u'⋅ THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  X1  :  iPolynomial()  List
2.  X2  :  iPolynomial()  List
3.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
4.  (\mforall{}p\mmember{}X1.int\_term\_value(f;ipolynomial-term(p))  =  0)
5.  (\mforall{}p\mmember{}X2.0  \mleq{}  int\_term\_value(f;ipolynomial-term(p)))
6.  v  :  \mBbbZ{}  List  List
7.  rev(pcs-mon-vars(<X1,  X2>))  =  v
8.  0  <  ||v||
9.  hd(v)  =  []
10.  \mforall{}[p:iPolynomial()]
            (((p  \mmember{}  X1)  \mvee{}  (p  \mmember{}  X2))
            {}\mRightarrow{}  (int\_term\_value(f;ipolynomial-term(p))
                  =  linearization(p;v)  \mcdot{}  map(\mlambda{}vs.accumulate  (with  value  x  and  list  item  v):
                                                                                  x  *  (f  v)
                                                                                over  list:
                                                                                    vs
                                                                                with  starting  value:
                                                                                  1);v)))
11.  i  :  \mBbbN{}||map(\mlambda{}p.linearization(p;v);X1)||
12.  ||map(\mlambda{}vs.accumulate  (with  value  x  and  list  item  v):
                              x  *  (f  v)
                            over  list:
                                vs
                            with  starting  value:
                              1);v)||
=  ||linearization(X1[i];v)||
13.  0  <  ||map(\mlambda{}vs.accumulate  (with  value  x  and  list  item  v):
                                      x  *  (f  v)
                                    over  list:
                                        vs
                                    with  starting  value:
                                      1);v)||
\mvdash{}  hd(map(\mlambda{}vs.accumulate  (with  value  x  and  list  item  v):
                            x  *  (f  v)
                          over  list:
                              vs
                          with  starting  value:
                            1);v))
=  1


By

---

Latex:
((DVar  `v'  THEN  All  Reduce\mcdot{})  THEN  Auto  THEN  DVar  `u'\mcdot{}  THEN  All  Reduce  THEN  Auto)

---

Home Index