---

Step * of Lemma Form-ext

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

---

Latex:

---

Latex:
\mforall{}[C:Type]
    Form(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{}  Form(C)
                                              if  lbl  =a  "Equal"  then  left:Form(C)  \mtimes{}  Form(C)
                                              if  lbl  =a  "Member"  then  element:Form(C)  \mtimes{}  Form(C)
                                              if  lbl  =a  "And"  then  left:Form(C)  \mtimes{}  Form(C)
                                              if  lbl  =a  "Or"  then  left:Form(C)  \mtimes{}  Form(C)
                                              if  lbl  =a  "Not"  then  Form(C)
                                              if  lbl  =a  "All"  then  var:Atom  \mtimes{}  Form(C)
                                              if  lbl  =a  "Exists"  then  var:Atom  \mtimes{}  Form(C)
                                              else  Void
                                              fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index