---

Step * of Lemma append_firstn_lastn_sq

∀[L:Top List]. ∀[n:ℕ||L|| + 1].  (L ~ firstn(n;L) @ nth_tl(n;L))
BY
{ (InductionOnList THEN Auto THEN Reduce 0 THEN Auto THEN RecUnfold `firstn` 0 THEN Reduce 0 THEN Auto THEN AutoSplit) }

1
1. u : Top
2. v : Top List
3. ∀[n:ℕ||v|| + 1]. (v ~ firstn(n;v) @ nth_tl(n;v))
4. n : ℕ||[u / v]|| + 1
5. 0 < n
⊢ [u / v] ~ [u / (firstn(n - 1;v) @ nth_tl(n;[u / v]))]

2
1. u : Top
2. v : Top List
3. ∀[n:ℕ||v|| + 1]. (v ~ firstn(n;v) @ nth_tl(n;v))
4. n : ℕ||[u / v]|| + 1
5. ¬0 < n
⊢ [u / v] ~ nth_tl(n;[u / v])

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[n:\mBbbN{}||L||  +  1].    (L  \msim{}  firstn(n;L)  @  nth\_tl(n;L))


By

---

Latex:
(InductionOnList
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto
  THEN  RecUnfold  `firstn`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index