---

Step * 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
⊢ append-tuple(n;(||v|| + 1) - n;fst(split-tuple(x;n));snd(split-tuple(x;n))) ~ x
BY
{ (RecUnfold `append-tuple` 0 THEN AutoSplit) }

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
6. n ≤ 0
⊢ snd(split-tuple(x;n)) ~ x

2
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)
⊢ if (n =z 1)
then if (||v|| + 1) - n ≤z 0 then fst(split-tuple(x;n)) else <fst(split-tuple(x;n)), snd(split-tuple(x;n))> fi 
else let a,b = fst(split-tuple(x;n)) 
     in <a, append-tuple(n - 1;(||v|| + 1) - n;b;snd(split-tuple(x;n)))>
fi  ~ x

---

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
\mvdash{}  append-tuple(n;(||v||  +  1)  -  n;fst(split-tuple(x;n));snd(split-tuple(x;n)))  \msim{}  x


By

---

Latex:
(RecUnfold  `append-tuple`  0  THEN  AutoSplit)

---

Home Index