---

Step * 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)
⊢ satisfiable(map(λp.linearization(p;v);X1);map(λp.linearization(p;v);X2))
BY
{ Assert ⌜∀[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)
               ∈ ℤ))⌝⋅ }

1
.....assertion..... 
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)
⊢ ∀[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)
       ∈ ℤ))

2
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)
         ∈ ℤ))
⊢ satisfiable(map(λp.linearization(p;v);X1);map(λp.linearization(p;v);X2))

---

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)  =  []
\mvdash{}  satisfiable(map(\mlambda{}p.linearization(p;v);X1);map(\mlambda{}p.linearization(p;v);X2))


By

---

Latex:
Assert  \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{}

---

Home Index