d5b7ba26785d7494166d48876362ba30ff30b98awrowelogic CspCASL

c30ef289fe64ac7fedc44cfcc6b439f0f8458b4cgregamesspec tcs4 =

c30ef289fe64ac7fedc44cfcc6b439f0f8458b4cgregamesdata sorts A, B, C < S

396aeca634b86a3ab34d5bdb9c32cbce73c72421jerenkrantz ops a: A; b1, b2: B; c: C;

2de11b5d55c9ffae11582eda6853c5628fccaad1jerenkrantz f: A ->? A; g: C->? C

2de11b5d55c9ffae11582eda6853c5628fccaad1jerenkrantz . a = b1 . b2 = c

2de11b5d55c9ffae11582eda6853c5628fccaad1jerenkrantz . forall x: A . not def f(x) . forall x: C . not def g(x);

9e398d701dd430f073ff5418fb720642e064046ajerenkrantzprocess

9e398d701dd430f073ff5418fb720642e064046ajerenkrantz P1 = f(a) -> SKIP || g(c) -> SKIP

9e398d701dd430f073ff5418fb720642e064046ajerenkrantz