---

Step * 1 2 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)||
⊢ 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) =0
BY
{ (Unfold `satisfies-integer-equality` 0 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)
         ∈ ℤ))
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 ∈ ℤ

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)
         ∈ ℤ))
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)||
14. hd(map(λvs.accumulate (with value x and list item v): x * (f v)over list:  vswith starting value: 1);v)) = 1 ∈ ℤ
⊢ linearization(X1[i];v) ⋅ map(λvs.accumulate (with value x and list item v):
                                    x * (f v)
                                   over list:
                                     vs
                                   with starting value:
                                    1);v)
= 0
∈ ℤ

---

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)||
\mvdash{}  map(\mlambda{}vs.accumulate  (with  value  x  and  list  item  v):
                      x  *  (f  v)
                    over  list:
                        vs
                    with  starting  value:
                      1);v)  \mcdot{}  linearization(X1[i];v)  =0


By

---

Latex:
(Unfold  `satisfies-integer-equality`  0  THEN  Auto)

---

Home Index