---

Step * 1 1 1 1 of Lemma imonomial-less-transitive


1. m5 : {vs:ℤ List| sorted(vs)} 
2. m4 : ℤ-o
3. m6 : ℤ-o
4. m7 : {vs:ℤ List| sorted(vs)} 
5. m8 : ℤ-o
6. m9 : {vs:ℤ List| sorted(vs)} 
7. ¬(m5 = m7 ∈ (ℤ List))
8. m5 ≤_lex m7 = tt
9. ¬(m7 = m5 ∈ (ℤ List))
10. m7 ≤_lex m5 = tt
11. m5 = m9 ∈ (ℤ List)
⊢ False
BY
{ (FLemma `intlex-antisym` [-4;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  m5  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
2.  m4  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  m6  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  m7  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
5.  m8  :  \mBbbZ{}\msupminus{}\msupzero{}
6.  m9  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
7.  \mneg{}(m5  =  m7)
8.  m5  \mleq{}\_lex  m7  =  tt
9.  \mneg{}(m7  =  m5)
10.  m7  \mleq{}\_lex  m5  =  tt
11.  m5  =  m9
\mvdash{}  False


By

---

Latex:
(FLemma  `intlex-antisym`  [-4;-2]  THEN  Auto)

---

Home Index