(sorts A, B, C, L, R

op a : A

op b : B

op c : A * B * L -> C

op l : R -> L

op la : A -> L

op r : R

op r : L -> R,

[forall v1, v2 : A . la(v1) = la(v2) <=> v1 = v2

%(ga_injective_la)%,

forall v1, v2 : R . l(v1) = l(v2) <=> v1 = v2 %(ga_injective_l)%,

forall v1 : A; v2 : R . not la(v1) = l(v2) %(ga_disjoint_la_l)%,

forall v1, v2 : L . r(v1) = r(v2) <=> v1 = v2 %(ga_injective_r)%,

forall v1 : L . not r = r(v1) %(ga_disjoint_r_r)%,

forall v1 : A; v2 : B; v3 : L; v4 : A; v5 : B; v6 : L

. c(v1, v2, v3) = c(v4, v5, v6) <=> v1 = v4 /\ v2 = v5 /\ v3 = v6

%(ga_injective_c)%,

%% free

generated type A ::= a %(ga_generated_A)%,

%% free

generated type B ::= b %(ga_generated_B)%,

%% free

generated types

L ::= l(R) | la(A);

R ::= r | r(L) %(ga_generated_L_R)%,

%% free

generated type

C

::= c(A;

B;

L) %(ga_generated_C)%])