---

Step * of Lemma MultiTree-ext

∀[T:Type]
  MultiTree(T) ≡ lbl:Atom × if lbl =a "Node" then labels:{L:Atom List| 0 < ||L||}  × ({a:Atom| (a ∈ labels)}  ─→ MultiTr\000Cee(T))
                            if lbl =a "Leaf" then T
                            else Void
                            fi 
BY
{ ProveDatatypeExt }

---

Latex:


\mforall{}[T:Type]
    MultiTree(T)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Node"
                                                            then  labels:\{L:Atom  List|  0  <  ||L||\} 
                                                                      \mtimes{}  (\{a:Atom|  (a  \mmember{}  labels)\}    {}\mrightarrow{}  MultiTree(T))
                                                        if  lbl  =a  "Leaf"  then  T
                                                        else  Void
                                                        fi 


By

ProveDatatypeExt

---

Home Index