---

Step * of Lemma last-solution_wf

∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[d:a:E ⟶ Dec(P[a])].  (last-solution(es;P;d) ∈ E ⟶ (E + Top))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:a:E  {}\mrightarrow{}  Dec(P[a])].    (last-solution(es;P;d)  \mmember{}  E  {}\mrightarrow{}  (E  +  Top))


By

---

Latex:
ProveWfLemma

---

Home Index