---

Step * 1 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
⊢ ¬(b2 = a2 ∈ (ℤ List))
BY
{ (ParallelLast THEN HypSubst' (-1) 0) }

1
1. a1 : ℤ-o
2. a2 : {vs:ℤ List| sorted(vs)} 
3. b1 : ℤ-o
4. b2 : {vs:ℤ List| sorted(vs)} 
5. b2 = a2 ∈ (ℤ List)
⊢ ↑a2 ≤_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
\mvdash{}  \mneg{}(b2  =  a2)


By

---

Latex:
(ParallelLast  THEN  HypSubst'  (-1)  0)

---

Home Index