---

Step * 1 of Lemma mul-monomials_wf


1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
⊢ <m5 * m3, merge-int(m6;m4)> ∈ iMonomial()
BY
{ (Unfold `iMonomial` 0 THEN MemCD) }

1
.....subterm..... T:t
1:n
1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
⊢ m5 * m3 ∈ ℤ-o

2
.....subterm..... T:t
2:n
1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
⊢ merge-int(m6;m4) ∈ {vs:ℤ List| sorted(vs)} 

---

Latex:

---

Latex:

1.  m5  :  \mBbbZ{}\msupminus{}\msupzero{}
2.  m6  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
3.  m3  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  m4  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
\mvdash{}  <m5  *  m3,  merge-int(m6;m4)>  \mmember{}  iMonomial()


By

---

Latex:
(Unfold  `iMonomial`  0  THEN  MemCD)

---

Home Index