---

Step * of Lemma bdd-val_wf

∀[x:formula()]. ∀[v0:{a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹]. ∀[n:ℕ].  (bdd-val(v0;x;n) ∈ Type)
BY
{ (ProveWfLemma
   THEN DoSubsume
   THEN Auto
   THEN (SubtypeReasoning THENM Try (RelRST))
   THEN Auto
   THEN (FLemma `prank_functionality` [-1] THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[x:formula()].  \mforall{}[v0:\{a:formula()|  a  \msubseteq{}  x  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbN{}].    (bdd-val(v0;x;n)  \mmember{}  Type)


By

---

Latex:
(ProveWfLemma
  THEN  DoSubsume
  THEN  Auto
  THEN  (SubtypeReasoning  THENM  Try  (RelRST))
  THEN  Auto
  THEN  (FLemma  `prank\_functionality`  [-1]  THEN  Auto)\mcdot{})

---

Home Index