---

Step * of Lemma binary-treeco-ext

binary-treeco() ≡ lbl:Atom × if lbl =a "Leaf" then ℤ
                             if lbl =a "Node" then left:binary-treeco() × binary-treeco()
                             else Void
                             fi 
BY
{ ProveCoDatatypeExt }

---

Latex:


binary-treeco()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Leaf"  then  \mBbbZ{}
                                                          if  lbl  =a  "Node"  then  left:binary-treeco()  \mtimes{}  binary-treeco()
                                                          else  Void
                                                          fi 


By

ProveCoDatatypeExt

---

Home Index