---

Step * of Lemma bfs-reduce_wf

∀[K:RngSig]. ∀[S:Type]. ∀[as,bs:basic-formal-sum(K;S)].  (bfs-reduce(K;S;as;bs) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[S:Type].  \mforall{}[as,bs:basic-formal-sum(K;S)].    (bfs-reduce(K;S;as;bs)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index