consts sort :: 'a list => 'a list       
rules "sorted  (sort s)"
      "is_perm (sort s) s"
   
---V-------

consts sort :: 'a list => 'a list          
rules "sort x == @z. sorted z & is_perm z x"
   
---V-------

rules "sort x == if length x <= 1 
                 then @z. sorted z & is_perm z x
                 else @z. sorted z & is_perm z x"
   
---V-------  z= x  ==> is_perm z x

rules "sort x == if length x <= 1 then @z. sorted z & z= x
                 else @z. sorted z & is_perm z x"

---V------- [| P x; z= x|] ==> P z

rules "sort x == if length x <= 1 then @z. sorted x & z= x
                 else @z. sorted z & is_perm z x"	

---V------- length x<= 1 ==> sorted x= True    True & x = x    (@z. z=x)= x 

rules "sort x == if length x <= 1 then x
                 else @z. sorted z & is_perm z x"

We can now split up the list x in three ways: 

1. Into head and tail:

---V-------- length x> 1 ==> x= (head x):(tail x)

rules "sort x == if length x <= 1 then x	
		 else @z. sorted z & is_perm z ((head x):(tail x))"

---V------- Recomposition:
		c     == :
		P x y == sorted y & is_perm y x
		c'    == insert
		Q (x, xs) (z, zs) == (z= x)& (zs= sort xs)
		
rules "sort x == if length x <= 1 then x
	         else insert (@(z,zs). (z= head x) & (zs= sort (tail x)))"

     Prf.obl: (z= x)& (zs= sort xs) ==> sorted (insert (z, zs)) & 
					is_perm (insert(z, zs)) (x:xs)

	      i.e.  sorted zs ==> sorted (insert(z, zs))
                    is_perm (insert(x, sort xs)) (x:xs)

---V-------- (@z. z= x)= x

rules "sort x == if length x <= 1 then x
	         else insert (head x, sort (tail x))"

     Prf.obl: as was

#

2. Into two lists (of length less-equal 1) by some 

	split :: 'a list => 'a list* 'a list
	
	s.t. length x>1 ==> let (a1, a2)= split x
			    in  (length a1) < (length x)
	                      & (length a2) < (length x)  (*)
                 
---V--------- let (a1, a2)= split x in a1@a2= x

rules "sort x == if length x <= 1 then x
		 else let (a1, a2)= split x
                      in  @z. sorted z & is_perm z (a1@a2)"

---V------- Recomposition:
		c     == @
		P x y == sorted y & is_perm y x
		c'    == merge
		Q (x1, x2) (z1, z2) == (z1= sort x1) &(z2= sort x2)
		
rules "sort x == if length x <= 1 then x
	         else let (a1, a2)= split x
		      in merge (@(z1, z2). z1= sort a1 & z2= sort a2)"

     Prf.obl: (z1= sort x1)& (z2= sort x2) ==> sorted  (merge(z1, z2)) & 
					       is_perm (merge(z1, z2)) x1@x2

	      i.e.  sorted x1 & sorted x2 ==> sorted (merge(x1, x2))
                    is_perm (merge(sort x1, sort x2)) x1@x2

---V-------- (@z.z= x)= x

rules "sort x == if length x <= 1 then x
		 else let (a1, a2)= split x
		      in merge (sort a1, sort a2)"

(* Attention, termination and well-definedness only guaranteed by Theorem (1) *)

#

3. Combine the previous two:

---V--------- length x> 1==> let (a1, a2)= split'(head x, tail x)
	                     in  x= (head x):(a1@a2)

	      let (a1, a2)= split'(x, xs) 
              in  (! a. a in a1 --> a <= x) & 
		  (! a. a in a2 --> x < a)
                    
rules "sort x == if length x <= 1 then x
		 else let (a1, a2)= split'(head x, tail x)
                      in  @z. sorted z & is_perm z (head x):(a1@a2)"

---V------- Recomposition:
		c x x1 x2     == x:(x1@x2)
		P x y         == sorted y & is_perm y x
		c'(z, z1, z2) == z1@[z]@z2                =def= ins_in_mid
		Q (x, x1, x2) (z, z1, z2) == 
			(x= z) & (z1= sort x1) &(z2= sort x2)	
		
rules "sort x == if length x <= 1 then x
	         else let (a1, a2)= split'(head x, tail x)
		      in  ins_in_mid(@(z, z1, z2). 
				     z= head x & z1= sort a1 & z2= sort a2)"

    Prf. obl: see below

---V-------- (@z.z= x)= x

rules "sort x == if length x <= 1 then x
	         else let (a1, a2)= split'(head x, tail x)
		      in  (sort a1)@[head x]@(sort a2)"

     Prf.obl: (z= head x)& (z1= sort a1)& (z2= sort a2) 
	      ==> sorted (z1@[z]@z2)& 
		  is_perm (z1@[z]z2) (x:(a1@a2))

	      i.e.  sorted a1 & (! a. a in a1 --> a <= z) &
                    sorted a2 & (! a. a in a2 --> z < a)
                    ==> sorted (a1@[z]@a2) 
		    is_perm((sort a1)@[z]@(sort a2)) (z:(a1@a2))