70N/Alogic CspCASL

70N/Aspec tcs4 =

70N/Adata sorts A, B, C < S

70N/A ops a: A; b1, b2: B; c: C;

70N/A f: A ->? A; g: C->? C

70N/A . a = b1 . b2 = c

70N/A . forall x: A . not def f(x) . forall x: C . not def g(x);

70N/Aprocess

70N/A tcs4: A, C

70N/A tcs4 = f(a) -> SKIP || g(c) -> SKIP

70N/A