(sorts a, s, s1, s2, t

sorts s1, s2 < s

op a : s -> t

op b : s -> t

op c : s

op c : a -> s

op c : a * t * t * t -> s

op d : s -> t,

[forall v1 : a; v2, v3, v4 : t . a(c(v1, v2, v3, v4)) = v2

%(ga_selector_a)%,

forall v1 : a; v2, v3, v4 : t . b(c(v1, v2, v3, v4)) = v3

%(ga_selector_b)%,

forall v1 : a; v2, v3, v4 : t . d(c(v1, v2, v3, v4)) = v4

%(ga_selector_d)%,

forall v1 : a; v2, v3, v4 : t; v5 : a; v6, v7, v8 : t

. c(v1, v2, v3, v4) = c(v5, v6, v7, v8)

<=> v1 = v5 /\ v2 = v6 /\ v3 = v7 /\ v4 = v8 %(ga_injective_c)%,

forall v1, v2 : a . c(v1) = c(v2) <=> v1 = v2 %(ga_injective_c)%,

forall v1 : s . not (v1 in s2 /\ v1 in s1)

%(ga_disjoint_sorts_s2_s1)%,

not c in s2 %(ga_disjoint_c_sort_s2)%,

not c in s1 %(ga_disjoint_c_sort_s1)%,

forall v1 : a; v2, v3, v4 : t . not c(v1, v2, v3, v4) in s2

%(ga_disjoint_c_sort_s2)%,

forall v1 : a; v2, v3, v4 : t . not c(v1, v2, v3, v4) in s1

%(ga_disjoint_c_sort_s1)%,

forall v1 : a . not c(v1) in s2 %(ga_disjoint_c_sort_s2)%,

forall v1 : a . not c(v1) in s1 %(ga_disjoint_c_sort_s1)%,

forall v1 : a; v2, v3, v4 : t . not c = c(v1, v2, v3, v4)

%(ga_disjoint_c_c)%,

forall v1 : a . not c = c(v1) %(ga_disjoint_c_c)%,

forall v1 : a; v2, v3, v4 : t; v5 : a

. not c(v1, v2, v3, v4) = c(v5) %(ga_disjoint_c_c)%,

not def a(c) %(ga_selector_undef_a_c)%,

forall v1 : a . not def a(c(v1)) %(ga_selector_undef_a_c)%,

not def b(c) %(ga_selector_undef_b_c)%,

forall v1 : a . not def b(c(v1)) %(ga_selector_undef_b_c)%,

not def d(c) %(ga_selector_undef_d_c)%,

forall v1 : a . not def d(c(v1)) %(ga_selector_undef_d_c)%,

%% free

generated type s ::= c | c(a)? | c(a; t; t; t) | sort s1 | sort s2

%(ga_generated_s)%,

forall v1 : a; v2, v3, v4 : t . a(c(v1, v2, v3, v4)) = v2

%(ga_selector_a)%,

forall v1 : a; v2, v3, v4 : t . b(c(v1, v2, v3, v4)) = v3

%(ga_selector_b)%,

forall v1 : a; v2, v3, v4 : t . d(c(v1, v2, v3, v4)) = v4

%(ga_selector_d)%,

generated type s ::= c | c(a)? | c(a; t; t; t) | sort s1 | sort s2

%(ga_generated_s)%])

3.30: ### Warning:

total selectors 'a : s -> t, b : s -> t, d : s -> t'

should be in alternative

'c : s'

3.53: ### Warning:

total selectors 'a : s -> t, b : s -> t, d : s -> t'

should be in alternative

'c : a ->? s'

3.53: *** Error: illegal free partial constructor 'c'

4.16: ### Hint: redeclared sort 's'

4.27: ### Hint: redeclared subsort 's2 < s'

4.30: ### Hint: redeclared subsort 's1 < s'

4.35: ### Hint: redeclared op 'c'

4.39: ### Hint: redeclared as total 'c'

4.46: ### Hint: redeclared op 'c'

4.51: ### Hint: redeclared op 'a'

4.53: ### Hint: redeclared op 'b'

4.58: ### Hint: redeclared op 'd'

4.65: ### Warning: partially redeclared 'c'

4.39: *** Error: duplicates at '(4,65)' for 'c : a -> s'

4.35: ### Warning:

total selectors 'a : s -> t, b : s -> t, d : s -> t'

should be in alternative

'c : s'

4.39: ### Warning:

total selectors 'a : s -> t, b : s -> t, d : s -> t'

should be in alternative

'c : a -> s'

4.65: ### Warning:

total selectors 'a : s -> t, b : s -> t, d : s -> t'

should be in alternative

'c : a ->? s'