---

Step * 1 1 1 1 1 1 of Lemma assert-init-seg-nat-seq


1. n : ℕ
2. k : ℕ
3. s : ℕn ⟶ ℕ
4. r : ℕn + k ⟶ ℕ
5. n + k ∈ ℕ
6. s = r ∈ (ℕn ⟶ ℕ)
⊢ <n + k, r> = <n, s>**λi.(r (i + n))^(k) ∈ finite-nat-seq()
BY
{ (RepUR ``append-finite-nat-seq finite-nat-seq mk-finite-nat-seq`` 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
4.  r  :  \mBbbN{}n  +  k  {}\mrightarrow{}  \mBbbN{}
5.  n  +  k  \mmember{}  \mBbbN{}
6.  s  =  r
\mvdash{}  <n  +  k,  r>  =  <n,  s>**\mlambda{}i.(r  (i  +  n))\^{}(k)


By

---

Latex:
(RepUR  ``append-finite-nat-seq  finite-nat-seq  mk-finite-nat-seq``  0  THEN  EqCD  THEN  Auto)

---

Home Index