---

Step * 1 2 of Lemma mul-monomials_wf

.....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)} 
BY
{ (DSetVars THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. m5 : ℤ-o
2. m6 : ℤ List
3. sorted(m6)
4. m3 : ℤ-o
5. m4 : ℤ List
6. sorted(m4)
⊢ sorted(merge-int(m6;m4))

---

Latex:

---

Latex:
.....subterm.....  T:t
2: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{}  merge-int(m6;m4)  \mmember{}  \{vs:\mBbbZ{}  List|  sorted(vs)\} 


By

---

Latex:
(DSetVars  THEN  MemTypeCD  THEN  Auto)

---

Home Index