---

Step * of Lemma shorten-tuple-append-tuple

∀[L1,L2:Type List].
  ∀[x:tuple-type(L1)]. ∀[y:tuple-type(L2)].
    (shorten-tuple(append-tuple(||L1||;||L2||;x;y);||L1||) = y ∈ tuple-type(L2)) 
  supposing 0 < ||L2||
BY
{ (Auto THEN (RWO "shorten-tuple-split-tuple" 0 THENA Auto) THEN RWO "split-tuple-append-tuple" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RWO  "shorten-tuple-split-tuple"  0  THENA  Auto)
  THEN  RWO  "split-tuple-append-tuple"  0
  THEN  Auto)

---

Home Index