# Two caches do not have exclusive access to the same block

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