(COMMENT 

  Claude Marché

  Quick Sort. An automatic translation from the ML program :

  let append l1 l2 =
    match l1 with
    | Nil -> l2
    | Cons(x,l) -> Cons(append(l,l2))

  let part a l =
    match l with
    | Nil -> Pair(Nil,Nil)
    | Cons(x,l') ->
        match test(a,x) with
        | False -> Pair(Cons(x,l1),l2)
        | True -> Pair(l1,Cons(x,l2))

  let quick l =
    match l with
    | Nil -> Nil
    | Cons(a,l') -> 
        match part(a,l') with
        | Pair(l1,l2) -> append(quick(l1),Cons(a,quick(l2)))

)

(VAR l_5  a  x  l'  l  a_4  l_3  l2  l1  l2_1  l1_2  y  x_0)
(RULES

test(x_0,y) -> True 
test(x_0,y) -> False 
append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2) 
match_0(l1_2,l2_1,Nil) -> l2_1 
match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1)) 
part(a_4,l_3) -> match_1(a_4,l_3,l_3) 
match_1(a_4,l_3,Nil) -> Pair(Nil,Nil) 
match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l')) 
match_2(x,l',a_4,l_3,Pair(l1,l2)) -> 
match_3(l1,l2,x,l',a_4,l_3,test(a_4,x)) 
match_3(l1,l2,x,l',a_4,l_3,False) -> Pair(Cons(x,l1),l2) 
match_3(l1,l2,x,l',a_4,l_3,True) -> Pair(l1,Cons(x,l2)) 
quick(l_5) -> match_4(l_5,l_5) 
match_4(l_5,Nil) -> Nil 
match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l')) 
match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2))) 

)