class Cpo

var a : -Cpo

fun __<=__ : Pred (a * a)

type Nat

ops 1 : Nat;

__+__ : Nat * Nat -> Nat

type Chain a =

{s : Nat ->? a . forall n : Nat . def s n => s n <= s (n + 1)}

var a : Cpo

fun sup : Chain a ->? a

vars x : ? a; c : Chain a

. sup c <= x <=> forall n : Nat . c n <= x;

types

Chain : Cpo -> Type;

Nat : Type;

gn_t25 : -Type -> +Type -> Type

type

gn_t25 < __->?__

type

Chain := gn_t25 Nat

var

a : Cpo %(var_26)%

op 1 : Nat %(op)%

op __+__ : Nat * Nat -> Nat %(op)%

op __<=__ : forall a : -Cpo . Pred (a * a) %(fun)%

op sup : forall a : Cpo . Chain a ->? a %(fun)%

vars

c : Chain a;

x : ? a

forall a : Cpo; c : Chain a; x : ? a

. sup c <= x <=> forall n : Nat . c n <= x

### Warning 1.7, unchanged class 'Cpo'

### Hint 2.8, is type variable 'a'

### Hint 6.15, rebound type variable 'a'

### Hint 7.35, not a class 'Nat'

### Hint 8.8, is type variable 'a'

### Hint 8.8, rebound type variable 'a'

### Hint 10.9, not a kind '? a'

### Hint 10.16, not a kind 'Chain a'

### Hint 11.26, not a class 'Nat'