---

Step * of Lemma intlex-aux-transitive

∀[l1:ℤ List]. ∀[l2,l3:{as:ℤ List| ||as|| = ||l1|| ∈ ℤ} ].
  (intlex-aux(l1;l3) = tt) supposing (intlex-aux(l2;l3) = tt and intlex-aux(l1;l2) = tt)
BY
{ (InductionOnList
   THEN Auto
   THEN RepeatFor 2 (DVar `l2')
   THEN All Reduce
   THEN Auto
   THEN Assert  ⌜0 ≤ ||v||⌝⋅
   THEN Auto
   THEN RepeatFor 2 (DVar `l3')
   THEN All Reduce
   THEN Auto
   THEN (RecUnfold `intlex-aux` (-3) THEN Reduce -3)
   THEN RecUnfold `intlex-aux` (-2)
   THEN Reduce -2
   THEN RecUnfold `intlex-aux` 0
   THEN Reduce 0) }

1
1. u : ℤ
2. v : ℤ List
3. ∀[l2,l3:{as:ℤ List| ||as|| = ||v|| ∈ ℤ} ].
     (intlex-aux(v;l3) = tt) supposing (intlex-aux(l2;l3) = tt and intlex-aux(v;l2) = tt)
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
7. u2 : ℤ
8. v2 : ℤ List
9. (||v2|| + 1) = (||v|| + 1) ∈ ℤ
10. if (u) < (u1)  then inl Ax  else if u=u1 then intlex-aux(v;v1) else (inr Ax ) = tt
11. if (u1) < (u2)  then inl Ax  else if u1=u2 then intlex-aux(v1;v2) else (inr Ax ) = tt
12. 0 ≤ ||v||
⊢ if (u) < (u2)  then inl Ax  else if u=u2 then intlex-aux(v;v2) else (inr Ax ) = tt

---

Latex:

---

Latex:
\mforall{}[l1:\mBbbZ{}  List].  \mforall{}[l2,l3:\{as:\mBbbZ{}  List|  ||as||  =  ||l1||\}  ].
    (intlex-aux(l1;l3)  =  tt)  supposing  (intlex-aux(l2;l3)  =  tt  and  intlex-aux(l1;l2)  =  tt)


By

---

Latex:
(InductionOnList
  THEN  Auto
  THEN  RepeatFor  2  (DVar  `l2')
  THEN  All  Reduce
  THEN  Auto
  THEN  Assert    \mkleeneopen{}0  \mleq{}  ||v||\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  (DVar  `l3')
  THEN  All  Reduce
  THEN  Auto
  THEN  (RecUnfold  `intlex-aux`  (-3)  THEN  Reduce  -3)
  THEN  RecUnfold  `intlex-aux`  (-2)
  THEN  Reduce  -2
  THEN  RecUnfold  `intlex-aux`  0
  THEN  Reduce  0)

---

Home Index