---

Step * 1 1 of Lemma append-tuple-split-tuple


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
6. n ≤ 0
⊢ snd(split-tuple(x;n)) ~ x
BY
{ (RecUnfold `split-tuple` 0 THEN AutoSplit)⋅ }

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mforall{}[x:tuple-type(v)].  \mforall{}[n:\mBbbN{}||v||].
          (append-tuple(n;||v||  -  n;fst(split-tuple(x;n));snd(split-tuple(x;n)))  \msim{}  x)
4.  x  :  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi 
5.  n  :  \mBbbN{}||v||  +  1
6.  n  \mleq{}  0
\mvdash{}  snd(split-tuple(x;n))  \msim{}  x


By

---

Latex:
(RecUnfold  `split-tuple`  0  THEN  AutoSplit)\mcdot{}

---

Home Index