; @origtpdbfilename ./TRS/secret07/aprove/aprove03.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove03.xml"
(format TRS)
(fun average 2)
(fun if 3)
(fun ge 2)
(fun true 0)
(fun averIter 3)
(fun false 0)
(fun ifIter 4)
(fun plus 2)
(fun s 1)
(fun |0| 0)
(fun append 2)
(fun nil 0)
(fun cons 2)
(fun app 2)
(fun low 2)
(fun if_low 3)
(fun high 2)
(fun if_high 3)
(fun quicksort 1)
(fun ifquick 2)
(fun isempty 1)
(fun head 1)
(fun tail 1)
(fun error 0)
(fun a 0)
(fun b 0)
(fun c 0)
(rule (average x y) (if (ge x y) x y))
(rule (if true x y) (averIter y x y))
(rule (if false x y) (averIter x y x))
(rule (averIter x y z) (ifIter (ge x y) x y z))
(rule (ifIter true x y z) z)
(rule (ifIter false x y z) (averIter (plus x (s (s (s |0|)))) (plus y (s |0|)) (plus z (s |0|))))
(rule (append nil y) y)
(rule (append (cons n x) y) (cons n (app x y)))
(rule (low n nil) nil)
(rule (low n (cons m x)) (if_low (ge m n) n (cons m x)))
(rule (if_low false n (cons m x)) (cons m (low n x)))
(rule (if_low true n (cons m x)) (low n x))
(rule (high n nil) nil)
(rule (high n (cons m x)) (if_high (ge m n) n (cons m x)))
(rule (if_high false n (cons m x)) (high n x))
(rule (if_high true n (cons m x)) (cons (average m m) (high n x)))
(rule (quicksort x) (ifquick (isempty x) x))
(rule (ifquick true x) nil)
(rule (ifquick false x) (append (quicksort (low (head x) (tail x))) (cons (tail x) (quicksort (high (head x) (tail x))))))
(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))
(rule (isempty nil) true)
(rule (isempty (cons n x)) false)
(rule (head nil) error)
(rule (head (cons n x)) n)
(rule (tail nil) nil)
(rule (tail (cons n x)) x)
(rule (ge x |0|) true)
(rule (ge |0| (s y)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule a b)
(rule a c)