---

Step * of Lemma formula-ext

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

---

Latex:

---

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


By

---

Latex:
ProveDatatypeExt

---

Home Index