---

Step * 1 1 1 1 1 of Lemma valuation-exists


1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. a : formula()
5. f : bdd-val(v0;x;n - 1)
⊢ (a ⊆ x ∧ prank(a) < n) ⇒ (extend-val(v0;f;a) ∈ 𝔹)
BY
{ (SimpleDatatypeInduction (-2)
   THEN Unfolds ``prank extend-val`` 0
   THEN Reduce 0
   THEN Try (Folds ``prank`` 0)
   THEN (DVar `f'⋅
         THEN Auto
         THEN MemTypeCD
         THEN Auto
         THEN Try (((RWO "imax_unfold" (-2) THENA Auto) THEN SplitOnHypITE -2  THEN Complete (Auto))))⋅) }

1
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
5. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . f a = extend-val(v0;f;a)
6. a1 : formula()
7. (a1 ⊆ x ∧ prank(a1) < n) ⇒ (extend-val(v0;f;a1) ∈ 𝔹)
8. pnot(a1) ⊆ x
9. prank(a1) + 1 < n
⊢ a1 ⊆ x

2
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
5. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . f a = extend-val(v0;f;a)
6. left : formula()
7. a2 : formula()
8. (a2 ⊆ x ∧ prank(a2) < n) ⇒ (extend-val(v0;f;a2) ∈ 𝔹)
9. (left ⊆ x ∧ prank(left) < n) ⇒ (extend-val(v0;f;left) ∈ 𝔹)
10. pand(left;a2) ⊆ x
11. imax(prank(left);prank(a2)) + 1 < n
⊢ left ⊆ x

3
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
5. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . f a = extend-val(v0;f;a)
6. left : formula()
7. a2 : formula()
8. (a2 ⊆ x ∧ prank(a2) < n) ⇒ (extend-val(v0;f;a2) ∈ 𝔹)
9. (left ⊆ x ∧ prank(left) < n) ⇒ (extend-val(v0;f;left) ∈ 𝔹)
10. pand(left;a2) ⊆ x
11. imax(prank(left);prank(a2)) + 1 < n
12. ↑(f left)
⊢ a2 ⊆ x

4
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
5. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . f a = extend-val(v0;f;a)
6. left : formula()
7. a2 : formula()
8. (a2 ⊆ x ∧ prank(a2) < n) ⇒ (extend-val(v0;f;a2) ∈ 𝔹)
9. (left ⊆ x ∧ prank(left) < n) ⇒ (extend-val(v0;f;left) ∈ 𝔹)
10. pand(left;a2) ⊆ x
11. imax(prank(left);prank(a2)) + 1 < n
12. ↑(f left)
13. a2 ⊆ x
⊢ prank(a2) < n - 1

5
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
5. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . f a = extend-val(v0;f;a)
6. left : formula()
7. a2 : formula()
8. (a2 ⊆ x ∧ prank(a2) < n) ⇒ (extend-val(v0;f;a2) ∈ 𝔹)
9. (left ⊆ x ∧ prank(left) < n) ⇒ (extend-val(v0;f;left) ∈ 𝔹)
10. por(left;a2) ⊆ x
11. imax(prank(left);prank(a2)) + 1 < n
⊢ left ⊆ x

6
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
5. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . f a = extend-val(v0;f;a)
6. left : formula()
7. a2 : formula()
8. (a2 ⊆ x ∧ prank(a2) < n) ⇒ (extend-val(v0;f;a2) ∈ 𝔹)
9. (left ⊆ x ∧ prank(left) < n) ⇒ (extend-val(v0;f;left) ∈ 𝔹)
10. por(left;a2) ⊆ x
11. imax(prank(left);prank(a2)) + 1 < n
⊢ a2 ⊆ x

7
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
5. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . f a = extend-val(v0;f;a)
6. left : formula()
7. a2 : formula()
8. (a2 ⊆ x ∧ prank(a2) < n) ⇒ (extend-val(v0;f;a2) ∈ 𝔹)
9. (left ⊆ x ∧ prank(left) < n) ⇒ (extend-val(v0;f;left) ∈ 𝔹)
10. pimp(left;a2) ⊆ x
11. imax(prank(left);prank(a2)) + 1 < n
⊢ left ⊆ x

8
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
3. n : ℕ
4. f : {a:formula()| a ⊆ x ∧ prank(a) < n - 1}  ⟶ 𝔹
5. ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n - 1} . f a = extend-val(v0;f;a)
6. left : formula()
7. a2 : formula()
8. (a2 ⊆ x ∧ prank(a2) < n) ⇒ (extend-val(v0;f;a2) ∈ 𝔹)
9. (left ⊆ x ∧ prank(left) < n) ⇒ (extend-val(v0;f;left) ∈ 𝔹)
10. pimp(left;a2) ⊆ x
11. imax(prank(left);prank(a2)) + 1 < n
⊢ a2 ⊆ x

---

Latex:

---

Latex:

1.  x  :  formula()
2.  v0  :  \{a:formula()|  a  \msubseteq{}  x  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}
3.  n  :  \mBbbN{}
4.  a  :  formula()
5.  f  :  bdd-val(v0;x;n  -  1)
\mvdash{}  (a  \msubseteq{}  x  \mwedge{}  prank(a)  <  n)  {}\mRightarrow{}  (extend-val(v0;f;a)  \mmember{}  \mBbbB{})


By

---

Latex:
(SimpleDatatypeInduction  (-2)
  THEN  Unfolds  ``prank  extend-val``  0
  THEN  Reduce  0
  THEN  Try  (Folds  ``prank``  0)
  THEN  (DVar  `f'\mcdot{}
              THEN  Auto
              THEN  MemTypeCD
              THEN  Auto
              THEN  Try  (((RWO  "imax\_unfold"  (-2)  THENA  Auto)  THEN  SplitOnHypITE  -2    THEN  Complete  (Auto))))
  \mcdot{})

---

Home Index