---

Step * of Lemma rat_termco-ext

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

---

Latex:

---

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


By

---

Latex:
ProveCoDatatypeExt

---

Home Index