---

Step * of Lemma formulaco-ext

formulaco() ≡ lbl:Atom × if lbl =a "var" then Atom
                         if lbl =a "not" then formulaco()
                         if lbl =a "and" then left:formulaco() × formulaco()
                         if lbl =a "or" then left:formulaco() × formulaco()
                         if lbl =a "imp" then left:formulaco() × formulaco()
                         else Void
                         fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
formulaco()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "var"  then  Atom
                                                  if  lbl  =a  "not"  then  formulaco()
                                                  if  lbl  =a  "and"  then  left:formulaco()  \mtimes{}  formulaco()
                                                  if  lbl  =a  "or"  then  left:formulaco()  \mtimes{}  formulaco()
                                                  if  lbl  =a  "imp"  then  left:formulaco()  \mtimes{}  formulaco()
                                                  else  Void
                                                  fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index