Step
*
1
1
2
5
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. 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)
β’ left β x
BY
{ ((InstLemma `psub_transitivity` [βleftβ; βpimp(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. 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
\mvdash{} left \msubseteq{} x
By
Latex:
((InstLemma `psub\_transitivity` [\mkleeneopen{}left\mkleeneclose{}; \mkleeneopen{}pimp(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