2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars a: Ord; x: a
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederop __<=__ : Pred (a * a)
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederclasses BoundedOrd < Ord
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedervars a: Ord; b: BoundedOrd
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maederop __<=__ : Pred (a * a);
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedervars x, y, z: a; v: b
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. x <= y /\ y <= z => x <= z
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. x <= y /\ y <= x => x = y
6b7d53eb1a93b9a9d7e3ce48964128fcd142fe53Christian Maedervars a, b: Ord
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedertype instances a * b: Ord
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedervars x, y: a; v, w: b
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. (x, v) <= (y, w) <=> x <= y /\ v <= w
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederclass instance DiscreteOrd < Ord
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedervars a: DiscreteOrd; x, y: a
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. x <= y <=> x = y
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedervars a: Ord; b: Num
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maederops min: a * a ->? a;
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maeder min: b * b ->? b
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedervars a: Ord; b: Ord
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maederop __<=__ : Pred ((a ->? b) * (a ->? b))
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedertype instance a ->? b: Ord
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedertype instance Unit: Ord
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maedertype instance ?a: Ord
4ea69d9a971bbb8b4082bcd60350fdabd5411c23Christian Maeder. x <= y <=> def x() => x() <= y()
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maederclass Cpo < Ord
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maederop __<=__ : Pred (a * a)