%% Type Constructors -----------------------------------------------------

s : Type

t : Type

%% Assumptions -----------------------------------------------------------

__+__ : t -> t -> t

: t � t -> t

: s � s -> s

__<=__<=__ : s � s � s -> s

a : t

: s

b : t

: s

c : s = (op __+__ : s � s -> s) ((op a : s), (op b : s))

d : s = (op __+__ : s � s -> s) ((op a : s), (op a : s))

e : s � s -> s = (op __+__ : s � s -> s)

f : s � s -> s = (op __+__ : s � s -> s)

g : s � s = (((op a : s), (op b : s)))

h : s = (op __+__ : s � s -> s) (((op a : s), (op b : s)))

i1 : s = (op incr : s -> s) (op a : s)

i2 : s = (op incr : s -> s) (op a : s)

i3 : s = (op incr : s -> s) (op a : s)

incr : s -> s

l1 : s = (op __<=__<=__ : s � s � s -> s) ((op a : s), (op b : s),

(op c : s))

l2 : s � s � s -> s = (op __<=__<=__ : s � s � s -> s)

l3 : s = (op __<=__<=__ : s � s � s -> s) (((op a : s), (op b : s),

(op c : s)))

l4 : s = (op __<=__<=__ : s � s � s -> s) (((op a : s), (op b : s),

(op c : s)))

l5 : s � s � s = (((op a : s), (op b : s), (op c : s)))

x : s %(var)%

y : s = (op __<=__<=__ : s � s � s -> s) ((op a : s), (var x : s),

(op a : s) : s)

z : s = (op __+__ : s � s -> s) ((op x : s) as s,

(op x : s) as t as s)

%% Sentences -------------------------------------------------------------

(op x : s) in s %(bla_label)%

(op x : s) in t %()%

%% Diagnostics -----------------------------------------------------------

Hint (line 7, column 14) type 't' is not unifiable with 's'

Hint (line 8, column 14) type 't' is not unifiable with 't � t'

Hint (line 7, column 14) type 't' is not unifiable with 's � s'

Hint (line 3, column 12) type 't' is not unifiable with 's'

Hint (line 3, column 12) type 't' is not unifiable with 's'

Hint (line 40, column 9) not a class 's'