---

Step * of Lemma bs_treeco-ext

∀[E:Type]
  bs_treeco(E) ≡ lbl:Atom × if lbl =a "null" then Unit
                            if lbl =a "leaf" then E
                            if lbl =a "node" then left:bs_treeco(E) × value:E × bs_treeco(E)
                            else Void
                            fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
\mforall{}[E:Type]
    bs\_treeco(E)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "null"  then  Unit
                                                        if  lbl  =a  "leaf"  then  E
                                                        if  lbl  =a  "node"  then  left:bs\_treeco(E)  \mtimes{}  value:E  \mtimes{}  bs\_treeco(E)
                                                        else  Void
                                                        fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index