2N/Atypes s, t < t

2N/Aops a, b : s

2N/A

2N/A%% op __ + __ : s -> s -> s, idem, assoc, comm;

2N/Aop __+__ : s * s -> s

2N/Aop __+__ : t * t -> t

2N/Aops a, b : t

2N/Aop c : s = a + b;

2N/Aop d : s = a + a;

2N/Aop e : s * s -> s = __+__;

2N/Aop f : s * s -> s = __+__;

2N/Aop g : s * s = (a, b);

2N/Aop h : s = a + b;

2N/Aop i : s = (a : s) + (b : s);

2N/Aop incr : s -> s

2N/Aop i1 : s = incr a;

2N/Aop i2 : s = incr a;

2N/Aop i3 : s = incr a;

2N/Aop __<=__<=__ : s * s * s -> s

2N/Aop l1 : s = a <= b <= c;

2N/Aop l2 : s * s * s -> s = __<=__<=__;

2N/Aop l3 : s = a <= b <= c;

2N/Aop l4 : s = a <= b <= c;

2N/Aop l5 : s * s * s = (a, b, c);

2N/Aop x : s

2N/Aop y : s = (op a : s) <= (var x : s) <= (a : s);

2N/Aop z : s = (x as s) + (x as t as s);

2N/A. x in s %(bla_label)%

2N/A. x in t;

2N/A%% Type Constructors -----------------------------------------------------

2N/As : Type < t

2N/At : Type

2N/A%% Assumptions -----------------------------------------------------------

2N/A__+__

2N/A: t * t -> t %(op)%

2N/A: s * s -> s %(op)%

2N/A__<=__<=__ : s * s * s -> s %(op)%

2N/Aa

2N/A: t %(op)%

2N/A: s %(op)%

2N/Ab

2N/A: t %(op)%

2N/A: s %(op)%

2N/Ac

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

2N/Ad

2N/A: s %(op)% = (op __+__ : s * s -> s) ((op a : s), (op a : s)) as s

2N/Ae : s * s -> s %(op)% = (op __+__ : s * s -> s) as s * s -> s

2N/Af : s * s -> s %(op)% = (op __+__ : s * s -> s) as s * s -> s

2N/Ag : s * s %(op)% = ((op a : s), (op b : s)) as s * s

2N/Ah

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

2N/Ai

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

2N/Ai1 : s %(op)% = (op incr : s -> s) (op a : s) as s

2N/Ai2 : s %(op)% = (op incr : s -> s) (op a : s) as s

2N/Ai3 : s %(op)% = (op incr : s -> s) (op a : s) as s

2N/Aincr : s -> s %(op)%

2N/Al1

2N/A: s

2N/A%(op)% =

2N/A(op __<=__<=__ : s * s * s -> s)

2N/A((op a : s), (op b : s), (op c : s))

2N/Aas s

2N/Al2

2N/A: s * s * s -> s

2N/A%(op)% = (op __<=__<=__ : s * s * s -> s) as s * s * s -> s

2N/Al3

2N/A: s

2N/A%(op)% =

2N/A(op __<=__<=__ : s * s * s -> s)

2N/A((op a : s), (op b : s), (op c : s))

2N/Aas s

2N/Al4

2N/A: s

2N/A%(op)% =

2N/A(op __<=__<=__ : s * s * s -> s)

2N/A((op a : s), (op b : s), (op c : s))

2N/Aas s

2N/Al5

2N/A: s * s * s

2N/A%(op)% = ((op a : s), (op b : s), (op c : s)) as s * s * s

2N/Ax : s %(op)%

2N/Ay

2N/A: s

2N/A%(op)% =

2N/A(op __<=__<=__ : s * s * s -> s)

2N/A((op a : s), (var x : s), (op a : s))

2N/Aas s

2N/Az

2N/A: s

2N/A%(op)% =

2N/A(op __+__ : s * s -> s) ((op x : s) as s, (op x : s) as t as s) as

2N/As

2N/A%% Sentences -------------------------------------------------------------

2N/Ac = ((op __+__ : s * s -> s) ((op a : s), (op b : s)) as s)

2N/A %(def_c)%

2N/Ad = ((op __+__ : s * s -> s) ((op a : s), (op a : s)) as s)

2N/A %(def_d)%

2N/Ae = ((op __+__ : s * s -> s) as s * s -> s) %(def_e)%

2N/Af = ((op __+__ : s * s -> s) as s * s -> s) %(def_f)%

2N/Ag = (((op a : s), (op b : s)) as s * s) %(def_g)%

2N/Ah = ((op __+__ : s * s -> s) ((op a : s), (op b : s)) as s)

2N/A %(def_h)%

2N/Ai = ((op __+__ : s * s -> s) ((op a : s), (op b : s)) as s)

2N/A %(def_i)%

2N/Ai1 = (incr (op a : s) as s) %(def_i1)%

2N/Ai2 = (incr (op a : s) as s) %(def_i2)%

2N/Ai3 = (incr (op a : s) as s) %(def_i3)%

2N/Al1 = ((op a : s) <= (op b : s) <= c as s) %(def_l1)%

2N/Al2 = (__<=__<=__ as s * s * s -> s) %(def_l2)%

2N/Al3 = ((op a : s) <= (op b : s) <= c as s) %(def_l3)%

2N/Al4 = ((op a : s) <= (op b : s) <= c as s) %(def_l4)%

2N/Al5 = (((op a : s), (op b : s), c) as s * s * s) %(def_l5)%

2N/Ay = ((a : s) <= (var x : s) <= (op a : s) as s) %(def_y)%

2N/Az = ((op __+__ : s * s -> s) (x as s, x as t as s) as s) %(def_z)%

2N/Ax in s %(bla_label)%

2N/Ax in t

2N/A%% Diagnostics -----------------------------------------------------------

2N/A*** Error 9.7, expected tuple argument for '__+__'

2N/A