---

Step * 1 1 2 2 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. a1 : formula()
6. (a1 ⊆ x ∧ prank(a1) < n) ⇒ extend-val(v0;f;a1) = extend-val(v0;λa.extend-val(v0;f;a);a1)
⊢ (pnot(a1) ⊆ x
∧ formula_ind(a1;
              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;pnot(a1)) = extend-val(v0;λa.extend-val(v0;f;a);pnot(a1))
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
               Auto)
   THEN (GenConclAtAddrType ⌜bdd-val(v0;x;n - 1)⌝ [2;1]⋅ THENA Auto)
   THEN D -2
   THEN BHyp -2
   THEN (MemTypeCD THEN Auto)
   THEN (InstLemma `psub_transitivity` [⌜a1⌝; ⌜pnot(a1)⌝; ⌜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.  a1  :  formula()
6.  (a1  \msubseteq{}  x  \mwedge{}  prank(a1)  <  n)  {}\mRightarrow{}  extend-val(v0;f;a1)  =  extend-val(v0;\mlambda{}a.extend-val(v0;f;a);a1)
\mvdash{}  (pnot(a1)  \msubseteq{}  x
\mwedge{}  formula\_ind(a1;
                            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;pnot(a1))  =  extend-val(v0;\mlambda{}a.extend-val(v0;f;a);pnot(a1))


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
                          Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}bdd-val(v0;x;n  -  1)\mkleeneclose{}  [2;1]\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  BHyp  -2
  THEN  (MemTypeCD  THEN  Auto)
  THEN  (InstLemma  `psub\_transitivity`  [\mkleeneopen{}a1\mkleeneclose{};  \mkleeneopen{}pnot(a1)\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