-- Elementare Prädikate  
s == t  
s < t  
  
-- Zusammengesetzte Prädikate  
not p  
p && q   
p || q   
p => q  

Axiome für Map

lookup a (empty :: Map Int String) == Nothing  
  
lookup a (insert a v (s :: Map Int String)) == Just v  
lookup a (delete a (s :: Map Int String)) == Nothing  
  
a /= b ==> lookup a (insert b v s) == lookup a (s :: Map Int String)  
a /= b ==> lookup a (delete b s) == lookup a (s :: Map Int String)