(Devices 1) (CanSend 2) requires forall d1 d2 (CanSend(d1,d2) -> Devices(d1)) & forall d1 d2 (CanSend(d1,d2) -> Devices(d2)) & forall d1 (Devices(d1)->(exists d2 (CanSend(d2,d1)))) & exists d1 (Devices(d1) & (forall d2 (Devices(d2) -> (CanSend(d2,d1))))) DELETE FROM CanSend WHERE Column1=device_to_delete OR Column2=device_to_delete; ensures exists d2 (Devices(d2) & (forall d1 ((~(d1 = device_to_delete) & Devices(d1)) -> (CanSend(d1,d2)))))