---

Step * of Lemma firstn_append

∀[L1,L2:Top List]. ∀[n:ℕ||L1|| + 1].  (firstn(n;L1 @ L2) ~ firstn(n;L1))
BY
{ (InductionOnList THEN RecUnfold `firstn` 0 THEN Reduce 0) }

1
∀[L2:Top List]. ∀[n:ℕ1].  (case L2 of [] => [] | a::as' => if 0 <z n then [a / firstn(n - 1;as')] else [] fi  esac ~ [])

2
1. u : Top
2. v : Top List
3. ∀[L2:Top List]. ∀[n:ℕ||v|| + 1].  (firstn(n;v @ L2) ~ firstn(n;v))
⊢ ∀[L2:Top List]. ∀[n:ℕ(||v|| + 1) + 1].
    (if 0 <z n then [u / firstn(n - 1;v @ L2)] else [] fi  ~ if 0 <z n then [u / firstn(n - 1;v)] else [] fi )

---

Latex:

---

Latex:
\mforall{}[L1,L2:Top  List].  \mforall{}[n:\mBbbN{}||L1||  +  1].    (firstn(n;L1  @  L2)  \msim{}  firstn(n;L1))


By

---

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

---

Home Index