---

Step * of Lemma shorten-tuple-split-tuple

∀[n:ℕ]. ∀[x:Top].  (shorten-tuple(x;n) ~ snd(split-tuple(x;n)))
BY
{ (InductionOnNat
   THEN RecUnfold `shorten-tuple` 0
   THEN RecUnfold `split-tuple` 0
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 3 (OldAutoSplit)
   THEN (RWO "3" 0 THENA Auto)) }

1
1. n : ℤ
2. 0 < n
3. ∀[x:Top]. (shorten-tuple(x;n - 1) ~ snd(split-tuple(x;n - 1)))
4. x : Top
5. 0 < n
6. ¬(n = 0 ∈ ℤ)
7. n = 1 ∈ ℤ
⊢ snd(split-tuple(snd(x);n - 1)) ~ snd(x)

2
1. n : ℤ
2. 0 < n
3. ∀[x:Top]. (shorten-tuple(x;n - 1) ~ snd(split-tuple(x;n - 1)))
4. x : Top
5. 0 < n
6. ¬(n = 0 ∈ ℤ)
7. ¬(n = 1 ∈ ℤ)
⊢ snd(split-tuple(snd(x);n - 1)) ~ snd(let a,b = split-tuple(snd(x);n - 1) 
                                       in <<fst(x), a>, b>)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:Top].    (shorten-tuple(x;n)  \msim{}  snd(split-tuple(x;n)))


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `shorten-tuple`  0
  THEN  RecUnfold  `split-tuple`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  3  (OldAutoSplit)
  THEN  (RWO  "3"  0  THENA  Auto))

---

Home Index