%%%%%%%%%%%%%%%%%%%
%   definitions   %
%%%%%%%%%%%%%%%%%%%

:- op(200,xfy,[equal_set,inc]).
:- op(150,xfx,[inter,union]).

definition(maps(F, A, B) <=> for_all(X elt A, exists(Y elt B,..[F,X] :Y))
                              and for_all(X elt A, for_all(Y1 elt B, for_all(Y2 elt B,
                                           (..[F,X] :Y1) and (..[F,X] :Y2) 
                                                               => (Y1 = Y2))))).
definition(comp(G, F, A, B, C):H <=> for_all(X elt A, for_all(Z elt C, 
                  ..[H,X] :Z <=> exists(Y elt B, ..[F,X] :Y and ..[G,Y] :Z)))).
definition(A  equal_set B <=>  A inc B and B inc A).
definition(equiv(E, R) <=> 
           for_all(X elt E, ..[R,X,X] )
          and for_all(X elt E, for_all(Y elt E, ..[R, X, Y] => ..[R, Y, X]))
          and for_all(X elt E,for_all(Y elt E,for_all(Z elt E,
                        ..[R,X,Y] and ..[R,Y,Z] => ..[R,X,Z])))
           ).
definition(image(F,A) = [Y, exists(X elt A, ..[F,X] : Y)]).
definition((A inc B) <=> for_all(X,(X elt A => X elt B))).
definition(partition(A, E) <=> for_all(X elt A, X inc E)
                          and for_all(X elt E, exists(Y elt A, X elt Y))
                          and for_all(X elt A, for_all(Y elt A,
                               exists(Z,Z elt X and Z elt Y) => (X = Y)))).
definition(powerset(A) = [X, X inc A]).
definition(A inter B = [X,X elt A and X elt B]).
definition(transitive(R)  <=>
           for_all(X ,for_all(Y ,for_all(Z ,
                        (..[R,X,Y] and ..[R,Y,Z] => ..[R,X,Z]))))).
definition(transitive(R,E) <=>
            for_all(X elt E,for_all(Y elt E,for_all(Z elt E,
                        (..[R,X,Y] and ..[R,Y,Z] => ..[R,X,Z]))))).
definition(A union B = [X,X elt A or X elt B]).