MAYBE

Problem:
 app(app(app(rec(),f),x),0()) -> x
 app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y))

Proof:
 DP Processor:
  DPs:
   app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y)
   app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y))
   app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y))
  TRS:
   app(app(app(rec(),f),x),0()) -> x
   app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y))
  Open