---

Step * of Lemma member-polynomial-mon-vars

∀p:iMonomial() List. ∀L:ℤ List List. ∀vs:ℤ List.
  ((vs ∈ polynomial-mon-vars(L;p)) ⇐⇒ (vs ∈ L) ∨ (∃m∈p. vs = (snd(m)) ∈ (ℤ List)))
BY
{ (Unfold `polynomial-mon-vars` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN RWO "l_exists_nil l_exists_cons -1" 0
   THEN Auto
   THEN DVar `u'
   THEN All Reduce) }

1
1. u1 : ℤ-o@i
2. u2 : {vs:ℤ List| sorted(vs)} @i
3. v : iMonomial() List@i
4. ∀L:ℤ List List. ∀vs:ℤ List.
     ((vs ∈ accumulate (with value vss and list item m):
             let c,vs = m 
             in insert(vs;vss)
            over list:
              v
            with starting value:
             L))
     ⇐⇒ (vs ∈ L) ∨ (∃m∈v. vs = (snd(m)) ∈ (ℤ List)))@i
5. L : ℤ List List@i
6. vs : ℤ List@i
7. (vs ∈ insert(u2;L)) ∨ (∃m∈v. vs = (snd(m)) ∈ (ℤ List))@i
⊢ (vs ∈ L) ∨ (vs = u2 ∈ (ℤ List)) ∨ (∃m∈v. vs = (snd(m)) ∈ (ℤ List))

2
1. u1 : ℤ-o@i
2. u2 : {vs:ℤ List| sorted(vs)} @i
3. v : iMonomial() List@i
4. ∀L:ℤ List List. ∀vs:ℤ List.
     ((vs ∈ accumulate (with value vss and list item m):
             let c,vs = m 
             in insert(vs;vss)
            over list:
              v
            with starting value:
             L))
     ⇐⇒ (vs ∈ L) ∨ (∃m∈v. vs = (snd(m)) ∈ (ℤ List)))@i
5. L : ℤ List List@i
6. vs : ℤ List@i
7. (vs ∈ L) ∨ (vs = u2 ∈ (ℤ List)) ∨ (∃m∈v. vs = (snd(m)) ∈ (ℤ List))@i
⊢ (vs ∈ insert(u2;L)) ∨ (∃m∈v. vs = (snd(m)) ∈ (ℤ List))

---

Latex:

---

Latex:
\mforall{}p:iMonomial()  List.  \mforall{}L:\mBbbZ{}  List  List.  \mforall{}vs:\mBbbZ{}  List.
    ((vs  \mmember{}  polynomial-mon-vars(L;p))  \mLeftarrow{}{}\mRightarrow{}  (vs  \mmember{}  L)  \mvee{}  (\mexists{}m\mmember{}p.  vs  =  (snd(m))))


By

---

Latex:
(Unfold  `polynomial-mon-vars`  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  RWO  "l\_exists\_nil  l\_exists\_cons  -1"  0
  THEN  Auto
  THEN  DVar  `u'
  THEN  All  Reduce)

---

Home Index