; @origtpdbfilename ./TRS/higher-order/Lifantsev/Ex8Polymorphic.trs
; @xtcfilename "./TRS_Standard/Applicative_05/Ex8Polymorphic.xml"
(format TRS)
(fun app 2)
(fun twice 0)
(fun map 0)
(fun nil 0)
(fun cons 0)
(fun fmap 0)
(fun t_f 0)
(rule (app (app twice f) x) (app f (app f x)))
(rule (app (app map f) nil) nil)
(rule (app (app map f) (app (app cons h) t)) (app (app cons (app f h)) (app (app map f) t)))
(rule (app (app fmap nil) x) nil)
(rule (app (app fmap (app (app cons f) t_f)) x) (app (app cons (app f x)) (app (app fmap t_f) x)))