Step
*
1
2
of Lemma
intlex-antisym
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))
BY
{ (BoolCase ⌜(||l2|| =z ||l1||)⌝⋅ THENA Auto) }
1
1. l1 : ℤ List
2. l2 : ℤ List
3. ¬||l2|| < ||l1||
4. ||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)) = tt
5. ||l2|| = ||l1|| ∈ ℤ
⊢ intlex-aux(l2;l1) = tt
⇒ (l1 = l2 ∈ (ℤ List))
2
1. l1 : ℤ List
2. l2 : ℤ List
3. ||l2|| ≠ ||l1||
4. ¬||l2|| < ||l1||
5. ||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2)) = tt
⊢ ff = tt
⇒ (l1 = l2 ∈ (ℤ List))
Latex:
Latex:
1. l1 : \mBbbZ{} List
2. l2 : \mBbbZ{} List
3. \mneg{}||l2|| < ||l1||
4. ||l1|| <z ||l2|| \mvee{}\msubb{}((||l1|| =\msubz{} ||l2||) \mwedge{}\msubb{} intlex-aux(l1;l2)) = tt
\mvdash{} (||l2|| =\msubz{} ||l1||) \mwedge{}\msubb{} intlex-aux(l2;l1) = tt {}\mRightarrow{} (l1 = l2)
By
Latex:
(BoolCase \mkleeneopen{}(||l2|| =\msubz{} ||l1||)\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index