---

Step * of Lemma append-tuple-split-tuple

∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[n:ℕ||L||].
  (append-tuple(n;||L|| - n;fst(split-tuple(x;n));snd(split-tuple(x;n))) ~ x)
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. u : Type
2. v : Type List
3. ∀[x:tuple-type(v)]. ∀[n:ℕ||v||].  (append-tuple(n;||v|| - n;fst(split-tuple(x;n));snd(split-tuple(x;n))) ~ x)
4. x : if null(v) then u else u × tuple-type(v) fi 
5. n : ℕ||v|| + 1
⊢ append-tuple(n;(||v|| + 1) - n;fst(split-tuple(x;n));snd(split-tuple(x;n))) ~ x

---

Latex:

---

Latex:
\mforall{}[L:Type  List].  \mforall{}[x:tuple-type(L)].  \mforall{}[n:\mBbbN{}||L||].
    (append-tuple(n;||L||  -  n;fst(split-tuple(x;n));snd(split-tuple(x;n)))  \msim{}  x)


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index