; @origtpdbfilename ./TRS/Rubio/quick.trs
; @xtcfilename "./TRS_Standard/Rubio_04/quick.xml"
(format TRS)
(fun le 2)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun app 2)
(fun nil 0)
(fun cons 2)
(fun low 2)
(fun iflow 3)
(fun high 2)
(fun ifhigh 3)
(fun quicksort 1)
(rule (le |0| Y) true)
(rule (le (s X) |0|) false)
(rule (le (s X) (s Y)) (le X Y))
(rule (app nil Y) Y)
(rule (app (cons N L) Y) (cons N (app L Y)))
(rule (low N nil) nil)
(rule (low N (cons M L)) (iflow (le M N) N (cons M L)))
(rule (iflow true N (cons M L)) (cons M (low N L)))
(rule (iflow false N (cons M L)) (low N L))
(rule (high N nil) nil)
(rule (high N (cons M L)) (ifhigh (le M N) N (cons M L)))
(rule (ifhigh true N (cons M L)) (high N L))
(rule (ifhigh false N (cons M L)) (cons M (high N L)))
(rule (quicksort nil) nil)
(rule (quicksort (cons N L)) (app (quicksort (low N L)) (cons N (quicksort (high N L)))))