---

Step * 1 1 1 1 of Lemma intlex-total


1. u : ℤ
2. v : ℤ List
3. ∀bs:ℤ List. ((||bs|| = ||v|| ∈ ℤ) ⇒ ((↑intlex-aux(v;bs)) ∨ (↑intlex-aux(bs;v))))
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
⊢ (↑intlex-aux([u / v];[u1 / v1])) ∨ (↑intlex-aux([u1 / v1];[u / v]))
BY
{ ((RecUnfold `intlex-aux` 0 THEN Reduce 0) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}bs:\mBbbZ{}  List.  ((||bs||  =  ||v||)  {}\mRightarrow{}  ((\muparrow{}intlex-aux(v;bs))  \mvee{}  (\muparrow{}intlex-aux(bs;v))))
4.  u1  :  \mBbbZ{}
5.  v1  :  \mBbbZ{}  List
6.  (||v1||  +  1)  =  (||v||  +  1)
\mvdash{}  (\muparrow{}intlex-aux([u  /  v];[u1  /  v1]))  \mvee{}  (\muparrow{}intlex-aux([u1  /  v1];[u  /  v]))


By

---

Latex:
((RecUnfold  `intlex-aux`  0  THEN  Reduce  0)  THEN  AutoSplit)

---

Home Index