---

Step * 1 of Lemma intlex-cons-same


1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. ||l1|| < ||l2|| ∨ (x < x ∧ (||l1|| = ||l2|| ∈ ℤ)) ∨ ((x = x ∈ ℤ) ∧ (↑l1 ≤_lex l2))
⊢ ↑l1 ≤_lex l2
BY
{ (SplitOrHyps THEN Auto) }

1
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. ||l1|| < ||l2||
⊢ ↑l1 ≤_lex l2

---

Latex:

---

Latex:

1.  l1  :  \mBbbZ{}  List
2.  l2  :  \mBbbZ{}  List
3.  x  :  \mBbbZ{}
4.  ||l1||  <  ||l2||  \mvee{}  (x  <  x  \mwedge{}  (||l1||  =  ||l2||))  \mvee{}  ((x  =  x)  \mwedge{}  (\muparrow{}l1  \mleq{}\_lex  l2))
\mvdash{}  \muparrow{}l1  \mleq{}\_lex  l2


By

---

Latex:
(SplitOrHyps  THEN  Auto)

---

Home Index