---

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

.....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)
       ∈ ℤ))
BY
{ ((Assert no_repeats(ℤ List;v) BY
          (RevHypSubst'  (-3) 0 THEN RWO "no_repeats_reverse" 0 THEN Auto))
   THEN (D 0 THENA Auto)
   THEN RWO "linearization-value<" 0
   THEN Auto
   THEN (D 0 THENA 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. no_repeats(ℤ List;v)
11. p : iPolynomial()
12. (p ∈ X1) ∨ (p ∈ X2)
13. i : ℕ||p||
⊢ (snd(p[i]) ∈ v)

---

Latex:

---

Latex:
.....assertion..... 
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{}  \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)))


By

---

Latex:
((Assert  no\_repeats(\mBbbZ{}  List;v)  BY
                (RevHypSubst'    (-3)  0  THEN  RWO  "no\_repeats\_reverse"  0  THEN  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  RWO  "linearization-value<"  0
  THEN  Auto
  THEN  (D  0  THENA  Auto))

---

Home Index