09688ec5ffb8b9cf9883a770e2f9ebd60b28888dTripptype s, t < t

0fdefaa9ca017edfb76b736c825b34186f33045aTrippop a, b : s

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

0fdefaa9ca017edfb76b736c825b34186f33045aTrippop __+__ : s * s -> s

0fdefaa9ca017edfb76b736c825b34186f33045aTrippop __+__ : t * t -> t

0fdefaa9ca017edfb76b736c825b34186f33045aTrippop : t -> t -> t

09688ec5ffb8b9cf9883a770e2f9ebd60b28888dTrippop a, b : t

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

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

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

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

828c58761d90445b8b9d20a82d85dc1479317f71Trippop g : s * s = (op a : s, op b : s)

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

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

ed59119d8c00addb07c7ee6c8aefcd1d9cb876f1Trippop incr : s -> s

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

828c58761d90445b8b9d20a82d85dc1479317f71Trippop i2 : s = (op incr : s -> s)(op a : s)

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

828c58761d90445b8b9d20a82d85dc1479317f71Trippop __<=__<=__ : s * s * s -> s

c7ba96d16d58075a9ab8d5c1e46c6c83ce11cb4eTrippop l1 : s

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

66ca16dd76367c074fe4df1dcf7b555489a9bf85Trippop l2 : s * s * s -> s = (op __<=__<=__ : s * s * s -> s)

66ca16dd76367c074fe4df1dcf7b555489a9bf85Trippop l3 : s

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

66ca16dd76367c074fe4df1dcf7b555489a9bf85Trippop l4 : s

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

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

e7c7565d9550eaa87043aef0df77125ada996deaTrippop x : s

e7c7565d9550eaa87043aef0df77125ada996deaTrippop y : s

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

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

828c58761d90445b8b9d20a82d85dc1479317f71Trippop z : s

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

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp. (op x : s) in t

828c58761d90445b8b9d20a82d85dc1479317f71Tripp%% Type Constructors -----------------------------------------------------

828c58761d90445b8b9d20a82d85dc1479317f71TrippPred : Type -> Type := \ a : Type . a ->? Unit

828c58761d90445b8b9d20a82d85dc1479317f71TrippUnit : Type := Unit

828c58761d90445b8b9d20a82d85dc1479317f71Tripp__*__ : Type+ -> Type+ -> Type

828c58761d90445b8b9d20a82d85dc1479317f71Tripp__-->__ : Type- -> Type+ -> Type

828c58761d90445b8b9d20a82d85dc1479317f71Tripp__-->?__ : Type- -> Type+ -> Type

753e68bea51094492944cd3cd92191c91d1e7c50Tripp__->__ : Type- -> Type+ -> Type

753e68bea51094492944cd3cd92191c91d1e7c50Tripp__->?__ : Type- -> Type+ -> Type

c7ba96d16d58075a9ab8d5c1e46c6c83ce11cb4eTripps : Type < t

828c58761d90445b8b9d20a82d85dc1479317f71Trippt : Type < t

828c58761d90445b8b9d20a82d85dc1479317f71Tripp%% Assumptions -----------------------------------------------------------

828c58761d90445b8b9d20a82d85dc1479317f71Tripp__+__ : s * s -> s %(op)%

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

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

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

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

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

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

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

753e68bea51094492944cd3cd92191c91d1e7c50Tripp__if__ : Unit * Unit ->? Unit %(fun)%

753e68bea51094492944cd3cd92191c91d1e7c50Tripp__when__else__ : forall a : Type . a * Unit * a ->? a %(fun)%

753e68bea51094492944cd3cd92191c91d1e7c50Trippa : s %(op)%

753e68bea51094492944cd3cd92191c91d1e7c50Trippb : s %(op)%

753e68bea51094492944cd3cd92191c91d1e7c50Trippbottom : forall a : Type . a %(fun)%

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

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

753e68bea51094492944cd3cd92191c91d1e7c50Trippdef__ : forall a : Type . a ->? Unit %(fun)%

753e68bea51094492944cd3cd92191c91d1e7c50Trippe : s * s -> s %(op)% = (op __+__ : s * s -> s)

