---

Step * of Lemma int_formulaco-ext

int_formulaco() ≡ lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
                             if lbl =a "le" then left:int_term() × int_term()
                             if lbl =a "eq" then left:int_term() × int_term()
                             if lbl =a "and" then left:int_formulaco() × int_formulaco()
                             if lbl =a "or" then left:int_formulaco() × int_formulaco()
                             if lbl =a "implies" then left:int_formulaco() × int_formulaco()
                             if lbl =a "not" then int_formulaco()
                             else Void
                             fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
int\_formulaco()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "less"  then  left:int\_term()  \mtimes{}  int\_term()
                                                          if  lbl  =a  "le"  then  left:int\_term()  \mtimes{}  int\_term()
                                                          if  lbl  =a  "eq"  then  left:int\_term()  \mtimes{}  int\_term()
                                                          if  lbl  =a  "and"  then  left:int\_formulaco()  \mtimes{}  int\_formulaco()
                                                          if  lbl  =a  "or"  then  left:int\_formulaco()  \mtimes{}  int\_formulaco()
                                                          if  lbl  =a  "implies"  then  left:int\_formulaco()  \mtimes{}  int\_formulaco()
                                                          if  lbl  =a  "not"  then  int\_formulaco()
                                                          else  Void
                                                          fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index