var S : Type; T : Type

type Bool;

Pred : -Type -> Type := \ S : -Type . S ->? Unit;

Set : Type -> Type := \ S : Type . S ->? Unit;

op True, False : Bool;

op 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 : S; x' : S; y : T; s : Set 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)

%% Type Constructors -----------------------------------------------------

Bool : Type

Set : Type -> Type := \ S : Type . S ->? Unit

%% Type Variables --------------------------------------------------------

S : Type %(var_1)%

T : Type %(var_2)%

%% Assumptions -----------------------------------------------------------

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 %(op)%

%% Variables -------------------------------------------------------------

s : Set S

s' : Set S

t : Set T

x : S

x' : S

y : T

%% Sentences -------------------------------------------------------------

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)

%% Diagnostics -----------------------------------------------------------

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

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

### Hint 3.19, rebound type variable 'S'

### Hint 3.8, redeclared type 'Pred'

### Hint 4.17, rebound type variable 'S'

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

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

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

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

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

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

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

### Hint 20.31, rebound variable 'x'