type s, t < t

op a, b : s

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

op __+__ : s * s -> s

op __+__ : t * t -> t

op a, b : t

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

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

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

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

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

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

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

op incr : s -> s

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

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

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

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

op l1 : s

= ((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s

op l2 : s * s * s -> s

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

op l3 : s

= ((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s

op l4 : s

= ((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s

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

op x : s

op y : s

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

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

s) as

s

op z : s

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

((op x : s) as s, ((op x : s) as t) as s) :

s) as

s

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

. (op x : s) in t

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

Logical : Type := Unit ->? Unit

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

Unit : Type

__*__ : Type+ -> Type+ -> Type

__-->__ : Type- -> Type+ -> Type < (__-->?__, __->__)

__-->?__ : Type- -> Type+ -> Type < __->?__

__->__ : Type- -> Type+ -> Type < __->?__

__->?__ : Type- -> Type+ -> Type

s : Type < t

t : Type < t

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

__+__

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

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

__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

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

__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__when__else__

: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

a : t %(op)%

: s %(op)%

b : t %(op)%

: s %(op)%

bottom : forall a : Type . a_v-1 %(fun)%

c : s

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

d : s

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

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

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

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

false : Unit %(fun)%

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

h : s

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

i : s

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

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

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

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

incr : s -> s %(op)%

l1

: s

%(op)%

= ((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s

l2

: s * s * s -> s

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

l3

: s

%(op)%

= ((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s

l4

: s

%(op)%

= ((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s

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

not__ : ? Unit ->? Unit %(fun)%

true : Unit %(fun)%

x : s %(op)%

y : s

%(op)%

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

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

s) as

s

z : s

%(op)%

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

((op x : s) as s, ((op x : s) as t) as s) :

s) as

s

�__ : ? Unit ->? Unit %(fun)%

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

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op c : s,

((op __+__ : s * s -> s)(op a : s, op b : s) : s) as s) %(def_c)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op d : s,

((op __+__ : s * s -> s)(op a : s, op a : s) : s) as s) %(def_d)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op e : s * s -> s,

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

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op f : s * s -> s,

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

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op g : s * s, (op a : s, op b : s) as s * s) %(def_g)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op h : s,

((op __+__ : s * s -> s)(op a : s, op b : s) : s) as s) %(def_h)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op i : s,

((op __+__ : s * s -> s)(op a : s, op b : s) : s) as s) %(def_i)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op i1 : s, ((op incr : s -> s)(op a : s) : s) as s) %(def_i1)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op i2 : s, ((op incr : s -> s)(op a : s) : s) as s) %(def_i2)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op i3 : s, ((op incr : s -> s)(op a : s) : s) as s) %(def_i3)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op l1 : s,

((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s) %(def_l1)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op l2 : s * s * s -> s,

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

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op l3 : s,

((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s) %(def_l3)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op l4 : s,

((op __<=__<=__ : s * s * s -> s)(op a : s, op b : s, op c : s) :

s) as

s) %(def_l4)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op l5 : s * s * s,

(op a : s, op b : s, op c : s) as s * s * s) %(def_l5)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op y : s,

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

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

s) as

s) %(def_y)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op z : s,

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

s) as

s) %(def_z)%

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

(op x : s) in t

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

*** Error 9.7, expected tuple argument for '__+__'

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

type 's * s'

is not unifiable with type 'Unit ->? t * t'

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

type 's * s'

is not unifiable with type 'Unit ->? s * s'

*** Hint 15.17-15.21, in type of '(op a : s, op a : s)'

type 's * s' (15.21)

is not unifiable with type 'Unit ->? t * t' (15.21)

*** Hint 15.17-15.21, in type of '(op a : s, op a : s)'

type 's * s' (15.21)

is not unifiable with type 'Unit ->? s * s' (15.21)

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

type 's * s'

is not unifiable with type 'Unit ->? t * t' (23.27)

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

type 's * s'

is not unifiable with type 'Unit ->? s * s' (23.27)

*** Hint 25.30-25.35, in type of '(op a : s, op b : s)'

type 's * s' (25.35)

is not unifiable with type 'Unit ->? t * t' (25.35)

*** Hint 25.30-25.35, in type of '(op a : s, op b : s)'

type 's * s' (25.35)

is not unifiable with type 'Unit ->? s * s' (25.35)

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

typename 's' (3.12)

is not unifiable with type 'Unit ->? s'

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

typename 's' (3.12)

is not unifiable with type 'Unit ->? s' (31.19)

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

typename 's' (3.12)

is not unifiable with type 'Unit ->? s' (32.22)

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

type 's * s * s'

is not unifiable with type 'Unit ->? s * s * s'

*** Hint 38.35-38.36, in type of '(op a : s, op b : s, op c : s)'

type 's * s * s' (38.36)

is not unifiable with type 'Unit ->? s * s * s' (38.36)

*** Hint 39.37-39.38, in type of '(op a : s, op b : s, op c : s)'

type 's * s * s' (39.38)

is not unifiable with type 'Unit ->? s * s * s' (39.38)

*** Hint 44.23-44.47, in type of '((op a : s) : s, var x : s, op a : s)'

type 's * s * s' (44.47)

is not unifiable with type 'Unit ->? s * s * s' (44.47)

*** Hint 46.12-46.38, in type of '((op x : s) as s, ((op x : s) as t) as s)'

type 's * s' (46.38)

is not unifiable with type 'Unit ->? t * t' (46.38)

*** Hint 46.12-46.38, in type of '((op x : s) as s, ((op x : s) as t) as s)'

type 's * s' (46.38)

is not unifiable with type 'Unit ->? s * s' (46.38)