---

Step * 1 1 of Lemma mul-monomials_wf

.....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
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}


By

---

Latex:
Auto

---

Home Index