43b4c41fbb07705c9df321221ab9cb9832460407Christian Maedertype s, t < t

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maederop a, b : s

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

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop __+__ : s * s -> s

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederop __+__ : t * t -> t

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop a, b : t

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

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

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

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

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

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

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

c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maederop incr : s -> s

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

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

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

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederop __<=__<=__ : s * s * s -> s

a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maederop l1 : s

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

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich (((op a : s), (op b : s), (op c : s)))

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder as s

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederop l2 : s * s * s -> s

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

4cb215739e9ab13447fa21162482ebe485b47455Christian Maederop l3 : s

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

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich (((op a : s), (op b : s), (op c : s)))

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder as s

74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maederop l4 : s

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

3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder (((op a : s), (op b : s), (op c : s)))

ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder as s

3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maederop l5 : s * s * s

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

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederop x : s

e593b89bfd4952698dc37feced21cefe869d87a2Christian Maederop y : s

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

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (((op a : s), (var x : s), (op a : s)))

7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder as s

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederop z : s

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder = (op __+__ : s * s -> s) (((op x : s) as s, (op x : s) as t as s))

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder as s

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

7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder. (op x : s) in t

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder%% Type Constructors -----------------------------------------------------

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder? : +Type -> Type

1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederLogical : Type := ? Unit

c3053d57f642ca507cdf79512e604437c4546cb9Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit

dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian MaederUnit : Type

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder__*__ : +Type -> +Type -> Type

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder__*__*__ : +Type -> +Type -> +Type -> Type

dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

05a62e84edac8c64de04f8349dee418598d216b9Christian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder__->__ : -Type -> +Type -> Type < __->?__

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder__->?__ : -Type -> +Type -> Type

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeders : Type < t

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maedert : Type

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder%% Assumptions -----------------------------------------------------------

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder__+__

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder : t * t -> t %(op)%

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

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

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

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

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder__=__ : forall a : Type . a * a ->? Unit %(fun)%

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

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

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

f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich__if__ : ? Unit * ? Unit ->? Unit %(fun)%

6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maedera : t %(op)%

431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder : s %(op)%

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederb : t %(op)%

498aa48bdb931ab50990d3b74318a5db2312186cChristian Maeder : s %(op)%

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederbottom : forall a : Type . a %(fun)%

6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederc : s

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

6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederd : s

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

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederdef__ : forall a : Type . a ->? Unit %(fun)%

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

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederf : s * s -> s %(op)% = (op __+__ : s * s -> s) as s * s -> s

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederfalse : Unit %(fun)%

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

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederh : s

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

9e748851c150e1022fb952bab3315e869aaf0214Christian Maederi : s

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

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

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

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

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

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederl1

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder : s

a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder %(op)%

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

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder (((op a : s), (op b : s), (op c : s)))

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder as s

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maederl2

a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder : s * s * s -> s

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

bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maederl3

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder : s

1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder %(op)%

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

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder (((op a : s), (op b : s), (op c : s)))

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder as s

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maederl4

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder : s

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder %(op)%

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

4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder (((op a : s), (op b : s), (op c : s)))

a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder as s

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederl5

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder : s * s * s

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

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maedernot__ : ? Unit ->? Unit %(fun)%

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maedertrue : Unit %(fun)%

a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maederx : s %(op)%

dc679edd4ca027663212afdf00926ae2ce19b555Christian Maedery : s

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder %(op)%

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

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (((op a : s), (var x : s), (op a : s)))

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder as s

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederz : s

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder %(op)%

4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder = (op __+__ : s * s -> s) (((op x : s) as s, (op x : s) as t as s))

b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder as s

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

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich%% Sentences -------------------------------------------------------------

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederc =

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

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederd =

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

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

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

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

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maederh =

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

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maederi =

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

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

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

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

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

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

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

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

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

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

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederz =

3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder((op __+__ : s * s -> s) ((x as s, x as t as s)) as s) %(def_z)%

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederx in s %(bla_label)%

6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederx in t

d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder%% Diagnostics -----------------------------------------------------------

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

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder