---

Step * 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. no_repeats(ℤ List;v)
11. p : iPolynomial()
12. (p ∈ X1) ∨ (p ∈ X2)
13. i : ℕ||p||
⊢ (snd(p[i]) ∈ v)
BY
{ (RevHypSubst' (-7) 0 THEN RWW "member-reverse member-pcs-mon-vars" 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. no_repeats(ℤ List;v)
11. p : iPolynomial()
12. (p ∈ X1) ∨ (p ∈ X2)
13. i : ℕ||p||
⊢ ((snd(p[i])) = [] ∈ (ℤ List))
∨ (∃p1∈fst(<X1, X2>). (∃m∈p1. (snd(p[i])) = (snd(m)) ∈ (ℤ List)))
∨ (∃p1∈snd(<X1, X2>). (∃m∈p1. (snd(p[i])) = (snd(m)) ∈ (ℤ List)))

---

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.  no\_repeats(\mBbbZ{}  List;v)
11.  p  :  iPolynomial()
12.  (p  \mmember{}  X1)  \mvee{}  (p  \mmember{}  X2)
13.  i  :  \mBbbN{}||p||
\mvdash{}  (snd(p[i])  \mmember{}  v)


By

---

Latex:
(RevHypSubst'  (-7)  0  THEN  RWW  "member-reverse  member-pcs-mon-vars"  0  THEN  Auto)

---

Home Index