(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)))))