MAYBE

Problem:
 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())

Proof:
 Uncurry Processor:
  rec4(t,u,v,0()) -> t
  rec4(t,u,v,s1(x)) -> app(app(u,x),rec4(t,u,v,x))
  rec4(t,u,v,lim1(f)) -> app(app(v,f),rectuv4(t,u,v,app(f,n())))
  rectuv4(t,u,v,n()) -> rec4(t,u,v,n())
  app(rec3(x7,x6,x5),x8) -> rec4(x7,x6,x5,x8)
  app(rec2(x7,x6),x8) -> rec3(x7,x6,x8)
  app(rec1(x7),x8) -> rec2(x7,x8)
  app(rec(),x8) -> rec1(x8)
  app(s(),x8) -> s1(x8)
  app(lim(),x8) -> lim1(x8)
  app(rectuv3(x7,x6,x5),x8) -> rectuv4(x7,x6,x5,x8)
  app(rectuv2(x7,x6),x8) -> rectuv3(x7,x6,x8)
  app(rectuv1(x7),x8) -> rectuv2(x7,x8)
  app(rectuv(),x8) -> rectuv1(x8)
  DP Processor:
   DPs:
    rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
    rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
    rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
    rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
    rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
    rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
    rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
    rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
    app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
    app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
   TRS:
    rec4(t,u,v,0()) -> t
    rec4(t,u,v,s1(x)) -> app(app(u,x),rec4(t,u,v,x))
    rec4(t,u,v,lim1(f)) -> app(app(v,f),rectuv4(t,u,v,app(f,n())))
    rectuv4(t,u,v,n()) -> rec4(t,u,v,n())
    app(rec3(x7,x6,x5),x8) -> rec4(x7,x6,x5,x8)
    app(rec2(x7,x6),x8) -> rec3(x7,x6,x8)
    app(rec1(x7),x8) -> rec2(x7,x8)
    app(rec(),x8) -> rec1(x8)
    app(s(),x8) -> s1(x8)
    app(lim(),x8) -> lim1(x8)
    app(rectuv3(x7,x6,x5),x8) -> rectuv4(x7,x6,x5,x8)
    app(rectuv2(x7,x6),x8) -> rectuv3(x7,x6,x8)
    app(rectuv1(x7),x8) -> rectuv2(x7,x8)
    app(rectuv(),x8) -> rectuv1(x8)
   TDG Processor:
    DPs:
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
     rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
     rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
     rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
     rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
     rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
     rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
     app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
    TRS:
     rec4(t,u,v,0()) -> t
     rec4(t,u,v,s1(x)) -> app(app(u,x),rec4(t,u,v,x))
     rec4(t,u,v,lim1(f)) -> app(app(v,f),rectuv4(t,u,v,app(f,n())))
     rectuv4(t,u,v,n()) -> rec4(t,u,v,n())
     app(rec3(x7,x6,x5),x8) -> rec4(x7,x6,x5,x8)
     app(rec2(x7,x6),x8) -> rec3(x7,x6,x8)
     app(rec1(x7),x8) -> rec2(x7,x8)
     app(rec(),x8) -> rec1(x8)
     app(s(),x8) -> s1(x8)
     app(lim(),x8) -> lim1(x8)
     app(rectuv3(x7,x6,x5),x8) -> rectuv4(x7,x6,x5,x8)
     app(rectuv2(x7,x6),x8) -> rectuv3(x7,x6,x8)
     app(rectuv1(x7),x8) -> rectuv2(x7,x8)
     app(rectuv(),x8) -> rectuv1(x8)
    graph:
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n()) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n()) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n()) ->
     rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n()) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n()) ->
     rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n()) ->
     rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n()) ->
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
     app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8) ->
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
     rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
     rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
     rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
     rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n())) ->
     rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
     rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n()))) ->
     app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n()))) ->
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,lim1(f)) -> app#(v,f) ->
     app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,lim1(f)) -> app#(v,f) ->
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,lim1(f)) -> app#(f,n()) ->
     app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,lim1(f)) -> app#(f,n()) ->
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x)) ->
     app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x)) ->
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,s1(x)) -> app#(u,x) ->
     app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,s1(x)) -> app#(u,x) ->
     app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
     rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
     rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
     rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
     rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
     rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) -> rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
    EDG Processor:
     DPs:
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
      rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
      rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
      rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
      rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
      rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
      rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
      rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
      app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
     TRS:
      rec4(t,u,v,0()) -> t
      rec4(t,u,v,s1(x)) -> app(app(u,x),rec4(t,u,v,x))
      rec4(t,u,v,lim1(f)) -> app(app(v,f),rectuv4(t,u,v,app(f,n())))
      rectuv4(t,u,v,n()) -> rec4(t,u,v,n())
      app(rec3(x7,x6,x5),x8) -> rec4(x7,x6,x5,x8)
      app(rec2(x7,x6),x8) -> rec3(x7,x6,x8)
      app(rec1(x7),x8) -> rec2(x7,x8)
      app(rec(),x8) -> rec1(x8)
      app(s(),x8) -> s1(x8)
      app(lim(),x8) -> lim1(x8)
      app(rectuv3(x7,x6,x5),x8) -> rectuv4(x7,x6,x5,x8)
      app(rectuv2(x7,x6),x8) -> rectuv3(x7,x6,x8)
      app(rectuv1(x7),x8) -> rectuv2(x7,x8)
      app(rectuv(),x8) -> rectuv1(x8)
     graph:
      app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8) ->
      rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
      rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
      rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
      rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
      rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
      rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
      rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
      rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n())) ->
      rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
      rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n()))) ->
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n()))) ->
      app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,lim1(f)) -> app#(v,f) ->
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,lim1(f)) -> app#(v,f) ->
      app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,lim1(f)) -> app#(f,n()) ->
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,lim1(f)) -> app#(f,n()) ->
      app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x)) ->
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x)) ->
      app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,s1(x)) -> app#(u,x) ->
      app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,s1(x)) -> app#(u,x) ->
      app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
      rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
      rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
      rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
      rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
      rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
      rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
      rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
     CDG Processor:
      DPs:
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
       rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
       rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
       rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
       rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
       rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
       rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
       rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
       app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
      TRS:
       rec4(t,u,v,0()) -> t
       rec4(t,u,v,s1(x)) -> app(app(u,x),rec4(t,u,v,x))
       rec4(t,u,v,lim1(f)) -> app(app(v,f),rectuv4(t,u,v,app(f,n())))
       rectuv4(t,u,v,n()) -> rec4(t,u,v,n())
       app(rec3(x7,x6,x5),x8) -> rec4(x7,x6,x5,x8)
       app(rec2(x7,x6),x8) -> rec3(x7,x6,x8)
       app(rec1(x7),x8) -> rec2(x7,x8)
       app(rec(),x8) -> rec1(x8)
       app(s(),x8) -> s1(x8)
       app(lim(),x8) -> lim1(x8)
       app(rectuv3(x7,x6,x5),x8) -> rectuv4(x7,x6,x5,x8)
       app(rectuv2(x7,x6),x8) -> rectuv3(x7,x6,x8)
       app(rectuv1(x7),x8) -> rectuv2(x7,x8)
       app(rectuv(),x8) -> rectuv1(x8)
      graph:
       app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8) ->
       rectuv{4,#}(t,u,v,n()) -> rec{4,#}(t,u,v,n())
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
       rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
       rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
       rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
       rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
       rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
       rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8) ->
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
       rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n()))) ->
       app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n()))) ->
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,lim1(f)) -> app#(v,f) ->
       app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,lim1(f)) -> app#(v,f) ->
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,lim1(f)) -> app#(f,n()) ->
       app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,lim1(f)) -> app#(f,n()) ->
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x)) ->
       app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x)) ->
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,s1(x)) -> app#(u,x) ->
       app#(rectuv3(x7,x6,x5),x8) -> rectuv{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,s1(x)) -> app#(u,x) ->
       app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
       rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
       rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
       rec{4,#}(t,u,v,lim1(f)) -> rectuv{4,#}(t,u,v,app(f,n()))
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
       rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
       rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) ->
       rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
       rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x) -> rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
      SCC Processor:
       #sccs: 1
       #rules: 7
       #arcs: 25/100
       DPs:
        app#(rec3(x7,x6,x5),x8) -> rec{4,#}(x7,x6,x5,x8)
        rec{4,#}(t,u,v,s1(x)) -> rec{4,#}(t,u,v,x)
        rec{4,#}(t,u,v,s1(x)) -> app#(u,x)
        rec{4,#}(t,u,v,s1(x)) -> app#(app(u,x),rec4(t,u,v,x))
        rec{4,#}(t,u,v,lim1(f)) -> app#(f,n())
        rec{4,#}(t,u,v,lim1(f)) -> app#(v,f)
        rec{4,#}(t,u,v,lim1(f)) -> app#(app(v,f),rectuv4(t,u,v,app(f,n())))
       TRS:
        rec4(t,u,v,0()) -> t
        rec4(t,u,v,s1(x)) -> app(app(u,x),rec4(t,u,v,x))
        rec4(t,u,v,lim1(f)) -> app(app(v,f),rectuv4(t,u,v,app(f,n())))
        rectuv4(t,u,v,n()) -> rec4(t,u,v,n())
        app(rec3(x7,x6,x5),x8) -> rec4(x7,x6,x5,x8)
        app(rec2(x7,x6),x8) -> rec3(x7,x6,x8)
        app(rec1(x7),x8) -> rec2(x7,x8)
        app(rec(),x8) -> rec1(x8)
        app(s(),x8) -> s1(x8)
        app(lim(),x8) -> lim1(x8)
        app(rectuv3(x7,x6,x5),x8) -> rectuv4(x7,x6,x5,x8)
        app(rectuv2(x7,x6),x8) -> rectuv3(x7,x6,x8)
        app(rectuv1(x7),x8) -> rectuv2(x7,x8)
        app(rectuv(),x8) -> rectuv1(x8)
       Open