---

Step * of Lemma binary_map-ext

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

---

Latex:

---

Latex:
\mforall{}[T,Key:Type].
    binary\_map(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\_map(T;Key)
                                                                                \mtimes{}  binary\_map(T;Key)
                                                                  else  Void
                                                                  fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index