---

Step * 2 of Lemma reg-seq-list-add_wf

.....set predicate..... 
1. L : ℝ List
⊢ ||L||-regular-seq(reg-seq-list-add(L))
BY
{ (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto) }

1
1. L : ℝ List
⊢ ||L||-regular-seq(λn.l_sum(map(λx.(x n);L)))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  L  :  \mBbbR{}  List
\mvdash{}  ||L||-regular-seq(reg-seq-list-add(L))


By

---

Latex:
(RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)

---

Home Index