(VAR f g x y ) (RULES app(app(plus,0),y) -> y app(app(plus,app(s,x)),y) -> app(s,app(app(plus,x),y)) app(app(times,0),y) -> 0 app(app(times,app(s,x)),y) -> app(app(plus,app(app(times,x),y)),y) app(app(app(comp,f),g),x) -> app(f,app(g,x)) app(twice,f) -> app(app(comp,f),f) )