---

Step * of Lemma mFOLco-ext

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

---

Latex:


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


By

ProveCoDatatypeExt

---

Home Index