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:


\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

ProveCoDatatypeExt




Home Index