---

Step * of Lemma split-tuple-append-tuple

∀[L1,L2:Type List].
  ∀[x:tuple-type(L1)]. ∀[y:tuple-type(L2)].  (split-tuple(append-tuple(||L1||;||L2||;x;y);||L1||) ~ <x, y>) supposing 0 \000C< ||L2||
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

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)
⊢ split-tuple(append-tuple(||v|| + 1;||L2||;x;y);||v|| + 1) ~ <x, y>

---

Latex:

---

Latex:
\mforall{}[L1,L2:Type  List].
    \mforall{}[x:tuple-type(L1)].  \mforall{}[y:tuple-type(L2)].
        (split-tuple(append-tuple(||L1||;||L2||;x;y);||L1||)  \msim{}  <x,  y>) 
    supposing  0  <  ||L2||


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index