OpDecls.hascasl.output revision b55cf4375478168316b212cbc7d261fb683645ff
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski%% op __ + __ : s -> s -> s, idem, assoc, comm;
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop __+__ : s * s -> s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop __+__ : t * t -> t
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop c : s = (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop d : s = (op __+__ : s * s -> s) ((op a : s), (op a : s)) as s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop e : s * s -> s = (op __+__ : s * s -> s) as s * s -> s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop f : s * s -> s = (op __+__ : s * s -> s) as s * s -> s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop g : s * s = ((op a : s), (op b : s)) as s * s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop h : s = (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop i : s = (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop incr : s -> s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop i1 : s = (op incr : s -> s) (op a : s) as s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop i2 : s = (op incr : s -> s) (op a : s) as s
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowskiop i3 : s = (op incr : s -> s) (op a : s) as s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskiop __<=__<=__ : s * s * s -> s
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski = (op __<=__<=__ : s * s * s -> s)
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski ((op a : s), (op b : s), (op c : s))
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowskiop l2 : s * s * s -> s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski = (op __<=__<=__ : s * s * s -> s) as s * s * s -> s
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski = (op __<=__<=__ : s * s * s -> s)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski ((op a : s), (op b : s), (op c : s))
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski = (op __<=__<=__ : s * s * s -> s)
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski ((op a : s), (op b : s), (op c : s))
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowskiop l5 : s * s * s
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski = ((op a : s), (op b : s), (op c : s)) as s * s * s
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski = (op __<=__<=__ : s * s * s -> s)
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski ((op a : s), (var x : s), (op a : s))
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski = (op __+__ : s * s -> s) ((op x : s) as s, (op x : s) as t as s)
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski. (op x : s) in s %(bla_label)%
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski. (op x : s) in t
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski%% Type Constructors -----------------------------------------------------
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski? : +Type -> Type
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiLogical : Type := ? Unit
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiPred : -Type -> Type := \ a : -Type . a ->? Unit
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski__*__ : +Type -> +Type -> Type
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski__*__*__ : +Type -> +Type -> +Type -> Type
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski__-->?__ : -Type -> +Type -> Type < __->?__
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski__->__ : -Type -> +Type -> Type < __->?__
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski__->?__ : -Type -> +Type -> Type
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski%% Assumptions -----------------------------------------------------------
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski : t * t -> t %(op)%
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski : s * s -> s %(op)%
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski__<=__<=__ : s * s * s -> s %(op)%
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski__=__ : forall a : Type . a * a ->? Unit %(fun)%
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski__if__ : ? Unit * ? Unit ->? Unit %(fun)%
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowskibottom : forall a : Type . a %(fun)%
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski %(op)% = (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski %(op)% = (op __+__ : s * s -> s) ((op a : s), (op a : s)) as s
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowskidef__ : forall a : Type . a ->? Unit %(fun)%
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowskie : s * s -> s %(op)% = (op __+__ : s * s -> s) as s * s -> s
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowskif : s * s -> s %(op)% = (op __+__ : s * s -> s) as s * s -> s
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskifalse : Unit %(fun)%
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskig : s * s %(op)% = ((op a : s), (op b : s)) as s * s
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski %(op)% = (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski %(op)% = (op __+__ : s * s -> s) ((op a : s), (op b : s)) as s
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskii1 : s %(op)% = (op incr : s -> s) (op a : s) as s
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskii2 : s %(op)% = (op incr : s -> s) (op a : s) as s
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskii3 : s %(op)% = (op incr : s -> s) (op a : s) as s
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskiincr : s -> s %(op)%
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski = (op __<=__<=__ : s * s * s -> s)
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski ((op a : s), (op b : s), (op c : s))
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski : s * s * s -> s
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski %(op)% = (op __<=__<=__ : s * s * s -> s) as s * s * s -> s
36e567ca4ae0eabbfc918b98b96762b5cf07bbb8Till Mossakowski = (op __<=__<=__ : s * s * s -> s)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski ((op a : s), (op b : s), (op c : s))
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski = (op __<=__<=__ : s * s * s -> s)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski ((op a : s), (op b : s), (op c : s))
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski %(op)% = ((op a : s), (op b : s), (op c : s)) as s * s * s
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowskinot__ : ? Unit ->? Unit %(fun)%
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowskitrue : Unit %(fun)%
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski = (op __<=__<=__ : s * s * s -> s)
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski ((op a : s), (var x : s), (op a : s))
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski = (op __+__ : s * s -> s) ((op x : s) as s, (op x : s) as t as s)
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski�__ : ? Unit ->? Unit %(fun)%
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski%% Sentences -------------------------------------------------------------
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski((op __+__ : s * s -> s) ((op a : s), (op b : s)) as s) %(def_c)%
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski((op __+__ : s * s -> s) ((op a : s), (op a : s)) as s) %(def_d)%
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskie = ((op __+__ : s * s -> s) as s * s -> s) %(def_e)%
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskif = ((op __+__ : s * s -> s) as s * s -> s) %(def_f)%
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowskig = (((op a : s), (op b : s)) as s * s) %(def_g)%
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski((op __+__ : s * s -> s) ((op a : s), (op b : s)) as s) %(def_h)%
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowski((op __+__ : s * s -> s) ((op a : s), (op b : s)) as s) %(def_i)%
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowskii1 = (incr (op a : s) as s) %(def_i1)%
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowskii2 = (incr (op a : s) as s) %(def_i2)%
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskii3 = (incr (op a : s) as s) %(def_i3)%
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederl1 = ((op a : s) <= (op b : s) <= c as s) %(def_l1)%
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskil2 = (__<=__<=__ as s * s * s -> s) %(def_l2)%
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskil3 = ((op a : s) <= (op b : s) <= c as s) %(def_l3)%
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskil4 = ((op a : s) <= (op b : s) <= c as s) %(def_l4)%
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskil5 = (((op a : s), (op b : s), c) as s * s * s) %(def_l5)%
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskiy = ((a : s) <= (var x : s) <= (op a : s) as s) %(def_y)%
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskiz = ((op __+__ : s * s -> s) (x as s, x as t as s) as s) %(def_z)%
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskix in s %(bla_label)%
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski%% Diagnostics -----------------------------------------------------------
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski*** Error 9.7, expected tuple argument for '__+__'