data sorts S, T

ops f: S ->? T

. forall x: S . not def f(x)

process (?x: S -> f(x) -> SKIP) [| T |] (?y : T -> if def y then P else Q)