---

Step * 1 1 of Lemma intlex-total


1. as : ℤ List
2. bs : ℤ List
3. ¬||bs|| < ||as||
4. ¬||as|| < ||bs||
5. ||as|| = ||bs|| ∈ ℤ
6. ||bs|| = ||as|| ∈ ℤ
⊢ (↑intlex-aux(as;bs)) ∨ (↑intlex-aux(bs;as))
BY
{ RepeatFor 3 (Thin (-2)) }

1
1. as : ℤ List
2. bs : ℤ List
3. ||bs|| = ||as|| ∈ ℤ
⊢ (↑intlex-aux(as;bs)) ∨ (↑intlex-aux(bs;as))

---

Latex:

---

Latex:

1.  as  :  \mBbbZ{}  List
2.  bs  :  \mBbbZ{}  List
3.  \mneg{}||bs||  <  ||as||
4.  \mneg{}||as||  <  ||bs||
5.  ||as||  =  ||bs||
6.  ||bs||  =  ||as||
\mvdash{}  (\muparrow{}intlex-aux(as;bs))  \mvee{}  (\muparrow{}intlex-aux(bs;as))


By

---

Latex:
RepeatFor  3  (Thin  (-2))

---

Home Index