Step
*
of Lemma
valuation-exists
No Annotations
∀x:formula(). ∀v0:{a:formula()| a ⊆ x ∧ (↑pvar?(a))} ⟶ 𝔹. (∃f:{a:formula()| a ⊆ x} ⟶ 𝔹 [valuation(v0;x;f)])
BY
{ TACTIC:((D 0 THEN Auto) THEN Assert ⌜∀[n:ℕ]. bdd-val(v0;x;n)⌝⋅) }
1
.....assertion.....
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))} ⟶ 𝔹
⊢ ∀[n:ℕ]. bdd-val(v0;x;n)
2
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))} ⟶ 𝔹
3. ∀[n:ℕ]. bdd-val(v0;x;n)
⊢ ∃f:{a:formula()| a ⊆ x} ⟶ 𝔹 [valuation(v0;x;f)]
Latex:
Latex:
No Annotations
\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:
TACTIC:((D 0 THEN Auto) THEN Assert \mkleeneopen{}\mforall{}[n:\mBbbN{}]. bdd-val(v0;x;n)\mkleeneclose{}\mcdot{})
Home
Index