---

Step * 1 1 2 5 4 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. left : formula()
6. a2 : formula()
7. (a2 ⊆ x ∧ prank(a2) < n) ⇒ extend-val(v0;f;a2) = extend-val(v0;λa.extend-val(v0;f;a);a2)
8. (left ⊆ x ∧ prank(left) < n) ⇒ extend-val(v0;f;left) = extend-val(v0;λa.extend-val(v0;f;a);left)
9. pimp(left;a2) ⊆ x
10. imax(prank(left);prank(a2)) + 1 < n
11. 1 < n
12. v : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
13. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . v a = extend-val(v0;v;a)
14. f = v ∈ bdd-val(v0;x;n - 1)
15. a2 ⊆ x
⊢ prank(a2) < n - 1
BY
{ ((RWO "imax_unfold" 10 THEN Auto) THEN SplitOnHypITE 10 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.  left  :  formula()
6.  a2  :  formula()
7.  (a2  \msubseteq{}  x  \mwedge{}  prank(a2)  <  n)  {}\mRightarrow{}  extend-val(v0;f;a2)  =  extend-val(v0;\mlambda{}a.extend-val(v0;f;a);a2)
8.  (left  \msubseteq{}  x  \mwedge{}  prank(left)  <  n)  {}\mRightarrow{}  extend-val(v0;f;left)  =  extend-val(v0;\mlambda{}a.extend-val(v0;f;a);left)
9.  pimp(left;a2)  \msubseteq{}  x
10.  imax(prank(left);prank(a2))  +  1  <  n
11.  1  <  n
12.  v  :  \{a:formula()|  a  \msubseteq{}  x  \mwedge{}  prank(a)  <  n  -  1\}    {}\mrightarrow{}  \mBbbB{}
13.  \mforall{}a:\{a:formula()|  a  \msubseteq{}  x  \mwedge{}  prank(a)  <  n  -  1\}  .  v  a  =  extend-val(v0;v;a)
14.  f  =  v
15.  a2  \msubseteq{}  x
\mvdash{}  prank(a2)  <  n  -  1


By

---

Latex:
((RWO  "imax\_unfold"  10  THEN  Auto)  THEN  SplitOnHypITE  10  THEN  Auto)

---

Home Index