---

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