% We prove:
%
% m<i & j<i & j<n &
% rperm(A0,A1,m,n) & rperm(A1,A2,m,j) & rperm(A2,A,i,n)
%   -> rperm(A0,A,m,n)
%
%
% Definitions:
%
% rperm(A,B,m,n) <-> perm(A,B) & (forall p. p<m -> A[p]=B[p])
%                              & (forall q. n<q -> A[q]=B[q])
%
% We model permutations as functions which have an inverse:
%
% perm(A,B) <-> exists f,g. (forall p. f(g(p))=p & g(f(p))=p & A[p]=B[f(p)])


% This proves the 2nd half of the theorem (cf. below).


predicates( [<,nota,notb,notc] ).


% ordering
:-option(special_relations(off)).	% to exercise resolution in the 
					% presence of transitivity

X<Y, Y<Z -> X<Z.
X<X -> [].
X<Y, Y<X, X=Y.

% apply and comp
comp(id,F)=F.
comp(F,id)=F.
comp(F,comp(G,H))=comp(comp(F,G),H).

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

% Hypotheses

m<i.
j<i.
j<n.

% rperm(A0,A1,m,n)
comp(f0,g0)=comp(g0,f0).
comp(g0,f0)=id.
a1(P)=a0(apply(f0,P)).
P<m -> a0(P)=a1(P).
n<Q -> a0(Q)=a1(Q).

% rperm(A1,A2,m,j)
comp(f1,g1)=comp(g1,f1).
comp(g1,f1)=id.
a2(I)=a1(apply(f1,I)).
P<m -> a1(P)=a2(P).
j<Q -> a1(Q)=a2(Q).

% rperm(A2,A,i,n)
comp(f2,g2)=comp(g2,f2).
comp(g2,f2)=id.
a(I)=a2(apply(f2,I)).
P<i -> a2(P)=a(P).
n<Q -> a2(Q)=a(Q).


% Conclusion

% not rperm(a0,a,m,n)
% <->
% not (perm(a0,a) & (forall p. p<m -> a0[p]=a[p])
%                 & (forall q. n<q -> a0[q]=a[q])
% <->
% (a)    not perm(a0,a)
% (b) or not forall p. p<m -> a0[p]=a[p]
% (c) or not forall q. n<q -> a0[q]=a[q]
%
% (a)
% <-> not exists F,G. forall P.   apply(F,apply(G,P))=P
%                               & apply(G,apply(F,P))=P
%                               & a(P)=a0(apply(F,P))
% <-> forall F,G.
%       exists P. 
%            not apply(F,apply(G,P))=P
%         or not apply(G,apply(F,P))=P
%         or not a(P)=a0(apply(F,P))
%
% (b)
% <-> exists p. not (p<m -> a0[p]=a[p])
% <-> exists p. p<m & not(a0[p]=a[p])
%
% (c)
% <-> not forall q. n<q -> a0[q]=a[q]
% <-> exists q. n<q & not(a0[q]=a[q])


% here we prove b and c



notb -> p<m.
notb,a0(p)=a(p) -> [].

notc -> n<q.
notc,a0(q)=a(q) -> [].

notb,notc.




/* saturate settings */

:-sama([1]).


first_predicate_precedence([<]).
precedence( [a0,a1,a2,a,f0,g0,f1,g1,f2,g2,p1,apply,comp,id,
	     p,q,i,j,m,n,nota,notb,notc] ).