---

Step * of Lemma reg-seq-list-add_wf

∀[L:ℝ List]. (reg-seq-list-add(L) ∈ {f:ℕ+ ⟶ ℤ| ||L||-regular-seq(f)} )
BY
{ (Auto THEN MemTypeCD THEN Auto) }

1
1. L : ℝ List
⊢ reg-seq-list-add(L) ∈ ℕ+ ⟶ ℤ

2
.....set predicate..... 
1. L : ℝ List
⊢ ||L||-regular-seq(reg-seq-list-add(L))

---

Latex:

---

Latex:
\mforall{}[L:\mBbbR{}  List].  (reg-seq-list-add(L)  \mmember{}  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  ||L||-regular-seq(f)\}  )


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index