% Lemmas from Hoare: "Proof of a Program: FIND", CACM 14(1), 1971.
% See also Slagle: "Experiments with an Automatic Theorem Prover
%   Having Partial Ordering Inference Rules", CACM 16(11), 1973.

{1 <= f <= N}
begin
  integer m,n;
  m:=1; n:=N; (*1,2*)
  {m <= f & (forall p,q. 1 <= p < m <= q <= N -> A[p] <= A[q]) "m-inv" &
   f <= n & (forall p,q. 1 <= p <= n < q <= N -> A[p] <= A[q]) "n-inv"}
  while m<n do
    begin
      integer r,i,j,w;
      {"m-inv" & "n-inv" & m<n}
      r:=A[f]; i:=m; j:=n; (*4,5*)
      {"m-inv" & "n-inv" & 
       m<=i & (forall p. 1 <= p < i -> A[p] <= r) "i-inv" &
       j<=n & (forall q. j < q <= N -> r <= A[q]) "j-inv"}
      while i <= j do
        begin
          {"m-inv" & "n-inv" & "i-inv" & "j-inv" & i <= j}
          while A[i] < r do i:=i+1; (*8*)
          {"m-inv" & "n-inv" & "i-inv" & "j-inv"}
          while r < A[j] do j:=j-1; (*9*)
          {"m-inv" & "n-inv" & "i-inv" & "j-inv"}
          if i <= j then (*10,11,12,13*)
            begin
              w:=A[i]; A{i]:=A[j]; A[j]:=w;
              i:=i+1; j:=j-1;
            end
          {"m-inv" & "n-inv" & "i-inv" & "j-inv"}
        end
      {"m-inv" & "n-inv" & "i-inv" & "j-inv" & i > j}
      if f <= j then n:=j (*6*)
      else if i <= f then m:=i
      else goto L (*7*)
      {"m-inv" & "n-inv"}
    end
  {"m-inv" & "n-inv" & m>=n}
L:
end (*3*)
{forall p,q. 1 <= p <= f <= q <= N -> A[p] <= A[f] <= A[q] "found"}


Lemma 1:
1 <= f <= N ->
  (1 <= f & (forall p,q. 1 <= p < 1 <= q <= N -> A[p] <= A[q]) "m-inv"[1/m])

(1a)
1 <= f.
f <= nn.
1 <= f -> [].

(1b)
1 <= f.
f <= nn.
1 <= p.
p < 1.
1 <= q.
q <= nn.
a(p) <= a(q) -> [].

Lemma 2:
1 <= f <= N ->
  (f <= N & (forall p,q. 1 <= p <= N < q <= N -> A[p] <= A[q]) "n-inv"[N/n])

(2a)
1 <= f.
f <= nn.
f <= nn -> [].

(2b)
1 <= f.
f <= nn.
1 <= p.
p <= nn.
nn < q.
q <= nn.
a(p) <= a(q) -> [].

Lemma 3:
"m-inv" & "n-inv" & m>=n -> "found"

Lemma 4:
"m-inv" -> m<=m & (forall p. 1 <= p < m -> A[p] <= A[f]) "i-inv"[m/i,A[f]/r]

Lemma 5:
"n-inv" -> n<=n & (forall q. n < q <= N -> A[f] <= A[q]) "j-inv"[n/j,A[f]/r]

Lemma 6:
j < i & "i-inv" & "j-inv" ->
  if f <= j then 
    f <= j & (forall p,q. 1 <= p <= j < q <= N -> A[p] <= A[q]) "n-inv"[j/n]
  else if i <= f then
    i <= f & (forall p,q. 1 <= p < i <= q <= N -> A[p] <= A[q]) "m-inv"[i/m]

Lemma 7:
1 <= f <= N & j < f < i & "i-inv" & "j-inv" -> "found"

Lemma 8:
A[i] <= r & "i-inv"
  -> m<=i+1 & (forall p. 1 <= p < i+1 -> A[p] <= r) "i-inv"[i+1/i]

(8a)
a(i)<=r.
m<=i.
1<=P,P<i -> a(P)<=r.

m<=i+1 -> [].

Lemma 9:
r <= A[j] & "j-inv"
  -> j-1<=n & (forall q. j-1 < q <= N -> r <= A[q]) "j-inv"[j-1/j]

Lemma 10:
A'[i]=A[j] & A'[j]=A[i] & (forall s. s\=i & s\=j -> A'[s]=A[s])
  & i <= j & "i-inv" 
  -> m<=i & (forall p. 1 <= p < i -> A'[p] <= r) "i-inv"[A'/A]

Lemma 11:
A'[i]=A[j] & A'[j]=A[i] & (forall s. s\=i & s\=j -> A'[s]=A[s])
  & i <= j & "j-inv" 
  -> j<=n & (forall q. j < q <= N -> r <= A'[q]) "j-inv"[A'/A]

Lemma 12:
A'[i]=A[j] & A'[j]=A[i] & (forall s. s\=i & s\=j -> A'[s]=A[s])
  & m <= i <= j & "m-inv"
  -> (forall p,q. 1 <= p < m <= q <= N -> A'[p] <= A'[q]) "m-inv"[A'/A]

Lemma 13:
A'[i]=A[j] & A'[j]=A[i] & (forall s. s\=i & s\=j -> A'[s]=A[s])
  & i <= j <= n & "n-inv"
  -> (forall p,q. 1 <= p <= n < q <= N -> A'[p] <= A'[q]) "n-inv"[A'/A]

In clause form:

ap[i]=a[j].
ap[j]=a[i].
S=i,S=j,ap[S]=a[S].
i<=j.
j<=n.
1<=P,P<=n,n<Q,Q<=nn -> a[P]<=a[Q].

1<=p.
p<=n.
n<q.
q<=nn.
ap[p]<=ap[q] -> [].


Replace x<=y by not(y<x):

ap[i]=a[j].
ap[j]=a[i].
S=i,S=j,ap[S]=a[S].
j<i -> [].
n<j -> [].
n<Q, a[Q]<a[P] -> P<1,n<P,nn<Q.

p<1 -> [].
n<p -> [].
n<q.
nn<q -> [].
ap[q]<ap[p].


exists p. i <= p <= n & r <= A[p] "i-term-inv"

Lemma 14:
m <= f <= n -> exists p. m <= p <= n & A[f] <= A[p] "i-term-inv"[m/i,A[f]/r]

Lemma 15:
A[i] < r & "i-term-inv"
  -> exists p. i+1 <= p <= n & r <= A[p] "i-term-inv"[i+1/i]

Lemma 16:
A'[i]=A[j] & A'[j]=A[i] & (forall s. s\=i & s\=j -> A'[s]=A[s])
  & r <= A[i] & i+1 <= j-1 & j<=n
  -> exists p. i+1 <= p <= n & r <= A'[p] "i-term-inv"[i+1/i,A'/A]


exists p. m <= q <= j & A[q] <= r "j-term-inv"

Lemma 14':
m <= f <= n -> exists p. m <= q <= n & A[q] <= A[f] "j-term-inv"[n/j,A[f]/r]

Lemma 17:
r < A[j] & "j-term-inv"
  -> exists p. m <= q <= j-1 & A[q] <= r "j-term-inv"[j-1/j]

Lemma 18:
A'[i]=A[j] & A'[j]=A[i] & (forall s. s\=i & s\=j -> A'[s]=A[s])
  & r <= A[i] & i+1 <= j-1 & j<=n
  -> exists p. exists p. m <= q <= j-1 & A'[q] <= r "j-term-inv"[j-1/j,A'/A]