Step
*
1
1
2
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)
⊢ (pand(left;a2) ⊆ x
∧ imax(formula_ind(left;
pvar(name)⇒ 0;
pnot(sub)⇒ rec1.rec1 + 1;
pand(left,right)⇒ rec2,rec3.imax(rec2;rec3) + 1;
por(left,right)⇒ rec4,rec5.imax(rec4;rec5) + 1;
pimp(left,right)⇒ rec6,rec7.imax(rec6;rec7) + 1) ;
formula_ind(a2;
pvar(name)⇒ 0;
pnot(sub)⇒ rec1.rec1 + 1;
pand(left,right)⇒ rec2,rec3.imax(rec2;rec3) + 1;
por(left,right)⇒ rec4,rec5.imax(rec4;rec5) + 1;
pimp(left,right)⇒ rec6,rec7.imax(rec6;rec7) + 1) )
+ 1 < n)
⇒ extend-val(v0;f;pand(left;a2)) = extend-val(v0;λa.extend-val(v0;f;a);pand(left;a2))
BY
{ (Fold `prank` 0⋅
THEN (D 0 THENA Auto)
THEN (RW (SubC (UnfoldTopC `extend-val`)) 0 THEN Reduce 0 THEN EqCD THEN Auto)
THEN (Assert 1 < n BY
((RWO "imax_unfold" 10 THEN Auto) THEN SplitOnHypITE 10 THEN Auto))
THEN (GenConclAtAddrType ⌜bdd-val(v0;x;n - 1)⌝ [2;1]⋅ THENA (With ⌜n - 1⌝ (DVar `f')⋅ THEN Auto))
THEN D (-2)
THEN BHyp -2
THEN MemTypeCD
THEN Auto) }
1
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. pand(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
2
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. pand(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. left ⊆ x
⊢ prank(left) < n - 1
3
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. pand(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
4
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. pand(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
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)
\mvdash{} (pand(left;a2) \msubseteq{} x
\mwedge{} imax(formula\_ind(left;
pvar(name){}\mRightarrow{} 0;
pnot(sub){}\mRightarrow{} rec1.rec1 + 1;
pand(left,right){}\mRightarrow{} rec2,rec3.imax(rec2;rec3) + 1;
por(left,right){}\mRightarrow{} rec4,rec5.imax(rec4;rec5) + 1;
pimp(left,right){}\mRightarrow{} rec6,rec7.imax(rec6;rec7) + 1) ;
formula\_ind(a2;
pvar(name){}\mRightarrow{} 0;
pnot(sub){}\mRightarrow{} rec1.rec1 + 1;
pand(left,right){}\mRightarrow{} rec2,rec3.imax(rec2;rec3) + 1;
por(left,right){}\mRightarrow{} rec4,rec5.imax(rec4;rec5) + 1;
pimp(left,right){}\mRightarrow{} rec6,rec7.imax(rec6;rec7) + 1) )
+ 1 < n)
{}\mRightarrow{} extend-val(v0;f;pand(left;a2)) = extend-val(v0;\mlambda{}a.extend-val(v0;f;a);pand(left;a2))
By
Latex:
(Fold `prank` 0\mcdot{}
THEN (D 0 THENA Auto)
THEN (RW (SubC (UnfoldTopC `extend-val`)) 0 THEN Reduce 0 THEN EqCD THEN Auto)
THEN (Assert 1 < n BY
((RWO "imax\_unfold" 10 THEN Auto) THEN SplitOnHypITE 10 THEN Auto))
THEN (GenConclAtAddrType \mkleeneopen{}bdd-val(v0;x;n - 1)\mkleeneclose{} [2;1]\mcdot{} THENA (With \mkleeneopen{}n - 1\mkleeneclose{} (DVar `f')\mcdot{} THEN Auto))
THEN D (-2)
THEN BHyp -2
THEN MemTypeCD
THEN Auto)
Home
Index