---

Step * of Lemma ap-tuple-as-tuple

∀[n:ℕ]. ∀[f,t:n-tuple(n)].  (ap-tuple(n;f;t) ~ tuple(n;i.f.i t.i))
BY
{ (InductionOnNat
   THEN (RWO "n-tuple-decomp tuple-decomp" 0 THENA Auto)
   THEN RecUnfold `ap-tuple` 0
   THEN (OReduce 0 THENA Auto)
   THEN Try (Complete (Auto))
   THEN ((RW (SweepUpC OmegaC) 0 THENA Auto) THEN Reduce 0)
   THEN AutoSplit
   THEN Auto
   THEN Try ((RecUnfold `select-tuple` 0 THEN Reduce 0 THEN Complete (AutoSplit))⋅)) }

1
1. n : ℤ
2. n ≠ 1
3. 0 < n
4. ∀[f,t:n-tuple(n - 1)].  (ap-tuple(n - 1;f;t) ~ tuple(n - 1;i.f.i t.i))
5. f : Top × n-tuple(n - 1)
6. t : Top × n-tuple(n - 1)
⊢ ap-tuple(n - 1;snd(f);snd(t)) ~ tuple(n - 1;i.f.i + 1 t.i + 1)

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  (RWO  "n-tuple-decomp  tuple-decomp"  0  THENA  Auto)
  THEN  RecUnfold  `ap-tuple`  0
  THEN  (OReduce  0  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  ((RW  (SweepUpC  OmegaC)  0  THENA  Auto)  THEN  Reduce  0)
  THEN  AutoSplit
  THEN  Auto
  THEN  Try  ((RecUnfold  `select-tuple`  0  THEN  Reduce  0  THEN  Complete  (AutoSplit))\mcdot{}))

---

Home Index