d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblettdata sort S < T
d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett ops f : S ->? T
d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett . forall x: S . not def f(x)
d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblettprocess (?x: S -> f(x) -> SKIP) [| T |] (?y : T -> if def y then P else Q)