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