753e68bea51094492944cd3cd92191c91d1e7c50Trippf : s * s -> s %(op)% = (op __+__ : s * s -> s)

753e68bea51094492944cd3cd92191c91d1e7c50Trippfalse : Unit %(fun)%

753e68bea51094492944cd3cd92191c91d1e7c50Trippg : s * s %(op)% = (op a : s, op b : s)

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

753e68bea51094492944cd3cd92191c91d1e7c50Trippi : s

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

753e68bea51094492944cd3cd92191c91d1e7c50Trippi1 : s %(op)% = (op incr : s -> s)(op a : s)

753e68bea51094492944cd3cd92191c91d1e7c50Trippi2 : s %(op)% = (op incr : s -> s)(op a : s)

753e68bea51094492944cd3cd92191c91d1e7c50Trippi3 : s %(op)% = (op incr : s -> s)(op a : s)

753e68bea51094492944cd3cd92191c91d1e7c50Trippincr : s -> s %(op)%

753e68bea51094492944cd3cd92191c91d1e7c50Trippl1

753e68bea51094492944cd3cd92191c91d1e7c50Tripp : s

753e68bea51094492944cd3cd92191c91d1e7c50Tripp %(op)%

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

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

753e68bea51094492944cd3cd92191c91d1e7c50Trippl3

828c58761d90445b8b9d20a82d85dc1479317f71Tripp : s

828c58761d90445b8b9d20a82d85dc1479317f71Tripp %(op)%

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

828c58761d90445b8b9d20a82d85dc1479317f71Trippl4

828c58761d90445b8b9d20a82d85dc1479317f71Tripp : s

828c58761d90445b8b9d20a82d85dc1479317f71Tripp %(op)%

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

828c58761d90445b8b9d20a82d85dc1479317f71Trippl5 : s * s * s %(op)% = (op a : s, op b : s, op c : s)

828c58761d90445b8b9d20a82d85dc1479317f71Trippnot__ : Unit ->? Unit %(fun)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripptrue : Unit %(fun)%

828c58761d90445b8b9d20a82d85dc1479317f71Trippx : s %(op)%

828c58761d90445b8b9d20a82d85dc1479317f71Trippy : s

828c58761d90445b8b9d20a82d85dc1479317f71Tripp %(op)%

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

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

828c58761d90445b8b9d20a82d85dc1479317f71Trippz : s

828c58761d90445b8b9d20a82d85dc1479317f71Tripp %(op)%

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp%% Sentences -------------------------------------------------------------

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op c : s, (op __+__ : s * s -> s)(op a : s, op b : s)) %(def_c)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op d : s, (op __+__ : s * s -> s)(op a : s, op a : s)) %(def_d)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op e : s * s -> s, op __+__ : s * s -> s) %(def_e)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op f : s * s -> s, op __+__ : s * s -> s) %(def_f)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op h : s, (op __+__ : s * s -> s)(op a : s, op b : s)) %(def_h)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op i : s,

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op l1 : s,

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op a : s, op b : s, op c : s)) %(def_l1)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op l2 : s * s * s -> s, op __<=__<=__ : s * s * s -> s) %(def_l2)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op l3 : s,

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op a : s, op b : s, op c : s)) %(def_l3)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op l4 : s,

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op a : s, op b : s, op c : s)) %(def_l4)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op l5 : s * s * s, (op a : s, op b : s, op c : s)) %(def_l5)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op y : s,

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op a : s, var x : s, (op a : s) : s)) %(def_y)%

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(fun __=__ : forall a : Type . a * a ->? Unit)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op z : s,

828c58761d90445b8b9d20a82d85dc1479317f71Tripp (op __+__ : s * s -> s)

828c58761d90445b8b9d20a82d85dc1479317f71Tripp ((op x : s) as s, (op x : s) as t as s)) %(def_z)%

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp(op x : s) in t

828c58761d90445b8b9d20a82d85dc1479317f71Tripp%% Diagnostics -----------------------------------------------------------

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

828c58761d90445b8b9d20a82d85dc1479317f71Tripp