types s, t < t

ops a, b : s

%% op __ + __ : s -> s -> s, idem, assoc, comm;

op __+__ : s * s -> s

op __+__ : t * t -> t

op __+__ : t -> t -> t

ops a, b : t

op c : s = a + b;

op d : s = a + a;

op e : s * s -> s = __+__;

op f : s * s -> s = __+__;

op g : s * s = (a, b);

op h : s = a + b;

op i : s = (a : s) + (b : s);

op incr : s -> s

op i1 : s = incr a;

op i2 : s = incr a;

op i3 : s = incr a;

op __<=__<=__ : s * s * s -> s

op l1 : s = a <= b <= c;

op l2 : s * s * s -> s = __<=__<=__;

op l3 : s = a <= b <= c;

op l4 : s = a <= b <= c;

op l5 : s * s * s = (a, b, c);

op x : s

op y : s = (op a : s) <= (var x : s) <= (a : s);

op z : s = (x as s) + (x as t as s);

. x in s %(bla_label)%

. x in t;

types

s : Type;

t : Type

type

s < t

op __+__ : t -> t -> t %(op)%

op __+__ : s * s -> s %(op)%

op __+__ : t * t -> t %(op)%

op __<=__<=__ : s * s * s -> s %(op)%

op a : s %(op)%

op a : t %(op)%

op b : s %(op)%

op b : t %(op)%

op c : s

