---

Step * 2 1 of Lemma not-imonomial-le


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
BY
{ Assert ⌜(↑a2 ≤_lex b2) ∨ (↑b2 ≤_lex a2)⌝⋅ }

1
.....assertion..... 
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))
⊢ (↑a2 ≤_lex b2) ∨ (↑b2 ≤_lex a2)

2
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))
9. (↑a2 ≤_lex b2) ∨ (↑b2 ≤_lex a2)
⊢ ↑b2 ≤_lex a2

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}(\muparrow{}a2  \mleq{}\_lex  b2)  \mvee{}  (\muparrow{}b2  \mleq{}\_lex  a2)\mkleeneclose{}\mcdot{}

---

Home Index