; @origtpdbfilename ./AProVE_09_Inductive/qsortmiddle.trs
; @xtcfilename "./TRS_Standard/AProVE_09_Inductive/qsortmiddle.xml"
(format TRS)
(fun qsort 1)
(fun qs 2)
(fun half 1)
(fun length 1)
(fun nil 0)
(fun cons 2)
(fun append 2)
(fun filterlow 2)
(fun get 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 xs) (qs (half (length xs)) xs))
(rule (qs n nil) nil)
(rule (qs n (cons x xs)) (append (qs (half n) (filterlow (get n (cons x xs)) (cons x xs))) (cons (get n (cons x xs)) (qs (half n) (filterhigh (get n (cons x xs)) (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)))
(rule (length nil) |0|)
(rule (length (cons x xs)) (s (length xs)))
(rule (half |0|) |0|)
(rule (half (s |0|)) |0|)
(rule (half (s (s x))) (s (half x)))
(rule (get n nil) |0|)
(rule (get n (cons x nil)) x)
(rule (get |0| (cons x (cons y xs))) x)
(rule (get (s n) (cons x (cons y xs))) (get n (cons y xs)))