---

Step * 1 of Lemma intlex-length


1. l1 : ℤ List
2. l2 : ℤ List
3. ↑(||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)))
⊢ ||l1|| ≤ ||l2||
BY
{ (MoveToConcl (-1) THEN AutoBoolCase ⌜||l1|| <z ||l2||⌝⋅ THEN AutoBoolCase ⌜(||l1|| =z ||l2||)⌝⋅) }

---

Latex:

---

Latex:

1.  l1  :  \mBbbZ{}  List
2.  l2  :  \mBbbZ{}  List
3.  \muparrow{}(||l1||  <z  ||l2||  \mvee{}\msubb{}((||l1||  =\msubz{}  ||l2||)  \mwedge{}\msubb{}  intlex-aux(l1;l2)))
\mvdash{}  ||l1||  \mleq{}  ||l2||


By

---

Latex:
(MoveToConcl  (-1)  THEN  AutoBoolCase  \mkleeneopen{}||l1||  <z  ||l2||\mkleeneclose{}\mcdot{}  THEN  AutoBoolCase  \mkleeneopen{}(||l1||  =\msubz{}  ||l2||)\mkleeneclose{}\mcdot{})

---

Home Index