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__)

((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (op emptySet[S] : forall S : Type . Set S))))

. (__<=>__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S),

(op {__}[S] : forall S : Type . S -> Set S) (var x' : S))),

(__=__) (((var x : S), (var x' : S)))))

. (__<=>__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s : Set S))),

(var s : Set S) (var x : S)))

. (__<=>__)

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

(((var s : Set S), (var s' : Set S))),

forall x : S

. (__=>__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s : Set S))),

(op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s' : Set S)))))))

. (__<=>__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S),

(op __union__[S] : forall S : Type . Set S * Set S -> Set S)

(((var s : Set S), (var s' : Set S))))),

(__\/__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s : Set S))),

(op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s' : Set S)))))))

. (__<=>__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S),

(op __intersection__[S] : forall S : Type . Set S * Set S -> Set S)

(((var s : Set S), (var s' : Set S))))),

(__/\__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s : Set S))),

(op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s' : Set S)))))))

. (__<=>__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S),

(op __\\__[S] : forall S : Type . Set S * Set S -> Set S)

(((var s : Set S), (var s' : Set S))))),

(__/\__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s : Set S))),

(not__)

((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s' : Set S))))))))

. (__<=>__)

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

(((var s : Set S), (var s' : Set S))),

(__=__)

(((op __intersection__[S] :

forall S : Type . Set S * Set S -> Set S)

(((var s : Set S), (var s' : Set S))),

(op emptySet[S] : forall S : Type . Set S)))))

. (__<=>__)

(((op __isIn__[S * T] : forall S : Type . S * Set S ->? Unit)

((((var x : S), (var y : T)),

(op __*__[S; T] :

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

(((var s : Set S), (var t : Set T))))),

(__/\__)

(((op __isIn__[S] : forall S : Type . S * Set S ->? Unit)

(((var x : S), (var s : Set S))),

(op __isIn__[T] : forall S : Type . S * Set S ->? Unit)

(((var y : T), (var t : Set T)))))))

. (__=__)

(((op inl[S] : forall S : Type . S -> S * Bool) (var x : S),

((var x : S), (op False : Bool))))

. (__=__)

(((op inr[S] : forall S : Type . S -> S * Bool) (var x : S),

((var x : S), (op True : Bool))))

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

? : +Type -> Type

Bool : Type

Logical : Type := ? Unit

Pred : -Type -> Type := \ a : -Type . a ->? Unit

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

Unit : Type

__*__ : +Type -> +Type -> Type

__*__*__ : +Type -> +Type -> +Type -> Type

__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

__-->?__ : -Type -> +Type -> Type < __->?__

__->__ : -Type -> +Type -> Type < __->?__

__->?__ : -Type -> +Type -> Type

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

__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=__ : forall a : Type . a * a ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__\\__ : 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)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__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)%

__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

bottom : forall a : Type . a %(fun)%

def__ : forall a : Type . a ->? Unit %(fun)%

emptySet : forall S : Type . Set S %(op)%

false : Unit %(fun)%

inl : forall S : Type . S -> S * Bool %(op)%

inr : forall S : Type . S -> S * Bool %(op)%

not__ : ? Unit ->? Unit %(fun)%

true : Unit %(fun)%

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

�__ : ? Unit ->? Unit %(fun)%

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

s : Set S

s' : Set S

t : Set T

x : S

x' : S

y : T

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

not ((__isIn__) ((x, emptySet)))

((__isIn__) ((x, ({__}) x'))) <=> ((__=__) ((x, x')))

((__isIn__) ((x, s))) <=> (s (x))

((__subset__) ((s, s'))) <=>

(forall x : S . ((__isIn__) ((x, s))) => ((__isIn__) ((x, s'))))

((__isIn__) ((x, (__union__) ((s, s'))))) <=>

(((__isIn__) ((x, s))) \/ ((__isIn__) ((x, s'))))

((__isIn__) ((x, (__intersection__) ((s, s'))))) <=>

(((__isIn__) ((x, s))) /\ ((__isIn__) ((x, s'))))

((__isIn__) ((x, (__\\__) ((s, s'))))) <=>

(((__isIn__) ((x, s))) /\ (not ((__isIn__) ((x, s')))))

((__disjoint__) ((s, s'))) <=>

((__=__) (((__intersection__) ((s, s')), emptySet)))

((__isIn__) (((x, y), (__*__) ((s, t))))) <=>

(((__isIn__) ((x, s))) /\ ((__isIn__) ((y, 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'