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

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

3.20: ### Hint:

no kind found for 'S'

expected: {Cpo}

found: {Type}

3.20: ### Hint:

no kind found for 'S'

expected: {Cppo}

found: {Type}

4.51: ### Hint:

no kind found for 'S'

expected: {Cpo}

found: {Type}

4.51: ### Hint:

no kind found for 'S'

expected: {Cppo}

found: {Type}

4.51: ### Hint:

no kind found for 'S'

expected: {Cpo}

found: {Type}

4.51: ### Hint:

no kind found for 'S'

expected: {Cppo}

found: {Type}

4.51: ### Hint:

no kind found for 'S'

expected: {Cpo}

found: {Type}

4.51: ### Hint:

no kind found for 'S'

expected: {Cppo}

found: {Type}

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

5.16: ### Hint:

no kind found for 'S'

expected: {Cpo}

found: {Type}

5.16: ### Hint:

no kind found for 'S'

expected: {Cppo}

found: {Type}

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

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

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

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

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

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

9.26: ### Hint:

no kind found for 'S'

expected: {Cpo}

found: {Type}

9.26: ### Hint:

no kind found for 'S'

expected: {Cppo}

found: {Type}

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

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