%[op= (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s]%

op d : s

%[op= (op __+__ : s * s -> s) ((op a : s), (op a : s)) as s]%

op e : s * s -> s %[op= (op __+__ : s * s -> s) as s * s -> s]%

op f : s * s -> s %[op= (op __+__ : s * s -> s) as s * s -> s]%

op g : s * s %[op= ((op a : s), (op b : s)) as s * s]%

op h : s

%[op= (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s]%

op i : s

%[op= (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s]%

op i1 : s %[op= (op incr : s -> s) (op a : s) as s]%

op i2 : s %[op= (op incr : s -> s) (op a : s) as s]%

op i3 : s %[op= (op incr : s -> s) (op a : s) as s]%

op incr : s -> s %(op)%

op l1 : s

%[op=

(op __<=__<=__ : s * s * s -> s)

((op a : s), (op b : s), (op c : s))

as s]%

op l2 : s * s * s -> s

%[op= (op __<=__<=__ : s * s * s -> s) as s * s * s -> s]%

op l3 : s

%[op=

(op __<=__<=__ : s * s * s -> s)

((op a : s), (op b : s), (op c : s))

as s]%

op l4 : s

%[op=

(op __<=__<=__ : s * s * s -> s)

((op a : s), (op b : s), (op c : s))

as s]%

op l5 : s * s * s

%[op= ((op a : s), (op b : s), (op c : s)) as s * s * s]%

op x : s %(op)%

op y : s

%[op=

(op __<=__<=__ : s * s * s -> s)

((op a : s), (var x : s), (op a : s))

as s]%

op z : s

%[op=

(op __+__ : s * s -> s) ((op x : s) as s, (op x : s) as t as s) as

s]%

. c = ((op __+__ : s * s -> s) (a, b) as s)

. d = ((op __+__ : s * s -> s) (a, a) as s)

. e = ((op __+__ : s * s -> s) as s * s -> s)

. f = ((op __+__ : s * s -> s) as s * s -> s)

. g = (((op a : s), (op b : s)) as s * s)

. h = ((op __+__ : s * s -> s) (a, b) as s)

. i = ((op __+__ : s * s -> s) (a, b) as s)

. i1 = (incr a as s)

. i2 = (incr a as s)

. i3 = (incr a as s)

. l1 = ((a <= b <= c) as s)

. l2 = (__<=__<=__ as s * s * s -> s)

. l3 = ((a <= b <= c) as s)

. l4 = ((a <= b <= c) as s)

. l5 = (((op a : s), (op b : s), c) as s * s * s)

forall x : s . y = ((a <= (var x : s) <= a) as s)

. z = ((op __+__ : s * s -> s) (x as s, x as t as s) as s)

. x in s %(bla_label)%

. x in t

### Hint 7.14,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 7.14,

no kind found for 's'

expected: {Cppo}

found: {Type}

### Hint 8.14,

no kind found for 't'

expected: {Cpo}

found: {Type}

### Hint 8.14,

no kind found for 't'

expected: {Cppo}

found: {Type}

### Warning 9.7, expected tuple argument for '__+__'

### Hint 13.12-13.16,

in type of '((op a : s), (op b : s))'

typename 't' (9.14)

is not unifiable with type 's * s' (3.12)

### Hint 13.12-13.16,

in type of '((op a : s), (op b : t))'

typename 't' (9.14)

is not unifiable with type 's * t' (11.10)

### Hint 13.12-13.16,

in type of '((op a : t), (op b : s))'

typename 't' (9.14)

is not unifiable with type 't * s' (11.10)

### Hint 13.12-13.16,

in type of '((op a : t), (op b : t))'

typename 't' (9.14)

is not unifiable with type 't * t' (11.10)

### Hint 13.12-13.16, untypeable term (with type: t) '(a, b)'

### Hint 13.12-13.16,

rejected 't < s' of '((op a : s), (op b : t))'

### Hint 13.12-13.16,

rejected 't < s' of '((op a : t), (op b : s))'

### Hint 13.12-13.16,

rejected 't < s' of '((op a : t), (op b : t))'

### Hint 15.14-15.21,

in type of '((op a : s), (op a : s))'

typename 't' (9.14)

is not unifiable with type 's * s' (15.21)

### Hint 15.14-15.21,

in type of '((op a : s), (op a : t))'

typename 't' (9.14)

is not unifiable with type 's * t' (15.21)

### Hint 15.14-15.21,

in type of '((op a : t), (op a : s))'

typename 't' (9.14)

is not unifiable with type 't * s' (15.21)

### Hint 15.14-15.21,

in type of '((op a : t), (op a : t))'

typename 't' (9.14)

is not unifiable with type 't * t' (15.21)

### Hint 15.14-15.21, untypeable term (with type: t) '(a, a)'

### Hint 15.14-15.21,

rejected 't < s' of '((op a : s), (op a : t))'

### Hint 15.14-15.21,

rejected 't < s' of '((op a : t), (op a : s))'

### Hint 15.14-15.21,

rejected 't < s' of '((op a : t), (op a : t))'

### Hint 17.8,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 17.8,

no kind found for 's'

expected: {Cppo}

found: {Type}

### Hint 17.6-17.24,

in type of '(op __+__ : t -> t -> t) as s * s -> s'

typename 't' (9.14)

is not unifiable with type 's * s' (17.12)

### Hint 19.8,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 19.8,

no kind found for 's'

expected: {Cppo}

found: {Type}

### Hint 19.6-19.25,

in type of '(op __+__ : t -> t -> t) as s * s -> s'

typename 't' (9.14)

is not unifiable with type 's * s' (19.12)

### Hint 21.8,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 21.8,

no kind found for 's'

expected: {Cppo}

found: {Type}

### Hint 23.23-23.26,

in type of '((op a : s), (op b : s))'

typename 't' (9.14)

is not unifiable with type 's * s' (3.12)

### Hint 23.23-23.26,

in type of '((op a : s), (op b : t))'

typename 't' (9.14)

is not unifiable with type 's * t' (11.10)

### Hint 23.23-23.26,

in type of '((op a : t), (op b : s))'

typename 't' (9.14)

is not unifiable with type 't * s' (11.10)

### Hint 23.23-23.26,

in type of '((op a : t), (op b : t))'

typename 't' (9.14)

is not unifiable with type 't * t' (11.10)

### Hint 23.23-23.26, untypeable term (with type: t) '(a, b)'

### Hint 23.23-23.26,

rejected 't < s' of '((op a : s), (op b : t))'

### Hint 23.23-23.26,

rejected 't < s' of '((op a : t), (op b : s))'

### Hint 23.23-23.26,

rejected 't < s' of '((op a : t), (op b : t))'

### Hint 25.23-25.25, rejected 't < s' of '(op a : t) : s'

### Hint 25.30-25.32, rejected 't < s' of '(op b : t) : s'

### Hint 25.23-25.35,

in type of '((op a : s), (op b : s))'

typename 't' (9.14)

is not unifiable with type 's * s' (25.35)

### Hint 25.23-25.35,

untypeable term (with type: t) '(a : s, b : s)'

### Hint 25.23-25.25, rejected 't < s' of '(op a : t) : s'

### Hint 25.30-25.32, rejected 't < s' of '(op b : t) : s'

### Hint 25.23-25.25, rejected 't < s' of '(op a : t) : s'

### Hint 25.30-25.32, rejected 't < s' of '(op b : t) : s'

### Hint 30.18, rejected 't < s' of '(op a : t)'

### Hint 31.19, rejected 't < s' of '(op a : t)'

### Hint 32.21, rejected 't < s' of '(op a : t)'

### Hint 34.21,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 34.21,

no kind found for 's'

expected: {Cppo}

found: {Type}

### Hint 36.13-36.19,

rejected 't < s' of '((op a : s), (op b : t), (op c : s))'

### Hint 36.13-36.19,

rejected 't < s' of '((op a : t), (op b : s), (op c : s))'

### Hint 36.13-36.19,

rejected 't < s' of '((op a : t), (op b : t), (op c : s))'

### Hint 37.9,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 37.9,

no kind found for 's'

expected: {Cppo}

found: {Type}

### Hint 38.29-38.36,

rejected 't < s' of '((op a : s), (op b : t), (op c : s))'

### Hint 38.29-38.36,

rejected 't < s' of '((op a : t), (op b : s), (op c : s))'

### Hint 38.29-38.36,

rejected 't < s' of '((op a : t), (op b : t), (op c : s))'

### Hint 39.31-39.38,

rejected 't < s' of '((op a : s), (op b : t), (op c : s))'

### Hint 39.31-39.38,

rejected 't < s' of '((op a : t), (op b : s), (op c : s))'

### Hint 39.31-39.38,

rejected 't < s' of '((op a : t), (op b : t), (op c : s))'

### Hint 40.9,

no kind found for 's'

expected: {Cpo}

found: {Type}

### Hint 40.9,

no kind found for 's'

expected: {Cppo}

found: {Type}

### Hint 44.42-44.44, rejected 't < s' of '(op a : t) : s'

### Hint 46.12-46.38,

in type of '((op x : s) as s, (op x : s) as t as s)'

typename 't' (9.14)

is not unifiable with type 's * s' (46.38)

### Hint 46.12-46.38,

untypeable term (with type: t) '(x as s, x as t as s)'