/*


*/


use(to).


% 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)).



% def of permutations with the additional property that outside
% the interval [M,N] nothing is permuted
rperm(A0,A1,M,N) ==
	(perm(A0,A1) and 
	all(P,    (P<M => apply(A1,P)=apply(A0,P))
	      and (N<P => apply(A1,P)=apply(A0,P)))).	




% Thm: rperms compose (ternary version) if permutation intervals are
%      included into one another in the obvious way

goal ~(all(A,all(A2,all(A1,all(A0,all(M,all(N,all(I,all(J,
	M<I and J<I and J<N and
	rperm(A0,A1,M,N) and rperm(A1,A2,M,J) and rperm(A2,A,I,N) 
		=> rperm(A0,A,M,N)))))))))).