---

Step * 1 1 2 1 of Lemma valuation-exists


1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : ∀[m:ℕn]. bdd-val(v0;x;m)
5. sz : ℕ
6. ∀sz:ℕsz. ∀a:formula().
     (a ⊆ x ∧ prank(a) < n) ⇒ extend-val(v0;f;a) = extend-val(v0;λa.extend-val(v0;f;a);a) 
     supposing formula_size(a) ≤ sz
7. a1 : Atom
8. 0 ≤ sz
⊢ (pvar(a1) ⊆ x ∧ 0 < n) ⇒ extend-val(v0;f;pvar(a1)) = extend-val(v0;λa.extend-val(v0;f;a);pvar(a1))
BY
{ (D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  formula()
2.  v0  :  \{a:formula()|  a  \msubseteq{}  x  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}
3.  n  :  \mBbbN{}
4.  f  :  \mforall{}[m:\mBbbN{}n].  bdd-val(v0;x;m)
5.  sz  :  \mBbbN{}
6.  \mforall{}sz:\mBbbN{}sz.  \mforall{}a:formula().
          (a  \msubseteq{}  x  \mwedge{}  prank(a)  <  n)  {}\mRightarrow{}  extend-val(v0;f;a)  =  extend-val(v0;\mlambda{}a.extend-val(v0;f;a);a) 
          supposing  formula\_size(a)  \mleq{}  sz
7.  a1  :  Atom
8.  0  \mleq{}  sz
\mvdash{}  (pvar(a1)  \msubseteq{}  x  \mwedge{}  0  <  n)
{}\mRightarrow{}  extend-val(v0;f;pvar(a1))  =  extend-val(v0;\mlambda{}a.extend-val(v0;f;a);pvar(a1))


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index