/* 

A little fragment of set theory to execise reduction with equivalences.
Used in JSC04 paper.

*/

% set theory


% equality
eq_elem(S,T) == (S=T).

% extensional equality on binary relations
eq(S,T) == all(X,all(Y,contains(S,(X,Y)) <=> contains(T,(X,Y)))).
%eq(S,T) -> (S=T).


% cartesian product of relations
contains(product(S,T),(A,B)) == (contains(S,A) and contains(T,B)).

% composition
contains((S;T),(X,Y)) == exists(Z,contains(S,(X,Z)) and contains(T,(Z,Y))).

% Boolean operations
contains(union(S,T),X) == (contains(S,X) or contains(T,X)).

contains(intersection(S,T),X) == (contains(S,X) and contains(T,X)).

% binary relation R subseteq D x C
rel(R,D,C)==all(X,all(Y,(contains(R,(X,Y)) => contains(D,X) and contains(C,Y)))).


% the image of a relation F
contains(image(F),Y) == exists(X,contains(F,(X,Y))).

% the image of F on S
contains(image(F,S),Y) == exists(X,contains(S,X) and contains(F,(X,Y))).


% the identity
contains(id(T),(X,Y)) == (eq_elem(X,Y) and contains(T,X)).

% total relations
total(F,D)  == all(X,contains(D,X) => exists(Y,contains(F,(X,Y)))).

% unique relations
unique(F)   == all(X,all(Y,all(Z,contains(F,(X,Y)) and contains(F,(X,Z)) => eq_elem(Y,Z)))).

% partial functions
pfunc(F,D,C) ==  (rel(F,D,C) and unique(F)).

% injective relations
injective(F) == 
      all(X,all(Y,all(Z,contains(F,(X,Z)) and contains(F,(Y,Z)) => eq_elem(X,Y)))).

% functions
func(F,D,C)  == (pfunc(F,D,C) and total(F,D)).



% we prove that the 
% composition of relations with injective functions is injective.

goal
~(
    rel(p,s,t) and rel(q,s,t) and
    func(f,t,b) and injective(f) =>
                 
                 eq((p;f),(q;f)) => eq(p,q)
 ).