---

Step * 1 1 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)
⊢ ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n} . extend-val(v0;f;a) = extend-val(v0;λa.extend-val(v0;f;a);a)
BY
{ (Auto THEN D -1 THEN MoveToConcl (-1) THEN SimpleDatatypeInduction (-1) THEN Unfold `prank` 0 THEN Reduce 0) }

1
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : ∀[m:ℕn]. bdd-val(v0;x;m)
5. sz : ℕ
6. ∀sz:ℕsz. ∀a:formula().
     (a ⊆ x ∧ prank(a) < n) ⇒ extend-val(v0;f;a) = extend-val(v0;λa.extend-val(v0;f;a);a) 
     supposing formula_size(a) ≤ sz
7. a1 : Atom
8. 0 ≤ sz
⊢ (pvar(a1) ⊆ x ∧ 0 < n) ⇒ extend-val(v0;f;pvar(a1)) = extend-val(v0;λa.extend-val(v0;f;a);pvar(a1))

2
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))

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)
⊢ (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))

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)
⊢ (por(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;por(left;a2)) = extend-val(v0;λa.extend-val(v0;f;a);por(left;a2))

5
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)
⊢ (pimp(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;pimp(left;a2)) = extend-val(v0;λa.extend-val(v0;f;a);pimp(left;a2))

---

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)
\mvdash{}  \mforall{}a:\{a:formula()|  a  \msubseteq{}  x  \mwedge{}  prank(a)  <  n\} 
        extend-val(v0;f;a)  =  extend-val(v0;\mlambda{}a.extend-val(v0;f;a);a)


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  MoveToConcl  (-1)
  THEN  SimpleDatatypeInduction  (-1)
  THEN  Unfold  `prank`  0
  THEN  Reduce  0)

---

Home Index