(VAR f t u v x )
(RULES 
        app(app(app(app(rec,t),u),v),0) -> t
        app(app(app(app(rec,t),u),v),app(s,x)) -> app(app(u,x),app(app(app(app(rec,t),u),v),x))
        app(app(app(app(rec,t),u),v),app(lim,f)) -> app(app(v,f),app(app(app(app(rectuv,t),u),v),app(f,n)))
        app(app(app(app(rectuv,t),u),v),n) -> app(app(app(app(rec,t),u),v),n)
        
)