---

Step * of Lemma init-seg-nat-seq_wf

∀[f,g:finite-nat-seq()].  (init-seg-nat-seq(f;g) ∈ 𝔹)
BY
{ ProveWfLemma }

1
1. n : ℕ
2. f1 : ℕn ⟶ ℕ
3. n1 : ℕ
4. g1 : ℕn1 ⟶ ℕ
5. ble(n;n1) ∈ 𝔹
6. ↑ble(n;n1)
⊢ g1 ∈ ℕn ⟶ ℕ

---

Latex:

---

Latex:
\mforall{}[f,g:finite-nat-seq()].    (init-seg-nat-seq(f;g)  \mmember{}  \mBbbB{})


By

---

Latex:
ProveWfLemma

---

Home Index