---

Step * of Lemma Formco-ext

∀[C:Type]
  Formco(C) ≡ lbl:Atom × if lbl =a "Var" then Atom
                         if lbl =a "Const" then C
                         if lbl =a "Set" then var:Atom × Formco(C)
                         if lbl =a "Equal" then left:Formco(C) × Formco(C)
                         if lbl =a "Member" then element:Formco(C) × Formco(C)
                         if lbl =a "And" then left:Formco(C) × Formco(C)
                         if lbl =a "Or" then left:Formco(C) × Formco(C)
                         if lbl =a "Not" then Formco(C)
                         if lbl =a "All" then var:Atom × Formco(C)
                         if lbl =a "Exists" then var:Atom × Formco(C)
                         else Void
                         fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
\mforall{}[C:Type]
    Formco(C)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Var"  then  Atom
                                                  if  lbl  =a  "Const"  then  C
                                                  if  lbl  =a  "Set"  then  var:Atom  \mtimes{}  Formco(C)
                                                  if  lbl  =a  "Equal"  then  left:Formco(C)  \mtimes{}  Formco(C)
                                                  if  lbl  =a  "Member"  then  element:Formco(C)  \mtimes{}  Formco(C)
                                                  if  lbl  =a  "And"  then  left:Formco(C)  \mtimes{}  Formco(C)
                                                  if  lbl  =a  "Or"  then  left:Formco(C)  \mtimes{}  Formco(C)
                                                  if  lbl  =a  "Not"  then  Formco(C)
                                                  if  lbl  =a  "All"  then  var:Atom  \mtimes{}  Formco(C)
                                                  if  lbl  =a  "Exists"  then  var:Atom  \mtimes{}  Formco(C)
                                                  else  Void
                                                  fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index