---

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


1. u : Type
2. v : Type List
3. ∀[L2:Type List]
     ∀[x:tuple-type(v)]. ∀[y:tuple-type(L2)].  (split-tuple(append-tuple(||v||;||L2||;x;y);||v||) ~ <x, y>) supposing 0 \000C< ||L2||
4. L2 : Type List
5. 0 < ||L2||
6. x : if null(v) then u else u × tuple-type(v) fi 
7. y : tuple-type(L2)
⊢ split-tuple(append-tuple(||v|| + 1;||L2||;x;y);||v|| + 1) ~ <x, y>
BY
{ ((RecUnfold `append-tuple` 0 THEN RecUnfold `split-tuple` 0) THEN AutoSplit) }

1
1. u : Type
2. v : Type List
3. ∀[L2:Type List]
     ∀[x:tuple-type(v)]. ∀[y:tuple-type(L2)].  (split-tuple(append-tuple(||v||;||L2||;x;y);||v||) ~ <x, y>) supposing 0 \000C< ||L2||
4. L2 : Type List
5. 0 < ||L2||
6. x : if null(v) then u else u × tuple-type(v) fi 
7. y : tuple-type(L2)
8. (||v|| + 1) = 0 ∈ ℤ
⊢ <⋅, y> ~ <x, y>

2
1. u : Type
2. v : Type List
3. ||v|| + 1 ≠ 0
4. ∀[L2:Type List]
     ∀[x:tuple-type(v)]. ∀[y:tuple-type(L2)].  (split-tuple(append-tuple(||v||;||L2||;x;y);||v||) ~ <x, y>) supposing 0 \000C< ||L2||
5. L2 : Type List
6. 0 < ||L2||
7. x : if null(v) then u else u × tuple-type(v) fi 
8. y : tuple-type(L2)
⊢ if (||v|| + 1 =z 1)
then <fst(if ||v|| + 1 ≤z 0 then y
      if (||v|| + 1 =z 1) then <x, y>
      else let a,b = x 
           in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
      fi )
     , snd(if ||v|| + 1 ≤z 0 then y
       if (||v|| + 1 =z 1) then <x, y>
       else let a,b = x 
            in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
       fi )
     >
else let a,b = split-tuple(snd(if ||v|| + 1 ≤z 0 then y
     if (||v|| + 1 =z 1) then <x, y>
     else let a,b = x 
          in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
     fi );(||v|| + 1) - 1) 
     in <<fst(if ||v|| + 1 ≤z 0 then y
          if (||v|| + 1 =z 1) then if ||L2|| ≤z 0 then x else <x, y> fi 
          else let a,b = x 
               in <a, append-tuple((||v|| + 1) - 1;||L2||;b;y)>
          fi )
         , a
         >
        , b
        >
fi  ~ <x, y>

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mforall{}[L2:Type  List]
          \mforall{}[x:tuple-type(v)].  \mforall{}[y:tuple-type(L2)].
              (split-tuple(append-tuple(||v||;||L2||;x;y);||v||)  \msim{}  <x,  y>) 
          supposing  0  <  ||L2||
4.  L2  :  Type  List
5.  0  <  ||L2||
6.  x  :  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi 
7.  y  :  tuple-type(L2)
\mvdash{}  split-tuple(append-tuple(||v||  +  1;||L2||;x;y);||v||  +  1)  \msim{}  <x,  y>


By

---

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

---

Home Index