; @origtpdbfilename ./TRS/higher-order/AotoYam/020.trs
; @xtcfilename "./TRS_Standard/AotoYamada_05/020.xml"
(format TRS)
(fun app 2)
(fun plus 0)
(fun |0| 0)
(fun s 0)
(fun times 0)
(fun comp 0)
(fun twice 0)
(rule (app (app plus |0|) y) y)
(rule (app (app plus (app s x)) y) (app s (app (app plus x) y)))
(rule (app (app times |0|) y) |0|)
(rule (app (app times (app s x)) y) (app (app plus (app (app times x) y)) y))
(rule (app (app (app comp f) g) x) (app f (app g x)))
(rule (app twice f) (app (app comp f) f))