% function composition; id denotes the identity
comp(id,F)=F.
comp(F,id)=F.
comp(comp(F,G),H)=comp(F,comp(G,H)).

apply(id,P)=P.
apply(comp(F,G),P)=apply(F,apply(G,P)).

bijection(F)==exists(G,comp(F,G)=id and comp(G,F)=id).


% def of permutations
perm(A,B) == exists(F,bijection(F) and B = comp(A,F)).

top_predicates_precedence([perm,bijection]).