var S : Type

type Set S := S ->? Unit

op __isIn__ : S * Set S ->? Unit

ops reflexive, symmetric, transitive : Pred (Set (S * S))

forall r : Set (S * S)

. reflexive r <=> forall x : S . r (x, x)

. symmetric r <=> forall x, y : S . r (x, y) => r (y, x)

. transitive r

<=> forall x, y, z : S . r (x, y) /\ r (y, z) => r (x, y);

type PER S = {r : Set (S * S) . symmetric r /\ transitive r}

op dom : PER S -> Set S

vars x : S; r : PER S

. x isIn dom r <=> (x, x) isIn r;

types

PER : Type -> Type;

Set : Type -> Type;

gn_t10[gn_t9[PER]] : -Type -> +Type -> Type;

gn_t9[PER] : Type -> +Type -> Type

type

gn_t10[gn_t9[PER]] < __->?__

types

PER (S : Type) := gn_t9[PER] S Unit;

Set (S : Type) := S ->? Unit;

gn_t9[PER] (S : Type) := gn_t10[gn_t9[PER]] (S * S)

var

S : Type %(var_1)%

op __isIn__ : forall S : Type . S * Set S ->? Unit

op dom : forall S : Type . PER S -> Set S

op reflexive : forall S : Type . Pred (Set (S * S))

op symmetric : forall S : Type . Pred (Set (S * S))

op transitive : forall S : Type . Pred (Set (S * S))

vars

r : PER S;

x : S

forall S : Type; r : Set (S * S)

. reflexive r <=> forall x : S . r (x, x)

forall S : Type; r : Set (S * S)

. symmetric r <=> forall x, y : S . r (x, y) => r (y, x)

forall S : Type; r : Set (S * S)

. transitive r

<=> forall x, y, z : S . r (x, y) /\ r (y, z) => r (x, y)

forall S : Type

. forall r : Set (S * S)

. (r in PER S) <=> symmetric r /\ transitive r

forall S : Type; r : PER S; x : S . x isIn dom r <=> (x, x) isIn r

### Hint 1.7, is type variable 'S'

### Hint 3.20,

no kind found for 'S'

expected: {Cpo}

found: {Type}

### Hint 3.20,

no kind found for 'S'

expected: {Cppo}

found: {Type}

### Hint 4.51,

no kind found for 'S'

expected: {Cpo}

found: {Type}

### Hint 4.51,

no kind found for 'S'

expected: {Cppo}

found: {Type}

### Hint 4.51,

no kind found for 'S'

expected: {Cpo}

found: {Type}

### Hint 4.51,

no kind found for 'S'

expected: {Cppo}

found: {Type}

### Hint 4.51,

no kind found for 'S'

expected: {Cpo}

found: {Type}

### Hint 4.51,

no kind found for 'S'

expected: {Cppo}

found: {Type}

### Hint 5.11, not a kind 'Set (S * S)'

### Hint 5.16,

no kind found for 'S'

expected: {Cpo}

found: {Type}

### Hint 5.16,

no kind found for 'S'

expected: {Cppo}

found: {Type}

### Hint 6.29, not a class 'S'

### Hint 7.29, not a class 'S'

### Hint 7.31, not a class 'S'

### Hint 8.30, not a class 'S'

### Hint 8.32, not a class 'S'

### Hint 8.34, not a class 'S'

### Hint 9.26,

no kind found for 'S'

expected: {Cpo}

found: {Type}

### Hint 9.26,

no kind found for 'S'

expected: {Cppo}

found: {Type}

### Hint 11.8, not a class 'S'

### Hint 11.13, not a kind 'PER S'