; @xtcfilename "./TRS_Relative/INVY_15/#3.55_rand.xml"
(format TRS)
(fun low 2)
(fun true 0)
(fun app 2)
(fun add 2)
(fun quicksort 1)
(fun if_high 3)
(fun rand 1)
(fun quot 2)
(fun false 0)
(fun nil 0)
(fun s 1)
(fun if_low 3)
(fun |0| 0)
(fun le 2)
(fun minus 2)
(fun high 2)
(rule (minus x |0|) x)
(rule (minus (s x) (s y)) (minus x y))
(rule (quot |0| (s y)) |0|)
(rule (quot (s x) (s y)) (s (quot (minus x y) (s y))))
(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 (add n x) y) (add n (app x y)))
(rule (low n nil) nil)
(rule (low n (add m x)) (if_low (le m n) n (add m x)))
(rule (if_low true n (add m x)) (add m (low n x)))
(rule (if_low false n (add m x)) (low n x))
(rule (high n nil) nil)
(rule (high n (add m x)) (if_high (le m n) n (add m x)))
(rule (if_high true n (add m x)) (high n x))
(rule (if_high false n (add m x)) (add m (high n x)))
(rule (quicksort nil) nil)
(rule (quicksort (add n x)) (app (quicksort (low n x)) (add n (quicksort (high n x)))))
(rule (rand x) x :cost 0)
(rule (rand x) (rand (s x)) :cost 0)