---

Step * 1 2 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)
         ∈ ℤ))
⊢ satisfiable(map(λp.linearization(p;v);X1);map(λp.linearization(p;v);X2))
BY
{ (D 0 With ⌜map(λvs.accumulate (with value x and list item v):
                      x * (f v)
                     over list:
                       vs
                     with starting value:
                      1);v)⌝ 
   THEN Auto
   ) }

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)
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)
         ∈ ℤ))
⊢ satisfies-integer-problem(map(λp.linearization(p;v);X1);map(λp.linearization(p;v);
                                                              X2);map(λvs.accumulate (with value x and list item v):
                                                                           x * (f v)
                                                                          over list:
                                                                            vs
                                                                          with starting value:
                                                                           1);v))

---

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


By

---

Latex:
(D  0  With  \mkleeneopen{}map(\mlambda{}vs.accumulate  (with  value  x  and  list  item  v):
                                        x  *  (f  v)
                                      over  list:
                                          vs
                                      with  starting  value:
                                        1);v)\mkleeneclose{} 
  THEN  Auto
  )

---

Home Index