---

Step * of Lemma mFOL-ext

mFOL() ≡ lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
                    if lbl =a "connect" then knd:Atom × left:mFOL() × mFOL()
                    if lbl =a "quant" then isall:𝔹 × var:ℤ × mFOL()
                    else Void
                    fi 
BY
{ ProveDatatypeExt }

---

Latex:


mFOL()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "atomic"  then  name:Atom  \mtimes{}  (\mBbbZ{}  List)
                                        if  lbl  =a  "connect"  then  knd:Atom  \mtimes{}  left:mFOL()  \mtimes{}  mFOL()
                                        if  lbl  =a  "quant"  then  isall:\mBbbB{}  \mtimes{}  var:\mBbbZ{}  \mtimes{}  mFOL()
                                        else  Void
                                        fi 


By

ProveDatatypeExt

---

Home Index