bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedertypes s, t < t

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederops a, b : s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

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

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop __+__ : s * s -> s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop __+__ : t * t -> t

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederops a, b : t

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop c : s = a + b;

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop d : s = a + a;

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop e : s * s -> s = __+__;

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop f : s * s -> s = __+__;

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop g : s * s = (a, b);

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop h : s = a + b;

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop i : s = (a : s) + (b : s);

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop incr : s -> s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop i1 : s = incr a;

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop i2 : s = incr a;

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederop i3 : s = incr a;

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop __<=__<=__ : s * s * s -> s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop l1 : s = a <= b <= c;

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederop l2 : s * s * s -> s = __<=__<=__;

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederop l3 : s = a <= b <= c;

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederop l4 : s = a <= b <= c;

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

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederop x : s

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

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederop z : s = (x as s) + (x as t as s);

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder. x in s %(bla_label)%

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder. x in t;

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder%% Type Constructors -----------------------------------------------------

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeders : Type < t

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maedert : Type

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder%% Assumptions -----------------------------------------------------------

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder__+__ : s * s -> s %(op)%

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder__+__ : t * t -> t %(op)%

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

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maedera : s %(op)%

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maedera : t %(op)%

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederb : s %(op)%

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederb : t %(op)%

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederc : s

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

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederd : s

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

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maedere : s * s -> s %(op)% = (op __+__ : t * t -> t) as s * s -> s

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederf : s * s -> s %(op)% = (op __+__ : t * t -> t) as s * s -> s

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

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederh : s

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

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederi : s

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

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

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

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

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maederincr : s -> s %(op)%

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maederl1 : s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder %(op)% =

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

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

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder as s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederl2 : s * s * s -> s

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

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederl3 : s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder %(op)% =

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

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

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder as s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederl4 : s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder %(op)% =

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

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

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder as s

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederl5 : s * s * s

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

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederx : s %(op)%

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maedery : s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder %(op)% =

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

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

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder as s

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederz : s

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder %(op)% =

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

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder s

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder%% Sentences -------------------------------------------------------------

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederc = ((op __+__ : t * t -> t) ((op a : s), (op b : s)) as s)

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder %(def_c)%

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederd = ((op __+__ : t * t -> t) ((op a : s), (op a : s)) as s)

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder %(def_d)%

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maedere = ((op __+__ : t * t -> t) as s * s -> s) %(def_e)%

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederf = ((op __+__ : t * t -> t) as s * s -> s) %(def_f)%

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederg = (((op a : s), (op b : s)) as s * s) %(def_g)%

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maederh = ((op __+__ : t * t -> t) ((op a : s), (op b : s)) as s)

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder %(def_h)%

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maederi = ((op __+__ : t * t -> t) ((op a : s), (op b : s)) as s)

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder %(def_i)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederi1 = (incr (op a : s) as s) %(def_i1)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederi2 = (incr (op a : s) as s) %(def_i2)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederi3 = (incr (op a : s) as s) %(def_i3)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederl1 = ((op a : s) <= (op b : s) <= c as s) %(def_l1)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederl2 = (__<=__<=__ as s * s * s -> s) %(def_l2)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederl3 = ((op a : s) <= (op b : s) <= c as s) %(def_l3)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederl4 = ((op a : s) <= (op b : s) <= c as s) %(def_l4)%

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

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maedery = ((a : s) <= (var x : s) <= (op a : s) as s) %(def_y)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederz = ((op __+__ : t * t -> t) (x as s, x as t as s) as s) %(def_z)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederx in s %(bla_label)%

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederx in t

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder%% Diagnostics -----------------------------------------------------------

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

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder