---

Step * of Lemma int_term-ext

int_term() ≡ lbl:Atom × if lbl =a "Constant" then ℤ
                        if lbl =a "Var" then ℤ
                        if lbl =a "Add" then left:int_term() × int_term()
                        if lbl =a "Subtract" then left:int_term() × int_term()
                        if lbl =a "Multiply" then left:int_term() × int_term()
                        if lbl =a "Minus" then int_term()
                        else Void
                        fi 
BY
{ ProveDatatypeExt }

---

Latex:

---

Latex:
int\_term()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Constant"  then  \mBbbZ{}
                                                if  lbl  =a  "Var"  then  \mBbbZ{}
                                                if  lbl  =a  "Add"  then  left:int\_term()  \mtimes{}  int\_term()
                                                if  lbl  =a  "Subtract"  then  left:int\_term()  \mtimes{}  int\_term()
                                                if  lbl  =a  "Multiply"  then  left:int\_term()  \mtimes{}  int\_term()
                                                if  lbl  =a  "Minus"  then  int\_term()
                                                else  Void
                                                fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index