---

Step * 1 of Lemma intlex-antisym


1. l1 : ℤ List
2. l2 : ℤ List
3. ||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)) = tt
4. ||l2|| <z ||l1|| ∨b((||l2|| =z ||l1||) ∧b intlex-aux(l2;l1)) = tt
⊢ l1 = l2 ∈ (ℤ List)
BY
{ (MoveToConcl (-1) THEN (BoolCase ⌜||l2|| <z ||l1||⌝⋅ THENA Auto)) }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)  THEN  (BoolCase  \mkleeneopen{}||l2||  <z  ||l1||\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index