MAYBE

Problem:
 ap(ap(f(),x),x) -> ap(ap(x,ap(f(),x)),ap(ap(cons(),x),nil()))
 ap(ap(ap(foldr(),g),h),nil()) -> h
 ap(ap(ap(foldr(),g),h),ap(ap(cons(),x),xs)) -> ap(ap(g,x),ap(ap(ap(foldr(),g),h),xs))

Proof:
 Uncurry Processor:
  f2(x,x) -> ap(ap(x,f1(x)),cons2(x,nil()))
  foldr3(g,h,nil()) -> h
  foldr3(g,h,cons2(x,xs)) -> ap(ap(g,x),foldr3(g,h,xs))
  ap(f1(x5),x6) -> f2(x5,x6)
  ap(f(),x6) -> f1(x6)
  ap(cons1(x5),x6) -> cons2(x5,x6)
  ap(cons(),x6) -> cons1(x6)
  ap(foldr2(x5,x4),x6) -> foldr3(x5,x4,x6)
  ap(foldr1(x5),x6) -> foldr2(x5,x6)
  ap(foldr(),x6) -> foldr1(x6)
  DP Processor:
   DPs:
    f{2,#}(x,x) -> ap#(x,f1(x))
    f{2,#}(x,x) -> ap#(ap(x,f1(x)),cons2(x,nil()))
    foldr{3,#}(g,h,cons2(x,xs)) -> foldr{3,#}(g,h,xs)
    foldr{3,#}(g,h,cons2(x,xs)) -> ap#(g,x)
    foldr{3,#}(g,h,cons2(x,xs)) -> ap#(ap(g,x),foldr3(g,h,xs))
    ap#(f1(x5),x6) -> f{2,#}(x5,x6)
    ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6)
   TRS:
    f2(x,x) -> ap(ap(x,f1(x)),cons2(x,nil()))
    foldr3(g,h,nil()) -> h
    foldr3(g,h,cons2(x,xs)) -> ap(ap(g,x),foldr3(g,h,xs))
    ap(f1(x5),x6) -> f2(x5,x6)
    ap(f(),x6) -> f1(x6)
    ap(cons1(x5),x6) -> cons2(x5,x6)
    ap(cons(),x6) -> cons1(x6)
    ap(foldr2(x5,x4),x6) -> foldr3(x5,x4,x6)
    ap(foldr1(x5),x6) -> foldr2(x5,x6)
    ap(foldr(),x6) -> foldr1(x6)
   TDG Processor:
    DPs:
     f{2,#}(x,x) -> ap#(x,f1(x))
     f{2,#}(x,x) -> ap#(ap(x,f1(x)),cons2(x,nil()))
     foldr{3,#}(g,h,cons2(x,xs)) -> foldr{3,#}(g,h,xs)
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(g,x)
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(ap(g,x),foldr3(g,h,xs))
     ap#(f1(x5),x6) -> f{2,#}(x5,x6)
     ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6)
    TRS:
     f2(x,x) -> ap(ap(x,f1(x)),cons2(x,nil()))
     foldr3(g,h,nil()) -> h
     foldr3(g,h,cons2(x,xs)) -> ap(ap(g,x),foldr3(g,h,xs))
     ap(f1(x5),x6) -> f2(x5,x6)
     ap(f(),x6) -> f1(x6)
     ap(cons1(x5),x6) -> cons2(x5,x6)
     ap(cons(),x6) -> cons1(x6)
     ap(foldr2(x5,x4),x6) -> foldr3(x5,x4,x6)
     ap(foldr1(x5),x6) -> foldr2(x5,x6)
     ap(foldr(),x6) -> foldr1(x6)
    graph:
     foldr{3,#}(g,h,cons2(x,xs)) -> foldr{3,#}(g,h,xs) ->
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(ap(g,x),foldr3(g,h,xs))
     foldr{3,#}(g,h,cons2(x,xs)) -> foldr{3,#}(g,h,xs) ->
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(g,x)
     foldr{3,#}(g,h,cons2(x,xs)) -> foldr{3,#}(g,h,xs) ->
     foldr{3,#}(g,h,cons2(x,xs)) -> foldr{3,#}(g,h,xs)
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(ap(g,x),foldr3(g,h,xs)) ->
     ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6)
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(ap(g,x),foldr3(g,h,xs)) ->
     ap#(f1(x5),x6) -> f{2,#}(x5,x6)
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(g,x) ->
     ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6)
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(g,x) ->
     ap#(f1(x5),x6) -> f{2,#}(x5,x6)
     ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6) ->
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(ap(g,x),foldr3(g,h,xs))
     ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6) ->
     foldr{3,#}(g,h,cons2(x,xs)) -> ap#(g,x)
     ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6) ->
     foldr{3,#}(g,h,cons2(x,xs)) -> foldr{3,#}(g,h,xs)
     ap#(f1(x5),x6) -> f{2,#}(x5,x6) ->
     f{2,#}(x,x) -> ap#(ap(x,f1(x)),cons2(x,nil()))
     ap#(f1(x5),x6) -> f{2,#}(x5,x6) ->
     f{2,#}(x,x) -> ap#(x,f1(x))
     f{2,#}(x,x) -> ap#(ap(x,f1(x)),cons2(x,nil())) ->
     ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6)
     f{2,#}(x,x) -> ap#(ap(x,f1(x)),cons2(x,nil())) ->
     ap#(f1(x5),x6) -> f{2,#}(x5,x6)
     f{2,#}(x,x) -> ap#(x,f1(x)) ->
     ap#(foldr2(x5,x4),x6) -> foldr{3,#}(x5,x4,x6)
     f{2,#}(x,x) -> ap#(x,f1(x)) -> ap#(f1(x5),x6) -> f{2,#}(x5,x6)
    Open