---

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


1. L : Type List
2. x : tuple-type(L)
3. n : ℕ||L||
4. append-tuple(n;||L|| - n;fst(split-tuple(x;n));snd(split-tuple(x;n))) ~ x
⊢ shorten-tuple(x;n) ~ snd(split-tuple(x;n))
BY
{ (RWO "shorten-tuple-split-tuple" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  Type  List
2.  x  :  tuple-type(L)
3.  n  :  \mBbbN{}||L||
4.  append-tuple(n;||L||  -  n;fst(split-tuple(x;n));snd(split-tuple(x;n)))  \msim{}  x
\mvdash{}  shorten-tuple(x;n)  \msim{}  snd(split-tuple(x;n))


By

---

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

---

Home Index