---

Step * of Lemma intlex-cons

∀l1,l2:ℤ List. ∀x,y:ℤ.
  uiff(↑[x / l1] ≤_lex [y / l2];||l1|| < ||l2|| ∨ (x < y ∧ (||l1|| = ||l2|| ∈ ℤ)) ∨ ((x = y ∈ ℤ) ∧ (↑l1 ≤_lex l2)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `intlex` 0
   THEN Reduce 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (Decide ||l1|| < ||l2|| THENA Auto)) }

1
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. ||l1|| < ||l2||
⊢ uiff(↑(||l1|| + 1 <z ||l2|| + 1 ∨b((||l1|| + 1 =z ||l2|| + 1) ∧b intlex-aux([x / l1];[y / l2])));||l1|| < ||l2||
∨ (x < y ∧ (||l1|| = ||l2|| ∈ ℤ))
∨ ((x = y ∈ ℤ) ∧ (↑(||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2))))))

2
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. ¬||l1|| < ||l2||
⊢ uiff(↑(||l1|| + 1 <z ||l2|| + 1 ∨b((||l1|| + 1 =z ||l2|| + 1) ∧b intlex-aux([x / l1];[y / l2])));||l1|| < ||l2||
∨ (x < y ∧ (||l1|| = ||l2|| ∈ ℤ))
∨ ((x = y ∈ ℤ) ∧ (↑(||l1|| <z ||l2|| ∨b((||l1|| =z ||l2||) ∧b intlex-aux(l1;l2))))))

---

Latex:

---

Latex:
\mforall{}l1,l2:\mBbbZ{}  List.  \mforall{}x,y:\mBbbZ{}.
    uiff(\muparrow{}[x  /  l1]  \mleq{}\_lex  [y  /  l2];||l1||  <  ||l2||
    \mvee{}  (x  <  y  \mwedge{}  (||l1||  =  ||l2||))
    \mvee{}  ((x  =  y)  \mwedge{}  (\muparrow{}l1  \mleq{}\_lex  l2)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `intlex`  0
  THEN  Reduce  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (Decide  ||l1||  <  ||l2||  THENA  Auto))

---

Home Index