Graphs.hascasl.output revision 4fb19f237193a3bd6778f8aee3b6dd8da5856665
var S : Type; T : Type
type Bool; Pred : Type -> Type := \ S : Type . S_v-1 ->? Unit;
Set : Type -> Type := \ S : Type . S_v-1 ->? 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 ->? Unit);
s' : Set S@(S ->? Unit); t : Set T@(T ->? Unit)
. (fun not__ : Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
op emptySet[S] : forall S : Type . Set S_v-1@(S_v-1 ->? Unit)))
. (fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
(op {__}[S]
: forall S : Type . S_v-1 -> Set S_v-1@(S_v-1 ->? Unit))
(var x' : S)),
(fun __=__[S] : forall a : Type . a_v-1 * a_v-1 ->? Unit)
(var x : S, var x' : S))
. (fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(var s : Set S@(S ->? Unit))(var x : S))
. (fun __<=>__ : Unit * Unit ->? Unit)
((op __subset__[S]
: forall S : Type .
Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),
forall x : S
. (fun __=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s' : Set S@(S ->? Unit))))
. (fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
(op __union__[S]
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),
(fun __\/__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s' : Set S@(S ->? Unit))))
. (fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
(op __intersection__[S]
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),
(fun __/\__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s' : Set S@(S ->? Unit))))
. (fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
(op __\\__[S]
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),
(fun __/\__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(fun not__ : Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s' : Set S@(S ->? Unit)))))
. (fun __<=>__ : Unit * Unit ->? Unit)
((op __disjoint__[S]
: forall S : Type .
Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),
(fun __=__[S ->? Unit] : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op __intersection__[S]
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),
op emptySet[S] : forall S : Type . Set S_v-1@(S_v-1 ->? Unit)))
. (fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S * T]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
((var x : S, var y : T),
(op __*__[S; T]
: forall S : Type; T : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set T_v-2@(T_v-2 ->? Unit) -> Set (S_v-1 * T_v-2)@(S_v-1 *
T_v-2 ->? Unit))
(var s : Set S@(S ->? Unit), var t : Set T@(T ->? Unit))),
(fun __/\__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(op __isIn__[T]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var y : T, var t : Set T@(T ->? Unit))))
. (fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op inl[S] : forall S : Type . S_v-1 -> S_v-1 * Bool)(var x : S),
(var x : S, op False : Bool))
. (fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op inr[S] : forall S : Type . S_v-1 -> S_v-1 * Bool)(var x : S),
(var x : S, op True : Bool))
%% Type Constructors -----------------------------------------------------
Bool : Type
Logical : Type := Unit ->? Unit
Pred : Type -> Type := \ a : Type . a_v-1 ->? Unit
S : Type %(var_1)%
Set : Type -> Type := \ S : Type . S_v-1 ->? Unit
T : Type %(var_2)%
Unit : Type := Unit
__*__ : Type+ -> Type+ -> Type
__-->__ : Type- -> Type+ -> Type
__-->?__ : Type- -> Type+ -> Type
__->__ : Type- -> Type+ -> Type
__->?__ : Type- -> Type+ -> Type
%% Assumptions -----------------------------------------------------------
False : Bool %(op)%
True : Bool %(op)%
__*__
: forall S : Type; T : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set T_v-2@(T_v-2 ->? Unit) -> Set (S_v-1 * T_v-2)@(S_v-1 *
T_v-2 ->? Unit)
%(op)%
__/\__ : Unit * Unit ->? Unit %(fun)%
__<=>__ : Unit * Unit ->? Unit %(fun)%
__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=>__ : Unit * Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__\/__ : Unit * Unit ->? Unit %(fun)%
__\\__
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)
%(op)%
__disjoint__
: forall S : Type .
Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
%(op)%
__disjointUnion__
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set (S_v-1 * Bool)@(S_v-1 *
Bool ->? Unit)
%(op)%
__if__ : Unit * Unit ->? Unit %(fun)%
__intersection__
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)
%(op)%
__isIn__
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit
%(op)%
__subset__
: forall S : Type .
Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
%(op)%
__union__
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)
%(op)%
__when__else__
: forall a : Type . a_v-1 * Unit * a_v-1 ->? a_v-1 %(fun)%
bottom : forall a : Type . a_v-1 %(fun)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
emptySet : forall S : Type . Set S_v-1@(S_v-1 ->? Unit) %(op)%
false : Unit %(fun)%
inl : forall S : Type . S_v-1 -> S_v-1 * Bool %(op)%
inr : forall S : Type . S_v-1 -> S_v-1 * Bool %(op)%
not__ : Unit ->? Unit %(fun)%
true : Unit %(fun)%
{__} : forall S : Type . S_v-1 -> Set S_v-1@(S_v-1 ->? Unit) %(op)%
�__ : Unit ->? Unit %(fun)%
%% Sentences -------------------------------------------------------------
(fun not__ : Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
op emptySet[S] : forall S : Type . Set S_v-1@(S_v-1 ->? Unit)))
(fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
(op {__}[S]
: forall S : Type . S_v-1 -> Set S_v-1@(S_v-1 ->? Unit))
(var x' : S)),
(fun __=__[S] : forall a : Type . a_v-1 * a_v-1 ->? Unit)
(var x : S, var x' : S))
(fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(var s : Set S@(S ->? Unit))(var x : S))
(fun __<=>__ : Unit * Unit ->? Unit)
((op __subset__[S]
: forall S : Type .
Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),
forall x : S
. (fun __=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s' : Set S@(S ->? Unit))))
(fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
(op __union__[S]
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),
(fun __\/__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s' : Set S@(S ->? Unit))))
(fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
(op __intersection__[S]
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),
(fun __/\__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s' : Set S@(S ->? Unit))))
(fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S,
(op __\\__[S]
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),
(fun __/\__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(fun not__ : Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s' : Set S@(S ->? Unit)))))
(fun __<=>__ : Unit * Unit ->? Unit)
((op __disjoint__[S]
: forall S : Type .
Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),
(fun __=__[S ->? Unit] : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op __intersection__[S]
: forall S : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))
(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),
op emptySet[S] : forall S : Type . Set S_v-1@(S_v-1 ->? Unit)))
(fun __<=>__ : Unit * Unit ->? Unit)
((op __isIn__[S * T]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
((var x : S, var y : T),
(op __*__[S; T]
: forall S : Type; T : Type .
Set S_v-1@(S_v-1 ->? Unit) *
Set T_v-2@(T_v-2 ->? Unit) -> Set (S_v-1 * T_v-2)@(S_v-1 *
T_v-2 ->? Unit))
(var s : Set S@(S ->? Unit), var t : Set T@(T ->? Unit))),
(fun __/\__ : Unit * Unit ->? Unit)
((op __isIn__[S]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var x : S, var s : Set S@(S ->? Unit)),
(op __isIn__[T]
: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)
(var y : T, var t : Set T@(T ->? Unit))))
(fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op inl[S] : forall S : Type . S_v-1 -> S_v-1 * Bool)(var x : S),
(var x : S, op False : Bool))
(fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op inr[S] : forall S : Type . S_v-1 -> S_v-1 * 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'