6f7660093e70d3a7c80738b681ac0f5c1b661c00Mark Andrewsspec tcs4 =

6f7660093e70d3a7c80738b681ac0f5c1b661c00Mark Andrewsdata {sorts A, B, C < S

1fdbadc594a49b423052ea342dac74ff1a36089dMark Andrews ops a: A; b1, b2: B; c: C;

1fdbadc594a49b423052ea342dac74ff1a36089dMark Andrews f: A ->? A; g: C->? C

a1898260ad19d02e88ab76c1855d33c67add9defMark Andrews . a = b1 . b2 = c

a1898260ad19d02e88ab76c1855d33c67add9defMark Andrews . forall x: A . not def f(x) . forall x: C . not def g(x) }

a1898260ad19d02e88ab76c1855d33c67add9defMark Andrewsprocess f(a) -> SKIP || g(c) -> SKIP

305b0eda33b16493355db1f1c86313a6f5fbfc3bDanny Mayer