---

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:


\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

ProveWfLemma

---

Home Index