---

Step * of Lemma intlex-transitive

∀[l1,l2,l3:ℤ List].  (l1 ≤_lex l3 = tt) supposing (l2 ≤_lex l3 = tt and l1 ≤_lex l2 = tt)
BY
{ (Auto
   THEN ∀h:hyp. (Unfold `intlex` h THEN RepeatFor 2 ((CallByValueReduce h THENA Auto))) 
   THEN Unfold `intlex` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. l1 : ℤ List
2. l2 : ℤ List
3. l3 : ℤ List
4. ||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)) = tt
5. ||l2|| <z ||l3|| ∨b((||l2|| =z ||l3||) ∧b intlex-aux(l2;l3)) = tt
⊢ ||l1|| <z ||l3|| ∨b((||l1|| =z ||l3||) ∧b intlex-aux(l1;l3)) = tt

---

Latex:

---

Latex:
\mforall{}[l1,l2,l3:\mBbbZ{}  List].    (l1  \mleq{}\_lex  l3  =  tt)  supposing  (l2  \mleq{}\_lex  l3  =  tt  and  l1  \mleq{}\_lex  l2  =  tt)


By

---

Latex:
(Auto
  THEN  \mforall{}h:hyp.  (Unfold  `intlex`  h  THEN  RepeatFor  2  ((CallByValueReduce  h  THENA  Auto))) 
  THEN  Unfold  `intlex`  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index