; @origtpdbfilename ./AProVE_09_Inductive/qsort.trs
; @xtcfilename "./TRS_Standard/AProVE_09_Inductive/qsort.xml"
(format TRS)
(fun qsort 1)
(fun nil 0)
(fun cons 2)
(fun append 2)
(fun filterlow 2)
(fun filterhigh 2)
(fun if1 4)
(fun ge 2)
(fun true 0)
(fun false 0)
(fun if2 4)
(fun |0| 0)
(fun s 1)
(fun ys 0)
(rule (qsort nil) nil)
(rule (qsort (cons x xs)) (append (qsort (filterlow x (cons x xs))) (cons x (qsort (filterhigh x (cons x xs))))))
(rule (filterlow n nil) nil)
(rule (filterlow n (cons x xs)) (if1 (ge n x) n x xs))
(rule (if1 true n x xs) (filterlow n xs))
(rule (if1 false n x xs) (cons x (filterlow n xs)))
(rule (filterhigh n nil) nil)
(rule (filterhigh n (cons x xs)) (if2 (ge x n) n x xs))
(rule (if2 true n x xs) (filterhigh n xs))
(rule (if2 false n x xs) (cons x (filterhigh n xs)))
(rule (ge x |0|) true)
(rule (ge |0| (s x)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule (append nil ys) ys)
(rule (append (cons x xs) ys) (cons x (append xs ys)))