---

Step * 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. ¬((snd(<m4, m5>)) = (snd(<m6, m7>)) ∈ (ℤ List))
8. m5 ≤_lex m7 = tt
9. ¬((snd(<m6, m7>)) = (snd(<m8, m9>)) ∈ (ℤ List))
10. m7 ≤_lex m9 = tt
⊢ ¬((snd(<m4, m5>)) = (snd(<m8, m9>)) ∈ (ℤ List))
BY
{ All Reduce  }

1
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))

---

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{}((snd(<m4,  m5>))  =  (snd(<m6,  m7>)))
8.  m5  \mleq{}\_lex  m7  =  tt
9.  \mneg{}((snd(<m6,  m7>))  =  (snd(<m8,  m9>)))
10.  m7  \mleq{}\_lex  m9  =  tt
\mvdash{}  \mneg{}((snd(<m4,  m5>))  =  (snd(<m8,  m9>)))


By

---

Latex:
All  Reduce 

---

Home Index