---

Step * of Lemma intlex-length

∀[l1,l2:ℤ List].  ||l1|| ≤ ||l2|| supposing ↑l1 ≤_lex l2
BY
{ ((Auto THEN Unfold `intlex` -1) THEN RepeatFor 2 ((CallByValueReduce (-1) THENA Auto))) }

1
1. l1 : ℤ List
2. l2 : ℤ List
3. ↑(||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)))
⊢ ||l1|| ≤ ||l2||

---

Latex:

---

Latex:
\mforall{}[l1,l2:\mBbbZ{}  List].    ||l1||  \mleq{}  ||l2||  supposing  \muparrow{}l1  \mleq{}\_lex  l2


By

---

Latex:
((Auto  THEN  Unfold  `intlex`  -1)  THEN  RepeatFor  2  ((CallByValueReduce  (-1)  THENA  Auto)))

---

Home Index