---

Step * of Lemma int_formula-ext

int_formula() ≡ 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_formula() × int_formula()
                           if lbl =a "or" then left:int_formula() × int_formula()
                           if lbl =a "implies" then left:int_formula() × int_formula()
                           if lbl =a "not" then int_formula()
                           else Void
                           fi 
BY
{ ProveDatatypeExt }

---

Latex:

---

Latex:
int\_formula()  \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\_formula()  \mtimes{}  int\_formula()
                                                      if  lbl  =a  "or"  then  left:int\_formula()  \mtimes{}  int\_formula()
                                                      if  lbl  =a  "implies"  then  left:int\_formula()  \mtimes{}  int\_formula()
                                                      if  lbl  =a  "not"  then  int\_formula()
                                                      else  Void
                                                      fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index