---

Step * of Lemma ap2-tuple-as-tuple

∀[n:ℕ]. ∀[f,t:n-tuple(n)]. ∀[x:Top].  (ap2-tuple(n;f;x;t) ~ tuple(n;i.f.i x t.i))
BY
{ (InductionOnNat
   THEN (RWO "n-tuple-decomp tuple-decomp" 0 THENA Auto)
   THEN RecUnfold `ap2-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 `f' THEN DVar `t')
   THEN Reduce 0
   THEN Unfold `tuple` 0
   THEN EqCD
   THEN Try (Trivial)
   THEN GenConclAtAddr [1;2]⋅
   THEN (Thin (-1)
         THEN ListInd (-1)
         THEN Reduce 0
         THEN Try (Trivial)
         THEN EqCD
         THEN Try (Trivial)
         THEN (RW (AddrC [2] (RecUnfoldC `select-tuple`)) 0⋅ THEN AutoSplit)⋅)⋅) }

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  (RWO  "n-tuple-decomp  tuple-decomp"  0  THENA  Auto)
  THEN  RecUnfold  `ap2-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  `f'  THEN  DVar  `t')
  THEN  Reduce  0
  THEN  Unfold  `tuple`  0
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  GenConclAtAddr  [1;2]\mcdot{}
  THEN  (Thin  (-1)
              THEN  ListInd  (-1)
              THEN  Reduce  0
              THEN  Try  (Trivial)
              THEN  EqCD
              THEN  Try  (Trivial)
              THEN  (RW  (AddrC  [2]  (RecUnfoldC  `select-tuple`))  0\mcdot{}  THEN  AutoSplit)\mcdot{})\mcdot{})

---

Home Index