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

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

definition(application(F, A, B) <=> qqs(X app A, ilexiste(Y app B,..[F,X] :Y))
                              et qqs(X app A, qqs(Y1 app B, qqs(Y2 app B,
                                           (..[F,X] :Y1) et (..[F,X] :Y2) 
                                                               => (Y1 = Y2))))).
definition(comp(G, F, A, B, C):H <=> qqs(X app A, qqs(Z app C, 
                  ..[H,X] :Z <=> ilexiste(Y app B, ..[F,X] :Y et ..[G,Y] :Z)))).
definition(A  egal_ens B <=>  A inc B et B inc A).
definition(equiv(E, R) <=> 
           qqs(X app E, ..[R,X,X] )
          et qqs(X app E, qqs(Y app E, ..[R, X, Y] => ..[R, Y, X]))
          et qqs(X app E,qqs(Y app E,qqs(Z app E,
                        ..[R,X,Y] et ..[R,Y,Z] => ..[R,X,Z])))
           ).
definition(image(F,A) = [Y, ilexiste(X app A, ..[F,X] : Y)]).
definition((A inc B) <=> qqs(X,(X app A => X app B))).
definition(partition(A, E) <=> qqs(X app A, X inc E)
                          et qqs(X app E, ilexiste(Y app A, X app Y))
                          et qqs(X app A, qqs(Y app A,
                               ilexiste(Z,Z app X et Z app Y) => (X = Y)))).
definition(parties(A) = [X, X inc A]).
definition(A inter B = [X,X app A et X app B]).
definition(transitive(R)  <=>
           qqs(X ,qqs(Y ,qqs(Z ,
                        (..[R,X,Y] et ..[R,Y,Z] => ..[R,X,Z]))))).
definition(transitive(R,E) <=>
            qqs(X app E,qqs(Y app E,qqs(Z app E,
                        (..[R,X,Y] et ..[R,Y,Z] => ..[R,X,Z]))))).
definition(A union B = [X,X app A ou X app B]).