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:
 Uncurry Processor:
  rec3(f,x,0()) -> x
  rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
  app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
  app(rec1(x4),x5) -> rec2(x4,x5)
  app(rec(),x5) -> rec1(x5)
  app(s(),x5) -> s1(x5)
  DP Processor:
   DPs:
    rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
    rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
    rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
    app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
   TRS:
    rec3(f,x,0()) -> x
    rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
    app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
    app(rec1(x4),x5) -> rec2(x4,x5)
    app(rec(),x5) -> rec1(x5)
    app(s(),x5) -> s1(x5)
   TDG Processor:
    DPs:
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
    TRS:
     rec3(f,x,0()) -> x
     rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
     app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
     app(rec1(x4),x5) -> rec2(x4,x5)
     app(rec(),x5) -> rec1(x5)
     app(s(),x5) -> s1(x5)
    graph:
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5) ->
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5) ->
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5) ->
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y)) ->
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y)) ->
     app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y) ->
     rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y) ->
     rec{3,#}(f,x,s1(y)) -> app#(f,s1(y))
     rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y) -> rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [app#](x0, x1) = 2x0 + 1x1 + 4,
      
      [rec{3,#}](x0, x1, x2) = 3x0 + 2x1 + 5,
      
      [s1](x0) = 2,
      
      [rec1](x0) = x0 + 2,
      
      [rec3](x0, x1, x2) = 2x0 + x1 + 4,
      
      [rec2](x0, x1) = 1x0 + x1 + 3,
      
      [s] = 2,
      
      [0] = 3,
      
      [app](x0, x1) = 1x0 + x1 + 0,
      
      [rec] = 3
     orientation:
      rec{3,#}(f,x,s1(y)) = 3f + 2x + 5 >= 3f + 2x + 5 = rec{3,#}(f,x,y)
      
      rec{3,#}(f,x,s1(y)) = 3f + 2x + 5 >= 2f + 4 = app#(f,s1(y))
      
      rec{3,#}(f,x,s1(y)) = 3f + 2x + 5 >= 3f + 1x + 5 = app#(app(f,s1(y)),rec3(f,x,y))
      
      app#(rec2(x4,x3),x5) = 2x3 + 3x4 + 1x5 + 5 >= 2x3 + 3x4 + 5 = rec{3,#}(x4,x3,x5)
      
      rec3(f,x,0()) = 2f + x + 4 >= x = x
      
      rec3(f,x,s1(y)) = 2f + x + 4 >= 2f + x + 4 = app(app(f,s1(y)),rec3(f,x,y))
      
      app(rec2(x4,x3),x5) = 1x3 + 2x4 + x5 + 4 >= x3 + 2x4 + 4 = rec3(x4,x3,x5)
      
      app(rec1(x4),x5) = 1x4 + x5 + 3 >= 1x4 + x5 + 3 = rec2(x4,x5)
      
      app(rec(),x5) = x5 + 4 >= x5 + 2 = rec1(x5)
      
      app(s(),x5) = x5 + 3 >= 2 = s1(x5)
     problem:
      DPs:
       rec{3,#}(f,x,s1(y)) -> rec{3,#}(f,x,y)
       rec{3,#}(f,x,s1(y)) -> app#(app(f,s1(y)),rec3(f,x,y))
       app#(rec2(x4,x3),x5) -> rec{3,#}(x4,x3,x5)
      TRS:
       rec3(f,x,0()) -> x
       rec3(f,x,s1(y)) -> app(app(f,s1(y)),rec3(f,x,y))
       app(rec2(x4,x3),x5) -> rec3(x4,x3,x5)
       app(rec1(x4),x5) -> rec2(x4,x5)
       app(rec(),x5) -> rec1(x5)
       app(s(),x5) -> s1(x5)
     Open