---

Step * of Lemma l_treeco-ext

∀[L,T:Type].
  l_treeco(L;T) ≡ lbl:Atom × if lbl =a "leaf" then L
                             if lbl =a "node" then val:T × left_subtree:l_treeco(L;T) × l_treeco(L;T)
                             else Void
                             fi 
BY
{ ProveCoDatatypeExt }

---

Latex:


\mforall{}[L,T:Type].
    l\_treeco(L;T)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "leaf"  then  L
                                                          if  lbl  =a  "node"  then  val:T  \mtimes{}  left$_{subtree}$:l\_tr\000Ceeco(L;T)  \mtimes{}  l\_treeco(L;T)
                                                          else  Void
                                                          fi 


By

ProveCoDatatypeExt

---

Home Index