---

Step * of Lemma intlex-aux_wf

∀[l1:ℤ List]. ∀[l2:{as:ℤ List| ||as|| = ||l1|| ∈ ℤ} ].  (intlex-aux(l1;l2) ∈ 𝔹)
BY
{ (Assert ∀[n:ℕ]. ∀[l1,l2:{as:ℤ List| ||as|| = n ∈ ℤ} ].  (intlex-aux(l1;l2) ∈ 𝔹) BY
         (InductionOnNat
          THEN Auto
          THEN RecUnfold `intlex-aux` 0
          THEN Reduce 0
          THEN Auto
          THEN RepeatFor 2 (DVar `l1')
          THEN All Reduce
          THEN Auto
          THEN (Assert 0 ≤ ||v|| BY
                      Auto)
          THEN Auto
          THEN BackThruSomeHyp
          THEN All Reduce
          THEN MemTypeCD
          THEN Auto)) }

1
1. ∀[n:ℕ]. ∀[l1,l2:{as:ℤ List| ||as|| = n ∈ ℤ} ].  (intlex-aux(l1;l2) ∈ 𝔹)
⊢ ∀[l1:ℤ List]. ∀[l2:{as:ℤ List| ||as|| = ||l1|| ∈ ℤ} ].  (intlex-aux(l1;l2) ∈ 𝔹)

---

Latex:

---

Latex:
\mforall{}[l1:\mBbbZ{}  List].  \mforall{}[l2:\{as:\mBbbZ{}  List|  ||as||  =  ||l1||\}  ].    (intlex-aux(l1;l2)  \mmember{}  \mBbbB{})


By

---

Latex:
(Assert  \mforall{}[n:\mBbbN{}].  \mforall{}[l1,l2:\{as:\mBbbZ{}  List|  ||as||  =  n\}  ].    (intlex-aux(l1;l2)  \mmember{}  \mBbbB{})  BY
              (InductionOnNat
                THEN  Auto
                THEN  RecUnfold  `intlex-aux`  0
                THEN  Reduce  0
                THEN  Auto
                THEN  RepeatFor  2  (DVar  `l1')
                THEN  All  Reduce
                THEN  Auto
                THEN  (Assert  0  \mleq{}  ||v||  BY
                                        Auto)
                THEN  Auto
                THEN  BackThruSomeHyp
                THEN  All  Reduce
                THEN  MemTypeCD
                THEN  Auto))

---

Home Index