---

Step * of Lemma binary-tree-ext

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

---

Latex:

---

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


By

---

Latex:
ProveDatatypeExt

---

Home Index