---

Step * of Lemma binary_mapco-ext

∀[T,Key:Type].
  binary_mapco(T;Key) ≡ lbl:Atom × if lbl =a "E" then Unit
                                   if lbl =a "T"
                                     then key:Key × value:T × cnt:ℤ × left:binary_mapco(T;Key) × binary_mapco(T;Key)
                                   else Void
                                   fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
\mforall{}[T,Key:Type].
    binary\_mapco(T;Key)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "E"  then  Unit
                                                                      if  lbl  =a  "T"
                                                                          then  key:Key
                                                                                    \mtimes{}  value:T
                                                                                    \mtimes{}  cnt:\mBbbZ{}
                                                                                    \mtimes{}  left:binary\_mapco(T;Key)
                                                                                    \mtimes{}  binary\_mapco(T;Key)
                                                                      else  Void
                                                                      fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index