context  Book 
 inv:  
 Name .allInstances() -> forAll (  v0  |  ( 
 Target .allInstances() -> exists (  v1  |  ( (self . addr[v0] -> includes(v1))  and  (Target .allInstances() -> includes( v1 )) ) )   implies  (self . names -> includes(v0)) ) ) 


context  Book 
 inv:  
 Name .allInstances() -> select (  n  |  self ->closure( z1 |  Target .allInstances()->select( z0 |  (self . addr[z1] -> includes(z0)) ))->includes( self ) )   -> isEmpty()


context  Book 
 inv:  
 Alias .allInstances() -> forAll (  a  |  
 Target .allInstances() -> select(  y0  |  (self . addr[a] -> includes(y0)) ) ->size() <= 1 ) 


context  Book :: add (n:Name,a:Target) : void 
pre:  (self . names -> includes(n)) 
post:  
 Name .allInstances() -> forAll (  v0  |  
 Target .allInstances() -> forAll (  v1  |  ( (self . addr[v0] -> includes(v1))  implies  ( (self . addr@pre[v0] -> includes(v1))  or  ( (v0 = n)  and  (v1 = a) ) ) ) )  )  


context  Book :: lookup (n:Name) : Set ( Book ) 
body:  Addr .allInstances() -> select( yy | ( self ->closure( z1 |  Target .allInstances()->select( z0 |  (self . addr[z1] -> includes(z0)) ))->includes( self )  and  (Addr .allInstances() -> includes( yy )) ) )