4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblettdata sorts A, B, C < S

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblett ops a: A; b1, b2: B; c: C;

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblett f: A ->? A; g: C->? C

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblett . a = b1 . b2 = c

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblett . forall x: A . not def f(x) . forall x: C . not def g(x)

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblettprocess f(a) -> SKIP || g(c) -> SKIP