# If a cache has exclusive access to a block, then the other cache
# has no access to that block 
# Property for block 0 owned by cache 1

AG(((cc1.block_state=EXCLUSIVE) * (cc1.block_add<0> = 0)) ->
    ((cc2.block_state=INVALID) + ! (cc2.block_add<0> = 0)) );