---

Step * 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. 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)
BY
{ ((RWO "4" 0 THENA Auto) THEN DProds THEN Reduce 0 THEN (Unfold `tuple` 0⋅ THEN EqCD) THEN Try (Trivial)) }

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. 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))

---

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.  f  :  Top  \mtimes{}  n-tuple(n  -  1)
6.  t  :  Top  \mtimes{}  n-tuple(n  -  1)
\mvdash{}  ap-tuple(n  -  1;snd(f);snd(t))  \msim{}  tuple(n  -  1;i.f.i  +  1  t.i  +  1)


By

---

Latex:
((RWO  "4"  0  THENA  Auto)
  THEN  DProds
  THEN  Reduce  0
  THEN  (Unfold  `tuple`  0\mcdot{}  THEN  EqCD)
  THEN  Try  (Trivial))

---

Home Index