/* 
   In this example we prove a lemma which is useful for the
   verification of quick-sorting an array a.
   If 
	(i)   aa <= m <= bb, 
	(ii)  subarrays a[aa:m] and a[m:bb] are sorted, and 
	(iii) each element in a[aa:m] is less or equal to any element 
	      in a[m:bb], 
   then a[aa:bb] is sorted.
*/


predicates( [<] ).

% < is a total ordering 
X<Y, Y<Z -> X<Z.
X<X -> [].
X<Y, Y<X, X=Y.

% reflexive_closure

X=<X.
X<Y -> X=<Y.
X=<Y -> X=Y,X<Y.

% sorted(a[aa:m])
aa=<m.
aa=<I, I=<J, J=<m -> a(I)=<a(J).


% sorted(a[m:bb])
m=<bb.
m=<I, I=<J, J=<bb -> a(I)=<a(J).



% a[aa:m] =< a[m:bb]
aa=<I, I=<m, m=<J, J=<bb -> a(I)=<a(J).

% not sorted(aa,bb) i.e., 
% exists i,j: aa=<i and i<j and j=<bb and a(j)<a(i)
aa=<i.
i<j.
j=<bb.
a(j)<a(i).


precedence( [<,a,aa,m,bb,i,j] ).



/*

980720 mpii-hg


Proof:
======

   2 : A<A ->                                                           [input]
   4 : m<n ->                                                           [input]
   5 : f<m ->                                                           [input]
   6 : A<m,a(B)<a(A) -> A<1,B<m,nn<B                                    [input]
   7 : n<f ->                                                           [input]
   8 : n<A,a(A)<a(B) -> B<1,n<B,nn<A                                    [input]
   9 : p<1 ->                                                           [input]
  10 : f<p ->                                                           [input]
  11 : q<f ->                                                           [input]
  12 : nn<q ->                                                          [input]
  13 : a(f)<a(p),a(q)<a(f)                                              [input]
  14 : =$<(n,m)                                    [totality resolution from 4]
  15 : =$<(m,f)                                    [totality resolution from 5]
  17 : =$<(a(A),a(B)),=$<(m,A),A<1,B<m,nn<B        [totality resolution from 6]
  18 : =$<(f,n)                                    [totality resolution from 7]
  20 : =$<(a(A),a(B)),=$<(B,n),A<1,n<A,nn<B        [totality resolution from 8]
  21 : =$<(1,p)                                    [totality resolution from 9]
  22 : =$<(p,f)                                   [totality resolution from 10]
  23 : =$<(f,q)                                   [totality resolution from 11]
  24 : =$<(q,nn)                                  [totality resolution from 12]
  25 : =$<(n,f)                                        [chaining of 14 from 15]
  26 : n=f                                            [reduction of 25 by [18]]
  27 : =$<(A,f),B<1,=$<(a(B),a(A)),nn<A,f<B        [reduction of 20 by [26,26]]
  28 : f=m                                         [reduction of 14 by [26,15]]
  29 : =$<(f,A),A<1,=$<(a(A),a(B)),nn<B,B<f        [reduction of 17 by [28,28]]
  30 : =$<(1,f)                                        [chaining of 21 from 22]
  31 : =$<(f,nn)                                       [chaining of 23 from 24]
  37 : a(f)<a(A),a(q)<a(f),nn<A,=$<(A,f),p<1,f<p       [chaining of 13 from 27]
  38 : a(f)<a(A),a(q)<a(f),nn<A,=$<(A,f)           [reduction of 37 by [21,22]]
  40 : a(A)<a(f),nn<q,=$<(q,f),A<1,f<A,a(f)<a(B),nn<B,=$<(B,f) [chaining of 27 from 38]
  41 : a(A)<a(f),=$<(B,f),nn<B,a(f)<a(B),f<A,A<1,q=f [reduction of 40 by [24,23]]
  42 : p$1 -> =$<(A,f),nn<A,a(f)<a(A),q=f        [variable elimination from 41]
  43 : p$1,a(A)<a(f),f<A,A<1                     [variable elimination from 41]
  44 : p$1,f<1                                  [ordered resolution of 43 on 2]
  49 : p$1                                            [reduction of 44 by [30]]
  50 : q=f,=$<(A,f),nn<A,a(f)<a(A)                    [reduction of 42 by [49]]
  58 : a(f)<a(A),a(q)<a(f),=$<(f,p),p<1,nn<A,A<f       [chaining of 13 from 29]
  67 : f=p,a(f)<a(A),a(q)<a(f),A<f,nn<A            [reduction of 58 by [22,21]]
  96 : a(A)<a(f),=$<(f,A),A<1,nn<q,q<f,a(f)<a(B),p=f,B<f,nn<B [chaining of 29 from 67]
 104 : a(A)<a(f),=$<(f,A),A<1,nn<B,B<f,p=f,a(f)<a(B) [reduction of 96 by [24,23]]
 105 : p$2 -> nn<A,A<f,a(f)<a(A),p=f            [variable elimination from 104]
 106 : p$2,a(A)<a(f),=$<(f,A),A<1               [variable elimination from 104]
 107 : a(q)<a(f),p$2,=$<(f,p),p<1                     [chaining of 13 from 106]
 116 : f=p,a(q)<a(f),p$2                          [reduction of 107 by [22,21]]
 119 : nn<q,q=f,=$<(q,f),p$2,p=f                      [chaining of 50 from 116]
 123 : nn<q,=$<(q,f),p$2,p=f                              [condensement of 119]
 124 : p=f,p$2,q=f                                [reduction of 123 by [24,23]]
 126 : p$2,q=f,a(q)<a(f)                              [chaining of 124 from 13]
 128 : nn<q,q=f,=$<(q,f),p$2,q=f                      [chaining of 50 from 126]
 133 : =$<(q,f),nn<q,p$2                                  [condensement of 128]
 134 : q=f,p$2                                    [reduction of 133 by [23,24]]
 139 : p$2,a(f)<a(A),p=f,A<f,nn<A                     [chaining of 134 from 67]
 141 : nn<A,A<f,p=f,a(f)<a(A)                       [reduction of 139 by [105]]
 152 : nn<f,p=f                                [ordered resolution of 141 on 2]
 158 : p=f                                           [reduction of 152 by [31]]
 160 : a(q)<a(f)                                   [reduction of 13 by [158,2]]
 162 : nn<q,q=f,=$<(q,f)                              [chaining of 50 from 160]
 166 : nn<q,=$<(q,f)                                      [condensement of 162]
 167 : q=f                                        [reduction of 166 by [24,23]]
 169 : false                                      [reduction of 160 by [167,2]]


Length = 60, Depth = 29



Total time: 2720 milliseconds

Number of forward inferences: 95
Number of tableau inferences: 0
Number of kept clauses: 50

*/