(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

{sort s;

op c : s;

op c : a ->? s;

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

op gn_inj : s1 -> s;

op gn_inj : s2 -> s

} %(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

{sort s;

op c : s;

op c : a ->? s;

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

op gn_inj : s1 -> s;

op gn_inj : s2 -> s

} %(ga_generated_s)%])

*** Error 3.30,

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

must appear in alternative

'c : s'

*** Error 3.53,

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

must appear in alternative

'c : a ->? s'

### Hint 4.16, redeclared sort 's'

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

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

### Hint 4.35, redeclared op 'c'

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

### Hint 4.46, redeclared op 'c'

### Hint 4.51, redeclared op 'a'

### Hint 4.53, redeclared op 'b'

### Hint 4.58, redeclared op 'd'

### Warning 4.65, partially redeclared 'c'

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

*** Error 4.35,

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

must appear in alternative

'c : s'

*** Error 4.39,

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

must appear in alternative

'c : a -> s'

*** Error 4.65,

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

must appear in alternative

'c : a ->? s'