---

Step * 1 1 of Lemma ap-tuple-as-tuple


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. f1 : Top
6. f2 : n-tuple(n - 1)
7. t1 : Top
8. t2 : n-tuple(n - 1)
⊢ map(λi.(f2.i t2.i);upto(n - 1)) ~ map(λi.(<f1, f2>.i + 1 <t1, t2>.i + 1);upto(n - 1))
BY
{ (RW (AddrC [2] (RecUnfoldC `select-tuple`)) 0
   THEN Reduce 0
   THEN GenConclAtAddr [1;2]⋅
   THEN Thin (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Try (Trivial)
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  n  \mneq{}  1
3.  0  <  n
4.  \mforall{}[f,t:n-tuple(n  -  1)].    (ap-tuple(n  -  1;f;t)  \msim{}  tuple(n  -  1;i.f.i  t.i))
5.  f1  :  Top
6.  f2  :  n-tuple(n  -  1)
7.  t1  :  Top
8.  t2  :  n-tuple(n  -  1)
\mvdash{}  map(\mlambda{}i.(f2.i  t2.i);upto(n  -  1))  \msim{}  map(\mlambda{}i.(<f1,  f2>.i  +  1  <t1,  t2>.i  +  1);upto(n  -  1))


By

---

Latex:
(RW  (AddrC  [2]  (RecUnfoldC  `select-tuple`))  0
  THEN  Reduce  0
  THEN  GenConclAtAddr  [1;2]\mcdot{}
  THEN  Thin  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  AutoSplit)

---

Home Index