% We prove (in files qsort2iia1 and qsort2iia1) that
%
% 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)])



% In this part we prove 
% m<i & j<i & j<n &
% rperm(A0,A1,m,n) & rperm(A1,A2,m,j) & rperm(A2,A,i,n)
%   -> perm(A0,A)

% For this we only need the fact that rperm's are perm's.
% Actually, the technical problem is that if we include all properties
% of perm, we get lost in uninteresting parts of the search space.



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


% ordering
reflexive_closure(<,=<).
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

% perm(A0,A1)
comp(f0,g0)=comp(g0,f0).
comp(g0,f0)=id.
a1(P)=a0(apply(f0,P)).

% perm(A1,A2)
comp(f1,g1)=comp(g1,f1).
comp(g1,f1)=id.
a2(I)=a1(apply(f1,I)).

% perm(A2,A)
comp(f2,g2)=comp(g2,f2).
comp(g2,f2)=id.
a(I)=a2(apply(f2,I)).


% Conclusion

% (a)    not perm(a0,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))

  apply(G,apply(F,p1(F,G)))=p1(F,G),
     apply(F,apply(G,p1(F,G)))=p1(F,G),
     a(p1(F,G))=a0(apply(F,p1(F,G))) -> [].




/* saturate settings */

:-sama([1]).

first_predicate_precedence([<]).
precedence( [a0,a1,a2,a,f0,g0,f1,g1,f2,g2,p1,apply,comp,id,p,q] ).