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;

class

Cpo : Type

types

Chain : Cpo -> Type;

Nat : Type;

gn_t28 : -Type -> +Type -> Type

type

gn_t28 < __->?__

type

Chain := gn_t28 Nat

var

a : Cpo %(var_29)%

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

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

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

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

### Hint 7.27-7.49, constrain 'a : Cpo' is unprovable

*** Error 7.27-7.49,

in term 'forall n : Nat

. def (var s : Nat ->? a) (var n : Nat)

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

((var s : Nat ->? a) (var n : Nat),

(var s : Nat ->? a)

((op __+__ : Nat * Nat -> Nat) ((var n : Nat), (op 1 : Nat))))' of type 'Unit'

unresolved constraints

'{a : Cpo}'

### 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'