; @origtpdbfilename ./TRS/Thiemann/quicksort.trs
; @xtcfilename "./TRS_Standard/AProVE_06/quicksort.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 add 2)
(fun low 2)
(fun if_low 3)
(fun high 2)
(fun if_high 3)
(fun head 1)
(fun tail 1)
(fun isempty 1)
(fun quicksort 1)
(fun if_qs 4)
(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 (head (add n x)) n)
(rule (tail (add n x)) x)
(rule (isempty nil) true)
(rule (isempty (add n x)) false)
(rule (quicksort x) (if_qs (isempty x) (low (head x) (tail x)) (head x) (high (head x) (tail x))))
(rule (if_qs true x n y) nil)
(rule (if_qs false x n y) (app (quicksort x) (add n (quicksort y))))