---

Step * 1 1 1 of Lemma intlex-total


1. as : ℤ List
2. bs : ℤ List
3. ||bs|| = ||as|| ∈ ℤ
⊢ (↑intlex-aux(as;bs)) ∨ (↑intlex-aux(bs;as))
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN ListInd 1 THEN Auto THEN DVar `bs' THEN All Reduce THEN Auto) }

1
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]))

---

Latex:

---

Latex:

1.  as  :  \mBbbZ{}  List
2.  bs  :  \mBbbZ{}  List
3.  ||bs||  =  ||as||
\mvdash{}  (\muparrow{}intlex-aux(as;bs))  \mvee{}  (\muparrow{}intlex-aux(bs;as))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))  THEN  ListInd  1  THEN  Auto  THEN  DVar  `bs'  THEN  All  Reduce  THEN  Auto)

---

Home Index