How to translate `ca & ~intervening(W,ca)`

[fsestini]

This expression is used to define TLBuncacheable-pred and HU-pred.

(* TLBUncacheable-predecessor *)
let TLBuncacheable-pred =
  [range([TLBUncacheable & FAULT]; tr-ib^-1)]; (ca & ~intervening(W,ca)); [Exp & W]

(* Hardware-update-predecessor *)
let HU-pred =
  (ca & ~intervening(W,ca)); [HU]

intervening in turn is defined as

let intervening(S,r) = r; [S]; r

Therefore, ~intervening(W, ca) is equivalent to ~(ca; [W]; ca). There's no direct way to encode the complement/negation of a relaxation in diy. How should we then deal with this definition?