Step
*
2
2
1
of Lemma
intlex-cons
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. ¬||l1|| < ||l2||
6. ¬(||l1|| = ||l2|| ∈ ℤ)
7. (x < y ∧ (||l1|| = ||l2|| ∈ ℤ)) ∨ ((x = y ∈ ℤ) ∧ False)
⊢ False
BY
{ (D -1 THEN Auto) }
Latex:
Latex:
1. l1 : \mBbbZ{} List
2. l2 : \mBbbZ{} List
3. x : \mBbbZ{}
4. y : \mBbbZ{}
5. \mneg{}||l1|| < ||l2||
6. \mneg{}(||l1|| = ||l2||)
7. (x < y \mwedge{} (||l1|| = ||l2||)) \mvee{} ((x = y) \mwedge{} False)
\mvdash{} False
By
Latex:
(D -1 THEN Auto)
Home
Index