vars S, T : Type

types Bool;

Pred S := S ->? Unit;

Set S := S ->? Unit

ops True, False : Bool

ops emptySet : Set S;

{__} : S -> Set S;

__isIn__ : S * Set S ->? Unit;

__subset__ : Pred (Set (S) * Set (S));

__union__, __intersection__, __ \\ __ : Set S * Set S -> Set S;

__disjoint__ : Pred (Set (S) * Set (S));

__ * __ : Set S * Set T -> Set (S * T);

__disjointUnion__ : Set S * Set S -> Set (S * Bool);

inl, inr : S -> S * Bool

forall x, x' : S; y : T; s, s' : Set S; t : Set T

. not x isIn emptySet

. x isIn { x' } <=> x = x'

. x isIn s <=> s x

. s subset s' <=> forall x : S . x isIn s => x isIn s'

. x isIn (s union s') <=> x isIn s \/ x isIn s'

. x isIn (s intersection s') <=> x isIn s /\ x isIn s'

. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'

. s disjoint s' <=> s intersection s' = emptySet

. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t

. inl x = (x, False)

. inr x = (x, True);

types

Bool : Type;

Set : Type -> Type

type

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

vars

S : Type % (var_1) %;

T : Type % (var_2) %

op False : Bool

op True : Bool

op __ * __ : forall S : Type; T : Type . Set S * Set T -> Set (S * T)

op __ \\ __ : forall S : Type . Set S * Set S -> Set S

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

op __disjointUnion__ : forall S : Type

. Set S * Set S -> Set (S * Bool)

op __intersection__ : forall S : Type . Set S * Set S -> Set S

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

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

op __union__ : forall S : Type . Set S * Set S -> Set S

op emptySet : forall S : Type . Set S

op inl : forall S : Type . S -> S * Bool

op inr : forall S : Type . S -> S * Bool

op {__} : forall S : Type . S -> Set S

forall S : Type; x : S . not x isIn emptySet

forall S : Type; x : S; x' : S . x isIn { x' } <=> x = x'

forall S : Type; s : Set S; x : S . x isIn s <=> s x

forall S : Type; s : Set S; s' : Set S

. s subset s' <=> forall x : S . x isIn s => x isIn s'

forall S : Type; s : Set S; s' : Set S; x : S

. x isIn (s union s') <=> x isIn s \/ x isIn s'

forall S : Type; s : Set S; s' : Set S; x : S

. x isIn (s intersection s') <=> x isIn s /\ x isIn s'

forall S : Type; s : Set S; s' : Set S; x : S

. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'

forall S : Type; s : Set S; s' : Set S

. s disjoint s' <=> s intersection s' = emptySet

forall S : Type; T : Type; s : Set S; t : Set T; x : S; y : T

. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t

forall S : Type; x : S . inl x = (x, False)

forall S : Type; x : S . inr x = (x, True)

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

1.8 : ### Hint : is type variable 'T'

3.14 : ### Hint : rebound type variable 'S'

3.8 - 3.11 : ### Hint : redeclared type 'Pred'

4.13 : ### Hint : rebound type variable 'S'

9.18 : ### Hint :

no kind found for 'S'

expected : {Cpo}

found : {Type}

9.18 : ### Hint :

no kind found for 'S'

expected : {Cppo}

found : {Type}

10.25 - 10.29 : ### Hint :

no kind found for 'Set S'

expected : {Cpo}

found : {Type}

10.25 - 10.29 : ### Hint :

no kind found for 'Set S'

expected : {Cppo}

found : {Type}

11.46 - 11.50 : ### Hint :

no kind found for 'Set S'

expected : {Cpo}

found : {Type}

11.46 - 11.50 : ### Hint :

no kind found for 'Set S'

expected : {Cppo}

found : {Type}

11.46 - 11.50 : ### Hint :

no kind found for 'Set S'

expected : {Cpo}

found : {Type}

11.46 - 11.50 : ### Hint :

no kind found for 'Set S'

expected : {Cppo}

found : {Type}

11.46 - 11.50 : ### Hint :

no kind found for 'Set S'

expected : {Cpo}

found : {Type}

11.46 - 11.50 : ### Hint :

no kind found for 'Set S'

expected : {Cppo}

found : {Type}

12.28 - 12.32 : ### Hint :

no kind found for 'Set S'

expected : {Cpo}

found : {Type}

12.28 - 12.32 : ### Hint :

no kind found for 'Set S'

expected : {Cppo}

found : {Type}

13.15 - 13.19 : ### Hint :

no kind found for 'Set S'

expected : {Cpo}

found : {Type}

13.15 - 13.19 : ### Hint :

no kind found for 'Set S'

expected : {Cppo}

found : {Type}

13.37 : ### Hint :

no kind found for 'S'

expected : {Cpo}

found : {Type}

13.37 : ### Hint :

no kind found for 'S'

expected : {Cppo}

found : {Type}

14.28 - 14.32 : ### Hint :

no kind found for 'Set S'

expected : {Cpo}

found : {Type}

14.28 - 14.32 : ### Hint :

no kind found for 'Set S'

expected : {Cppo}

found : {Type}

14.50 : ### Hint :

no kind found for 'S'

expected : {Cpo}

found : {Type}

14.50 : ### Hint :

no kind found for 'S'

expected : {Cppo}

found : {Type}

15.22 : ### Hint :

no kind found for 'S'

expected : {Cpo}

found : {Type}

15.22 : ### Hint :

no kind found for 'S'

expected : {Cppo}

found : {Type}

15.22 : ### Hint :

no kind found for 'S'

expected : {Cpo}

found : {Type}

15.22 : ### Hint :

no kind found for 'S'

expected : {Cppo}

found : {Type}

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

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

16.19 : ### Hint : not a class 'T'

16.24 : ### Hint : not a kind 'Set (S) '

16.27: ### Hint: not a kind ' Set (S) '

16.37: ### Hint: not a kind ' Set (T) '

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

20.31 : ### Hint : rebound variable 'x'