---

Step * 2 1 1 of Lemma intlex-cons


1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. ¬||l1|| < ||l2||
6. ||l1|| = ||l2|| ∈ ℤ
⊢ uiff(↑intlex-aux([x / l1];[y / l2]);||l1|| < ||l2||
∨ (x < y ∧ (||l1|| = ||l2|| ∈ ℤ))
∨ ((x = y ∈ ℤ) ∧ (↑intlex-aux(l1;l2))))
BY
{ ((RW (AddrC [1;1] (RecUnfoldC `intlex-aux`)) 0 THEN Reduce 0)
   THEN RepeatFor 2 (AutoSplit)
   THEN Auto
   THEN SplitOrHyps
   THEN Auto) }

1
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. x ≠ y
6. ¬x < y
7. ¬||l1|| < ||l2||
8. ||l1|| = ||l2|| ∈ ℤ
9. ↑(inr Ax )
⊢ x = y ∈ ℤ

---

Latex:

---

Latex:

1.  l1  :  \mBbbZ{}  List
2.  l2  :  \mBbbZ{}  List
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  \mneg{}||l1||  <  ||l2||
6.  ||l1||  =  ||l2||
\mvdash{}  uiff(\muparrow{}intlex-aux([x  /  l1];[y  /  l2]);||l1||  <  ||l2||
\mvee{}  (x  <  y  \mwedge{}  (||l1||  =  ||l2||))
\mvee{}  ((x  =  y)  \mwedge{}  (\muparrow{}intlex-aux(l1;l2))))


By

---

Latex:
((RW  (AddrC  [1;1]  (RecUnfoldC  `intlex-aux`))  0  THEN  Reduce  0)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index