---

Step * of Lemma valuation-exists-ext

∀x:formula(). ∀v0:{a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹.  (∃f:{a:formula()| a ⊆ x}  ⟶ 𝔹 [valuation(v0;x;f)])
BY
{ xxxNormalizeExtractTo (ioid Obid: valuation-exists) λx,v0. fix((λv,a. extend-val(v0;v;a))) 100 ``extend-val``  ⋅xxx }

---

Latex:

---

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


By

---

Latex:
xxxNormalizeExtractTo  (ioid  Obid:  valuation-exists)  \mlambda{}x,v0.  fix((\mlambda{}v,a.  extend-val(v0;v;a)))
  100  ``extend-val``    \mcdot{}xxx

---

Home Index