---

Step * 1 1 of Lemma valuation-exists


1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. [n] : ℕ
4. ∀[m:ℕn]. bdd-val(v0;x;m)
⊢ bdd-val(v0;x;n)
BY
{ (RenameVar `f' (-1) THEN With ⌜λa.extend-val(v0;f;a)⌝ (D 0)⋅ THEN Reduce 0) }

1
.....wf..... 
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : ∀[m:ℕn]. bdd-val(v0;x;m)
⊢ λa.extend-val(v0;f;a) ∈ {a:formula()| a ⊆ x ∧ prank(a) < n}  ⟶ 𝔹

2
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : ∀[m:ℕn]. bdd-val(v0;x;m)
⊢ ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n} . extend-val(v0;f;a) = extend-val(v0;λa.extend-val(v0;f;a);a)

3
.....wf..... 
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : ∀[m:ℕn]. bdd-val(v0;x;m)
5. f1 : {a:formula()| a ⊆ x ∧ prank(a) < n}  ⟶ 𝔹
⊢ istype(∀a:{a:formula()| a ⊆ x ∧ prank(a) < n} . f1 a = extend-val(v0;f1;a))

---

Latex:

---

Latex:

1.  x  :  formula()
2.  v0  :  \{a:formula()|  a  \msubseteq{}  x  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}
3.  [n]  :  \mBbbN{}
4.  \mforall{}[m:\mBbbN{}n].  bdd-val(v0;x;m)
\mvdash{}  bdd-val(v0;x;n)


By

---

Latex:
(RenameVar  `f'  (-1)  THEN  With  \mkleeneopen{}\mlambda{}a.extend-val(v0;f;a)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0)

---

Home Index