---

Step * of Lemma valuation_wf

∀[x:formula()]. ∀[v0:{a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹]. ∀[f:{a:formula()| a ⊆ x}  ⟶ 𝔹].  (valuation(v0;x;f) ∈ ℙ\000C)
BY
{ (ProveWfLemma THEN (DoSubsume THEN Auto THEN (SubtypeReasoning THENM RelRST) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[x:formula()].  \mforall{}[v0:\{a:formula()|  a  \msubseteq{}  x  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{a:formula()|  a  \msubseteq{}  x\}    {}\mrightarrow{}  \mBbbB{}].
    (valuation(v0;x;f)  \mmember{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma  THEN  (DoSubsume  THEN  Auto  THEN  (SubtypeReasoning  THENM  RelRST)  THEN  Auto)\mcdot{})

---

Home Index