---

Step * 1 1 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||
⊢ (∃p1∈X1. (∃m∈p1. (snd(p[i])) = (snd(m)) ∈ (ℤ List))) ∨ (∃p1∈X2. (∃m∈p1. (snd(p[i])) = (snd(m)) ∈ (ℤ List)))
BY
{ (ParallelOp -2
   THEN RepeatFor 2 (D -2)
   THEN D 0 With ⌜i1⌝ 
   THEN Auto
   THEN D 0 With ⌜i⌝ 
   THEN Auto
   THEN RevHypSubst' (-2) 0
   THEN Auto) }

---

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{}  (\mexists{}p1\mmember{}X1.  (\mexists{}m\mmember{}p1.  (snd(p[i]))  =  (snd(m))))  \mvee{}  (\mexists{}p1\mmember{}X2.  (\mexists{}m\mmember{}p1.  (snd(p[i]))  =  (snd(m))))


By

---

Latex:
(ParallelOp  -2
  THEN  RepeatFor  2  (D  -2)
  THEN  D  0  With  \mkleeneopen{}i1\mkleeneclose{} 
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{} 
  THEN  Auto
  THEN  RevHypSubst'  (-2)  0
  THEN  Auto)

---

Home Index