---

Step * of Lemma map-tuple-as-tuple

∀[n:ℕ]. ∀[f:Top]. ∀[t:n-tuple(n)].  (map-tuple(n;f;t) ~ tuple(n;i.f t.i))
BY
{ (InductionOnNat
   THEN (RWO "n-tuple-decomp tuple-decomp" 0 THENA Auto)
   THEN RecUnfold `map-tuple` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 (AutoSplit)
   THEN Auto
   THEN Try ((RecUnfold `select-tuple` 0 THEN Reduce 0 THEN Complete (AutoSplit))⋅)
   THEN (RWO "5" 0 THENA Auto)
   THEN (DVar `t'
         THEN Reduce 0
         THEN Unfold `tuple` 0
         THEN EqCD
         THEN Try (Trivial)
         THEN GenConclAtAddr [1;2]⋅
         THEN Thin (-1)⋅)⋅) }

1
1. n : ℤ
2. n ≠ 1
3. n ≠ 0
4. 0 < n
5. ∀[f:Top]. ∀[t:n-tuple(n - 1)].  (map-tuple(n - 1;f;t) ~ tuple(n - 1;i.f t.i))
6. f : Top
7. t1 : Top
8. t2 : n-tuple(n - 1)
9. v : ℕn - 1 List
⊢ map(λi.(f t2.i);v) ~ map(λi.(f <t1, t2>.i + 1);v)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:Top].  \mforall{}[t:n-tuple(n)].    (map-tuple(n;f;t)  \msim{}  tuple(n;i.f  t.i))


By

---

Latex:
(InductionOnNat
  THEN  (RWO  "n-tuple-decomp  tuple-decomp"  0  THENA  Auto)
  THEN  RecUnfold  `map-tuple`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Auto
  THEN  Try  ((RecUnfold  `select-tuple`  0  THEN  Reduce  0  THEN  Complete  (AutoSplit))\mcdot{})
  THEN  (RWO  "5"  0  THENA  Auto)
  THEN  (DVar  `t'
              THEN  Reduce  0
              THEN  Unfold  `tuple`  0
              THEN  EqCD
              THEN  Try  (Trivial)
              THEN  GenConclAtAddr  [1;2]\mcdot{}
              THEN  Thin  (-1)\mcdot{})\mcdot{})

---

Home Index