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 : forall S : Type . Set S;

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

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

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

__union__, __intersection__, __\\__ : forall S : Type .

Set S * Set S -> Set S;

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

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

__disjointUnion__ : forall S : Type .

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

inl, inr : forall S : Type . S -> S * Bool

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

. (fun not__ : Unit ->? Unit)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

forall x : S . (fun __=>__ : Unit * Unit ->? Unit)

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

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

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

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

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

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

(var x : S,

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

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

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

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

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

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

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

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

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

(var x : S,

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

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

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

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

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

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

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

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

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

(var x : S,

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

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

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

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

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

(fun not__ : Unit ->? Unit)

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

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

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

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

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

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

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

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

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

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

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

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

(op __*__

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Bool : Type

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

S : Type %(var)%

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

T : Type %(var)%

Unit : Type := Unit

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

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

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

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

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

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

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

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

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

false : Bool %(op)%

: Unit %(fun)%

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

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

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

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

true : Bool %(op)%

: Unit %(fun)%

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

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

(fun not__ : Unit ->? Unit)

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

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

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

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

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

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

(var x : S, var x' : S)) %()%

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

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

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

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

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

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

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

forall x : S . (fun __=>__ : Unit * Unit ->? Unit)

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

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

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

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

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

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

(var x : S,

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

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

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

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

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

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

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

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

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

(var x : S,

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

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

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

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

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

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

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

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

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

(var x : S,

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

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

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

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

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

(fun not__ : Unit ->? Unit)

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

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

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

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

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

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

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

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

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

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

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

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

(op __*__

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

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

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

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

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

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

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

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

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

(var x : S, op false : Bool)) %()%

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

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

(var x : S, op true : Bool)) %()%

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

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

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

*** Hint 3.18, redeclared type 'S'

*** Hint 3.8, redeclared type 'Pred'

*** Hint 4.17, redeclared type 'S'