; @origtpdbfilename ./TRS/higher-order/AotoYam/016.trs
; @xtcfilename "./TRS_Standard/AotoYamada_05/016.xml"
(format TRS)
(fun app 2)
(fun neq 0)
(fun |0| 0)
(fun false 0)
(fun s 0)
(fun true 0)
(fun filter 0)
(fun nil 0)
(fun cons 0)
(fun filtersub 0)
(fun nonzero 0)
(rule (app (app neq |0|) |0|) false)
(rule (app (app neq |0|) (app s y)) true)
(rule (app (app neq (app s x)) |0|) true)
(rule (app (app neq (app s x)) (app s y)) (app (app neq x) y))
(rule (app (app filter f) nil) nil)
(rule (app (app filter f) (app (app cons y) ys)) (app (app (app filtersub (app f y)) f) (app (app cons y) ys)))
(rule (app (app (app filtersub true) f) (app (app cons y) ys)) (app (app cons y) (app (app filter f) ys)))
(rule (app (app (app filtersub false) f) (app (app cons y) ys)) (app (app filter f) ys))
(rule nonzero (app filter (app neq |0|)))