---

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


1. m4 : ℤ-o
2. m5 : {vs:ℤ List| sorted(vs)} 
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 = m9 ∈ (ℤ List))
10. m7 ≤_lex m9 = tt
⊢ ¬(m5 = m9 ∈ (ℤ List))
BY
{ ((D 0 THENA Auto) THEN Eliminate ⌜m9⌝⋅) }

1
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

---

Latex:

---

Latex:

1.  m4  :  \mBbbZ{}\msupminus{}\msupzero{}
2.  m5  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
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  =  m9)
10.  m7  \mleq{}\_lex  m9  =  tt
\mvdash{}  \mneg{}(m5  =  m9)


By

---

Latex:
((D  0  THENA  Auto)  THEN  Eliminate  \mkleeneopen{}m9\mkleeneclose{}\mcdot{})

---

Home Index