4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblettdata sorts S, T

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblett ops f: S ->? T

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblett . forall x: S . not def f(x)

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