---

Step * of Lemma intlex-total

∀as,bs:ℤ List.  ((↑as ≤_lex bs) ∨ (↑bs ≤_lex as))
BY
{ ((Auto THEN Unfold `intlex` 0)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN AutoBoolCase ⌜||as|| <z ||bs||⌝⋅
   THEN AutoBoolCase ⌜||bs|| <z ||as||⌝⋅) }

1
1. as : ℤ List
2. bs : ℤ List
3. ¬||bs|| < ||as||
4. ¬||as|| < ||bs||
⊢ (↑((||as|| =z ||bs||) ∧b intlex-aux(as;bs))) ∨ (↑((||bs|| =z ||as||) ∧b intlex-aux(bs;as)))

---

Latex:

---

Latex:
\mforall{}as,bs:\mBbbZ{}  List.    ((\muparrow{}as  \mleq{}\_lex  bs)  \mvee{}  (\muparrow{}bs  \mleq{}\_lex  as))


By

---

Latex:
((Auto  THEN  Unfold  `intlex`  0)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  AutoBoolCase  \mkleeneopen{}||as||  <z  ||bs||\mkleeneclose{}\mcdot{}
  THEN  AutoBoolCase  \mkleeneopen{}||bs||  <z  ||as||\mkleeneclose{}\mcdot{})

---

Home Index