logic CspCASL
spec tcs3 = 
data sorts S, T
     ops f: S ->? T
     . forall x: S . not def f(x);
process
  tcs3: S, T;
  tcs3 = [] x :: S -> f(x) -> SKIP
           [| T |]
         [] y :: T -> (if def y then SKIP else STOP)