---

Step * of Lemma bs_tree-ext

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

---

Latex:

---

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


By

---

Latex:
ProveDatatypeExt

---

Home Index