---

Step * of Lemma mFOL_case_wf

∀[T:Type]. ∀[v:mFOL()]. ∀[atomic:name:Atom ⟶ vars:(ℤ List) ⟶ T]. ∀[connect:knd:Atom
                                                                             ⟶ left:mFOL()
                                                                             ⟶ right:mFOL()
                                                                             ⟶ T]. ∀[quant:isall:𝔹
                                                                                            ⟶ var:ℤ
                                                                                            ⟶ body:mFOL()
                                                                                            ⟶ T].
  (case(v)
   name(vars) => atomic[name;vars];
   left knd right => connect[knd;left;right];
   isall var.body => quant[isall;var;body] ∈ T)
BY
{ (ProveWfLemma THEN DVar `v' THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[v:mFOL()].  \mforall{}[atomic:name:Atom  {}\mrightarrow{}  vars:(\mBbbZ{}  List)  {}\mrightarrow{}  T].  \mforall{}[connect:knd:Atom
                                                                                                                                                          {}\mrightarrow{}  left:mFOL()
                                                                                                                                                          {}\mrightarrow{}  right:mFOL()
                                                                                                                                                          {}\mrightarrow{}  T].
\mforall{}[quant:isall:\mBbbB{}  {}\mrightarrow{}  var:\mBbbZ{}  {}\mrightarrow{}  body:mFOL()  {}\mrightarrow{}  T].
    (case(v)
      name(vars)  =>  atomic[name;vars];
      left  knd  right  =>  connect[knd;left;right];
      isall  var.body  =>  quant[isall;var;body]  \mmember{}  T)


By

---

Latex:
(ProveWfLemma  THEN  DVar  `v'  THEN  All  Reduce  THEN  Auto)

---

Home Index