%
% a deterministic merge sort
%

rInt : sort.

mergeSort : trm (list rInt) -> trm (list rInt) -> atm.
msort : trm (list rInt) -> atm.
srt: trm (list rInt) -> atm.
merge : trm (list rInt) -> trm (list rInt) -> trm (list rInt) -> atm.
gt : trm rInt -> trm rInt -> atm.
lte : trm rInt -> trm rInt -> atm.

z : trm rInt.
s : trm rInt -> trm rInt. %prefix 10 s.


gt1 : prog( 
^ gt (s X) (s Y) 
     <= ^ gt X Y 
).

gt2 : prog( 
^ gt (s X) z 
).

lte1 : prog( 
^ lte (s X) (s Y) 
      <= ^ lte X Y 
).

lte2 : prog( 
^ lte z X 
).

merge1 : prog(
^ merge (H1 | T1) (H2 | T2) (H2 | T3)
	<= ^ gt H1 H2
	<= ^ merge (H1 | T1) T2 T3
).

merge2 : prog(
^ merge (H1 | T1) (H2 | T2) (H1 | T3)
	<= ^ lte H1 H2
	<= ^ merge T1 (H2 | T2) T3
).

merge3 : prog( 
^ merge L nil L 
).

merge4 : prog( 
^ merge nil L L 
).


msort1: prog(
^ mergeSort (H | T) L
        <<= (^ srt (H | nil) =>> ^ mergeSort T L)
). 

msort2 : prog(
^ mergeSort nil L 
	<<= ^ msort L
).

% replacing >=> by =>> in msort3 yields
% an insertion sort instead of a merge sort.

msort3 : prog(
^(msort L)
	<<= ^ srt L1
	<<= ^ srt L2 
	<=  ^ merge L1 L2 L12
	<=< (^ srt L12 >=> ^ msort L)
).


msort4 : prog(
 ^ msort L 
	<<= ^ srt L
).