2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maederclass Cpo

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maedervar a : -Cpo

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maederfun __ <= __ : Pred (a * a)

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maedertype Nat

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maederops 1 : Nat; __ + __ : Nat * Nat -> Nat

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maedertype Chain (a : Cpo) = {s: Nat ->? a .

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maeder forall n: Nat . def s n => s n <= s (n + 1)}

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maedervar a : Cpo

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maederfun sup: Chain a ->? a

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maedervar x: ?a; c: Chain a

2f6324a12df5979e1e0e3dfcec95c0546fc37c30Christian Maeder. sup c <= x <=> forall n: Nat . c n <= x