; @origtpdbfilename ./TRS/higher-order/Kusakari/Ex7_9.trs
; @xtcfilename "./TRS_Standard/Applicative_05/Ex7_9.xml"
(format TRS)
(fun app 2)
(fun if 0)
(fun true 0)
(fun false 0)
(fun sub 0)
(fun |0| 0)
(fun s 0)
(fun gtr 0)
(fun d 0)
(fun len 0)
(fun nil 0)
(fun cons 0)
(fun filter 0)
(rule (app (app (app if true) xs) ys) xs)
(rule (app (app (app if false) xs) ys) ys)
(rule (app (app sub x) |0|) x)
(rule (app (app sub (app s x)) (app s y)) (app (app sub x) y))
(rule (app (app gtr |0|) y) false)
(rule (app (app gtr (app s x)) |0|) true)
(rule (app (app gtr (app s x)) (app s y)) (app (app gtr x) y))
(rule (app (app d x) |0|) true)
(rule (app (app d (app s x)) (app s y)) (app (app (app if (app (app gtr x) y)) false) (app (app d (app s x)) (app (app sub y) x))))
(rule (app len nil) |0|)
(rule (app len (app (app cons x) xs)) (app s (app len xs)))
(rule (app (app filter p) nil) nil)
(rule (app (app filter p) (app (app cons x) xs)) (app (app (app if (app p x)) (app (app cons x) (app (app filter p) xs))) (app (app filter p) xs)))