---

Step * 1 1 2 1 2 1 1 1 2 of Lemma intlex-transitive


1. l1 : ℤ List
2. l2 : ℤ List
3. l3 : ℤ List
4. ||l1|| ≤ ||l2||
5. ||l2|| ≤ ||l3||
6. ¬||l1|| < ||l2||
7. ||l1|| = ||l2|| ∈ ℤ
8. intlex-aux(l1;l2) = tt
9. ¬||l2|| < ||l3||
10. ||l2|| = ||l3|| ∈ ℤ
11. intlex-aux(l2;l3) = tt
⊢ ||l1|| <z ||l1|| ∨b((||l1|| =z ||l1||) ∧b tt) = tt
BY
{ Auto }

---

Latex:

---

Latex:

1.  l1  :  \mBbbZ{}  List
2.  l2  :  \mBbbZ{}  List
3.  l3  :  \mBbbZ{}  List
4.  ||l1||  \mleq{}  ||l2||
5.  ||l2||  \mleq{}  ||l3||
6.  \mneg{}||l1||  <  ||l2||
7.  ||l1||  =  ||l2||
8.  intlex-aux(l1;l2)  =  tt
9.  \mneg{}||l2||  <  ||l3||
10.  ||l2||  =  ||l3||
11.  intlex-aux(l2;l3)  =  tt
\mvdash{}  ||l1||  <z  ||l1||  \mvee{}\msubb{}((||l1||  =\msubz{}  ||l1||)  \mwedge{}\msubb{}  tt)  =  tt


By

---

Latex:
Auto

---

Home Index