---

Step * 1 2 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)
⊢ 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
BY
{ ((DVar `v' THEN All Reduce THEN Auto)
   THEN DVar `x'
   THEN RecUnfold `split-tuple` 0
   THEN Reduce 0
   THEN AutoBoolCase ⌜(n =z 0)⌝⋅
   THEN AutoBoolCase ⌜(n =z 1)⌝⋅
   THEN Try ((AutoSplit THEN Auto')⋅)) }

1
1. u : Type
2. u1 : Type
3. v : Type List
4. ∀[x:if null(v) then u1 else u1 × tuple-type(v) fi ]. ∀[n:ℕ||v|| + 1].
     (append-tuple(n;(||v|| + 1) - n;fst(split-tuple(x;n));snd(split-tuple(x;n))) ~ x)
5. x1 : u
6. x2 : if null(v) then u1 else u1 × tuple-type(v) fi 
7. n : ℕ(||v|| + 1) + 1
8. n ≠ 1
9. n ≠ 0
10. ¬(n ≤ 0)
⊢ let a,b = fst(let a,b = split-tuple(x2;n - 1) 
                in <<x1, a>, b>) 
  in <a, append-tuple(n - 1;((||v|| + 1) + 1) - n;b;snd(let a,b = split-tuple(x2;n - 1) in <<x1, a>, b>))> ~ <x1, x2>

---

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.  \mneg{}(n  \mleq{}  0)
\mvdash{}  if  (n  =\msubz{}  1)
then  if  (||v||  +  1)  -  n  \mleq{}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    \msim{}  x


By

---

Latex:
((DVar  `v'  THEN  All  Reduce  THEN  Auto)
  THEN  DVar  `x'
  THEN  RecUnfold  `split-tuple`  0
  THEN  Reduce  0
  THEN  AutoBoolCase  \mkleeneopen{}(n  =\msubz{}  0)\mkleeneclose{}\mcdot{}
  THEN  AutoBoolCase  \mkleeneopen{}(n  =\msubz{}  1)\mkleeneclose{}\mcdot{}
  THEN  Try  ((AutoSplit  THEN  Auto')\mcdot{}))

---

Home Index