c79e39ad568d9af854765f64049534044ef6c034nd(sorts a, s, s1, s2, t

2d0611ffc9f91c5fc2ddccb93f9a3d17791ae650takashi sorts s1, s2 < s

c79e39ad568d9af854765f64049534044ef6c034nd op a : s -> t

d3e250aab242db84d14060985b5db675a731d548nd op b : s -> t

c79e39ad568d9af854765f64049534044ef6c034nd op c : s

c79e39ad568d9af854765f64049534044ef6c034nd op c : a -> s

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

c79e39ad568d9af854765f64049534044ef6c034nd op d : s -> t,[ . forall X1: a; X2: t; X3: t; X4: t

c79e39ad568d9af854765f64049534044ef6c034nd . a(c(X1, X2, X3, X4)) = X2,

c79e39ad568d9af854765f64049534044ef6c034nd . forall X1: a; X2: t; X3: t; X4: t . b(c(X1, X2, X3, X4)) = X3,

4a56677aad9b66a36f3dc9fddbca8dc1230ad471rbowen . forall X1: a; X2: t; X3: t; X4: t . d(c(X1, X2, X3, X4)) = X4,

4a56677aad9b66a36f3dc9fddbca8dc1230ad471rbowen . forall X1: a; X2: t; X3: t; X4: t; Y1: a; Y2: t; Y3: t; Y4: t

4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluem . c(X1, X2, X3, X4) = c(Y1, Y2, Y3, Y4) <=>

c79e39ad568d9af854765f64049534044ef6c034nd X1 = Y1 /\ X2 = Y2 /\ X3 = Y3 /\ X4 = Y4,

c79e39ad568d9af854765f64049534044ef6c034nd . forall X1: a; Y1: a . c(X1) = c(Y1) <=> X1 = Y1,

. forall x: s . not (x in s2 /\ x in s1), . not c in s2,

. not c in s1,

. forall X1: a; X2: t; X3: t; X4: t . not c(X1, X2, X3, X4) in s2,

. forall X1: a; X2: t; X3: t; X4: t . not c(X1, X2, X3, X4) in s1,

. forall X1: a . not c(X1) in s2,

. forall X1: a . not c(X1) in s1,

. forall Y1: a; Y2: t; Y3: t; Y4: t . not c = c(Y1, Y2, Y3, Y4),

. forall Y1: a . not c = c(Y1),

. forall X1: a; X2: t; X3: t; X4: t; Y1: a

. not c(X1, X2, X3, X4) = c(Y1),

. not def a(c), . forall X1: a . not def a(c(X1)),

. not def b(c), . forall X1: a . not def b(c(X1)),

. not def d(c), . forall X1: a . not def d(c(X1)),

generated{sort s; op c : s; op c : a ->? s;

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

op g__inj : s2 -> s},

. forall X1: a; X2: t; X3: t; X4: t . a(c(X1, X2, X3, X4)) = X2,

. forall X1: a; X2: t; X3: t; X4: t . b(c(X1, X2, X3, X4)) = X3,

. forall X1: a; X2: t; X3: t; X4: t . d(c(X1, X2, X3, X4)) = X4,

generated{sort s; op c : s; op c : a ->? s;

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

op g__inj : s2 -> 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'