---

Step * 1 1 2 4 3 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. por(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)
⊢ a2 ⊆ x
BY
{ ((InstLemma `psub_transitivity` [⌜a2⌝; ⌜por(left;a2)⌝; ⌜x⌝]⋅ THEN Auto)
   THEN Unfold `psub` 0
   THEN Reduce 0
   THEN Fold `psub` 0
   THEN RWO "psub-same" 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.  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.  por(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
\mvdash{}  a2  \msubseteq{}  x


By

---

Latex:
((InstLemma  `psub\_transitivity`  [\mkleeneopen{}a2\mkleeneclose{};  \mkleeneopen{}por(left;a2)\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  Unfold  `psub`  0
  THEN  Reduce  0
  THEN  Fold  `psub`  0
  THEN  RWO  "psub-same"  0
  THEN  Auto)

---

Home Index