type s, t < t

op a, b : s

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

op __+__ : s � s -> s

op __+__ : t � t -> t

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

op a, b : t

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

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

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

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

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

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

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

op incr : s -> s

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

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

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

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

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

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

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

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

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

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

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

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

op x : s

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

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

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

(op x : s) as t as s)

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

. (op x : s) in t

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

Pred : Type -> Type := \ a : Type . a ->? Unit

Unit : Type := Unit

s : Type < t

t : Type < t

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

__+__ : t -> t -> t

: t � t -> t

: s � s -> s

__/\__ : Unit � Unit ->? Unit

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

__<=>__ : Unit � Unit ->? Unit

__=__ : forall a : Type . a � a ->? Unit

__=>__ : Unit � Unit ->? Unit

__=e=__ : forall a : Type . a � a ->? Unit

__\/__ : Unit � Unit ->? Unit

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))

def__ : forall a : Type . a ->? Unit

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))

i : s = (op __+__ : s � s -> s) ((op a : s) : s, (op b : s) : 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)

if__then__else__ : forall a : Type . Unit � a � a ->? a

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))

not__ : Unit ->? Unit

x : s

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 9, column 19) type 's' is not unifiable with 't -> t'

Hint (line 8, column 23) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 9, column 19) type 's' is not unifiable with 't -> t'

Hint (line 8, column 23) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

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

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

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

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

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 9, column 19) type 's' is not unifiable with 't -> t'

Hint (line 8, column 23) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 9, column 19) type 's' is not unifiable with 't -> t'

Hint (line 8, column 23) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 11, column 10) type 's' is not unifiable with 't'

Hint (line 9, column 19) type 's' is not unifiable with 't -> t'

Hint (line 8, column 23) type 's' is not unifiable with 't'