---

Step * of Lemma intlex-aux-antisym

∀[l1:ℤ List]. ∀[l2:{as:ℤ List| ||as|| = ||l1|| ∈ ℤ} ].
  (l1 = l2 ∈ (ℤ List)) supposing (intlex-aux(l2;l1) = 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) }

1
1. u : ℤ
2. v : ℤ List
3. ∀[l2:{as:ℤ List| ||as|| = ||v|| ∈ ℤ} ]
     (v = l2 ∈ (ℤ List)) supposing (intlex-aux(l2;v) = tt and intlex-aux(v;l2) = tt)
4. u1 : ℤ
5. v1 : ℤ List
6. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
7. intlex-aux([u / v];[u1 / v1]) = tt
8. intlex-aux([u1 / v1];[u / v]) = tt
9. 0 ≤ ||v||
⊢ [u / v] = [u1 / v1] ∈ (ℤ List)

---

Latex:

---

Latex:
\mforall{}[l1:\mBbbZ{}  List].  \mforall{}[l2:\{as:\mBbbZ{}  List|  ||as||  =  ||l1||\}  ].
    (l1  =  l2)  supposing  (intlex-aux(l2;l1)  =  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)

---

Home Index