% We introduce two isomorphic graphs G and H,
% and an isomorphism between them by the identifier F.
defThAs( graphIsom( G,F,H ), [
subseteq( bros(F), id), % F is a (partial) function
subseteq( sibs(F,F), id), % F is one-one
equiv( dom(F), nodes(G) ),
equiv( img(F), nodes(H) ),
equiv( G, circ(circ(F,H),rev(F)) ) % F is a morphism
% Recall:
% bros(P) defAs rev(P) circ P
% sibs(P) defAs P circ rev(P)
]).
defThAs( graphIsom( G,F,H, GN,FN,HN ), [
nameLets([GN,G,HN,H,FN,F]),
% The above is equivalent to:
% defAs(@(GN),G), % association of first graph with its name
% defAs(@(HN),H), % association of second graph with its name
% defAs(@(FN),F), % association of isomorphism with its name
defAs( @(nodes,G), dom(un(G,rev(G)))), % not the same G as in the header
%? IF YOU WANT TO TRY THE OVERRIDING:
%?defAs( @(nodes,G), int(id,rA(un(G,rev(G))))), % not the same G as in the header
graphIsom( GN,FN,HN )
]).