---

Step * 2 of Lemma not-imonomial-le


1. a1 : ℤ-o
2. a2 : {vs:ℤ List| sorted(vs)} 
3. b1 : ℤ-o
4. b2 : {vs:ℤ List| sorted(vs)} 
5. ¬↑a2 ≤_lex b2
6. ¬(b2 = a2 ∈ (ℤ List))
⊢ ↑b2 ≤_lex a2
BY
{ DSetVars }

1
1. a1 : ℤ-o
2. a2 : ℤ List
3. [%5] : sorted(a2)
4. b1 : ℤ-o
5. b2 : ℤ List
6. [%3] : sorted(b2)
7. ¬↑a2 ≤_lex b2
8. ¬(b2 = a2 ∈ (ℤ List))
⊢ ↑b2 ≤_lex a2

---

Latex:

---

Latex:

1.  a1  :  \mBbbZ{}\msupminus{}\msupzero{}
2.  a2  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
3.  b1  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  b2  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
5.  \mneg{}\muparrow{}a2  \mleq{}\_lex  b2
6.  \mneg{}(b2  =  a2)
\mvdash{}  \muparrow{}b2  \mleq{}\_lex  a2


By

---

Latex:
DSetVars

---

Home Index