MAYBE

Problem:
 app(app(map_1(),f),app(app(cons(),h),t)) -> app(app(cons(),app(f,h)),app(app(map_1(),f),t))
 app(app(app(map_2(),f),c),app(app(cons(),h),t)) ->
 app(app(cons(),app(app(f,h),c)),app(app(app(map_2(),f),c),t))
 app(app(app(app(map_3(),f),g()),c),app(app(cons(),h),t)) ->
 app(app(cons(),app(app(app(f,g()),h),c)),app(app(app(app(map_3(),f),g()),c),t))

Proof:
 Uncurry Processor:
  map_12(f,cons2(h,t)) -> cons2(app(f,h),map_12(f,t))
  map_23(f,c,cons2(h,t)) -> cons2(app(app(f,h),c),map_23(f,c,t))
  map_34(f,g(),c,cons2(h,t)) -> cons2(app(app(app(f,g()),h),c),map_34(f,g(),c,t))
  app(map_11(x6),x7) -> map_12(x6,x7)
  app(map_1(),x7) -> map_11(x7)
  app(cons1(x6),x7) -> cons2(x6,x7)
  app(cons(),x7) -> cons1(x7)
  app(map_22(x6,x5),x7) -> map_23(x6,x5,x7)
  app(map_21(x6),x7) -> map_22(x6,x7)
  app(map_2(),x7) -> map_21(x7)
  app(map_33(x6,x5,x4),x7) -> map_34(x6,x5,x4,x7)
  app(map_32(x6,x5),x7) -> map_33(x6,x5,x7)
  app(map_31(x6),x7) -> map_32(x6,x7)
  app(map_3(),x7) -> map_31(x7)
  DP Processor:
   DPs:
    map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t)
    map_1{2,#}(f,cons2(h,t)) -> app#(f,h)
    map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t)
    map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h)
    map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c)
    map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t)
    map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g())
    map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h)
    map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c)
    app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
    app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
    app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
   TRS:
    map_12(f,cons2(h,t)) -> cons2(app(f,h),map_12(f,t))
    map_23(f,c,cons2(h,t)) -> cons2(app(app(f,h),c),map_23(f,c,t))
    map_34(f,g(),c,cons2(h,t)) -> cons2(app(app(app(f,g()),h),c),map_34(f,g(),c,t))
    app(map_11(x6),x7) -> map_12(x6,x7)
    app(map_1(),x7) -> map_11(x7)
    app(cons1(x6),x7) -> cons2(x6,x7)
    app(cons(),x7) -> cons1(x7)
    app(map_22(x6,x5),x7) -> map_23(x6,x5,x7)
    app(map_21(x6),x7) -> map_22(x6,x7)
    app(map_2(),x7) -> map_21(x7)
    app(map_33(x6,x5,x4),x7) -> map_34(x6,x5,x4,x7)
    app(map_32(x6,x5),x7) -> map_33(x6,x5,x7)
    app(map_31(x6),x7) -> map_32(x6,x7)
    app(map_3(),x7) -> map_31(x7)
   TDG Processor:
    DPs:
     map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t)
     map_1{2,#}(f,cons2(h,t)) -> app#(f,h)
     map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t)
     map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h)
     map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g())
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c)
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
    TRS:
     map_12(f,cons2(h,t)) -> cons2(app(f,h),map_12(f,t))
     map_23(f,c,cons2(h,t)) -> cons2(app(app(f,h),c),map_23(f,c,t))
     map_34(f,g(),c,cons2(h,t)) -> cons2(app(app(app(f,g()),h),c),map_34(f,g(),c,t))
     app(map_11(x6),x7) -> map_12(x6,x7)
     app(map_1(),x7) -> map_11(x7)
     app(cons1(x6),x7) -> cons2(x6,x7)
     app(cons(),x7) -> cons1(x7)
     app(map_22(x6,x5),x7) -> map_23(x6,x5,x7)
     app(map_21(x6),x7) -> map_22(x6,x7)
     app(map_2(),x7) -> map_21(x7)
     app(map_33(x6,x5,x4),x7) -> map_34(x6,x5,x4,x7)
     app(map_32(x6,x5),x7) -> map_33(x6,x5,x7)
     app(map_31(x6),x7) -> map_32(x6,x7)
     app(map_3(),x7) -> map_31(x7)
    graph:
     map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t) ->
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t) ->
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t) ->
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g())
     map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t) ->
     map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c) ->
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c) ->
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c) ->
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h) ->
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h) ->
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h) ->
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g()) ->
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g()) ->
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g()) ->
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
     map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t) ->
     map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c)
     map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t) ->
     map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h)
     map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t) ->
     map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t)
     map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c) ->
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
     map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c) ->
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
     map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c) ->
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
     map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h) ->
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
     map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h) ->
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
     map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h) ->
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7) ->
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c)
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7) ->
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h)
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7) ->
     map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g())
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7) ->
     map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t)
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7) ->
     map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c)
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7) ->
     map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h)
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7) ->
     map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t)
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7) ->
     map_1{2,#}(f,cons2(h,t)) -> app#(f,h)
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7) ->
     map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t)
     map_1{2,#}(f,cons2(h,t)) -> app#(f,h) ->
     app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
     map_1{2,#}(f,cons2(h,t)) -> app#(f,h) ->
     app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
     map_1{2,#}(f,cons2(h,t)) -> app#(f,h) ->
     app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
     map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t) ->
     map_1{2,#}(f,cons2(h,t)) -> app#(f,h)
     map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t) -> map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t)
    CDG Processor:
     DPs:
      map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t)
      map_1{2,#}(f,cons2(h,t)) -> app#(f,h)
      map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t)
      map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h)
      map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g())
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c)
      app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
     TRS:
      map_12(f,cons2(h,t)) -> cons2(app(f,h),map_12(f,t))
      map_23(f,c,cons2(h,t)) -> cons2(app(app(f,h),c),map_23(f,c,t))
      map_34(f,g(),c,cons2(h,t)) -> cons2(app(app(app(f,g()),h),c),map_34(f,g(),c,t))
      app(map_11(x6),x7) -> map_12(x6,x7)
      app(map_1(),x7) -> map_11(x7)
      app(cons1(x6),x7) -> cons2(x6,x7)
      app(cons(),x7) -> cons1(x7)
      app(map_22(x6,x5),x7) -> map_23(x6,x5,x7)
      app(map_21(x6),x7) -> map_22(x6,x7)
      app(map_2(),x7) -> map_21(x7)
      app(map_33(x6,x5,x4),x7) -> map_34(x6,x5,x4,x7)
      app(map_32(x6,x5),x7) -> map_33(x6,x5,x7)
      app(map_31(x6),x7) -> map_32(x6,x7)
      app(map_3(),x7) -> map_31(x7)
     graph:
      map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t) ->
      map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t) ->
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g())
      map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t) ->
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t) ->
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c) ->
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c) ->
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h) ->
      app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h) ->
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h) ->
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g()) ->
      app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g()) ->
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g()) ->
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
      map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t) ->
      map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t)
      map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t) ->
      map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h)
      map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t) ->
      map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c)
      map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c) ->
      app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
      map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c) ->
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
      map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c) ->
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
      map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h) ->
      app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
      map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h) ->
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
      map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h) ->
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7) ->
      map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t)
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7) ->
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(f,g())
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7) ->
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h)
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7) ->
      map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c)
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7) ->
      map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t)
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7) ->
      map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h)
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7) ->
      map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c)
      app#(map_11(x6),x7) -> map_1{2,#}(x6,x7) ->
      map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t)
      app#(map_11(x6),x7) -> map_1{2,#}(x6,x7) ->
      map_1{2,#}(f,cons2(h,t)) -> app#(f,h)
      map_1{2,#}(f,cons2(h,t)) -> app#(f,h) ->
      app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
      map_1{2,#}(f,cons2(h,t)) -> app#(f,h) ->
      app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
      map_1{2,#}(f,cons2(h,t)) -> app#(f,h) ->
      app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
      map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t) ->
      map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t)
      map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t) -> map_1{2,#}(f,cons2(h,t)) -> app#(f,h)
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [map_3{4,#}](x0, x1, x2, x3) = 1x0 + 4x2 + 4x3,
       
       [map_2{3,#}](x0, x1, x2) = x0 + 4x1 + 4x2,
       
       [app#](x0, x1) = x0 + 4x1 + 0,
       
       [map_1{2,#}](x0, x1) = 4x0 + 4x1,
       
       [map_31](x0) = 4x0,
       
       [map_32](x0, x1) = 1x0 + 0,
       
       [map_34](x0, x1, x2, x3) = x0 + 4x2 + 4x3,
       
       [map_33](x0, x1, x2) = 1x0 + 4x2 + 0,
       
       [map_21](x0) = x0,
       
       [map_23](x0, x1, x2) = x0 + 4x1 + 4x2,
       
       [map_22](x0, x1) = x0 + 4x1,
       
       [cons2](x0, x1) = x0 + x1 + 2,
       
       [cons1](x0) = 4x0 + 7,
       
       [map_12](x0, x1) = 4x0 + 4x1 + 7,
       
       [map_11](x0) = 4x0 + 7,
       
       [g] = 1,
       
       [map_3] = 5,
       
       [map_2] = 7,
       
       [cons] = 7,
       
       [app](x0, x1) = x0 + 4x1 + 0,
       
       [map_1] = 7
      orientation:
       map_1{2,#}(f,cons2(h,t)) = 4f + 4h + 4t + 6 >= 4f + 4t = map_1{2,#}(f,t)
       
       map_1{2,#}(f,cons2(h,t)) = 4f + 4h + 4t + 6 >= f + 4h + 0 = app#(f,h)
       
       map_2{3,#}(f,c,cons2(h,t)) = 4c + f + 4h + 4t + 6 >= 4c + f + 4t = map_2{3,#}(f,c,t)
       
       map_2{3,#}(f,c,cons2(h,t)) = 4c + f + 4h + 4t + 6 >= f + 4h + 0 = app#(f,h)
       
       map_2{3,#}(f,c,cons2(h,t)) = 4c + f + 4h + 4t + 6 >= 4c + f + 4h + 0 = app#(app(f,h),c)
       
       map_3{4,#}(f,g(),c,cons2(h,t)) = 4c + 1f + 4h + 4t + 6 >= 4c + 1f + 4t = map_3{4,#}(f,g(),c,t)
       
       map_3{4,#}(f,g(),c,cons2(h,t)) = 4c + 1f + 4h + 4t + 6 >= f + 5 = app#(f,g())
       
       map_3{4,#}(f,g(),c,cons2(h,t)) = 4c + 1f + 4h + 4t + 6 >= f + 4h + 5 = app#(app(f,g()),h)
       
       map_3{4,#}(f,g(),c,cons2(h,t)) = 4c + 1f + 4h + 4t + 6 >= 4c + f + 4h + 5 = app#(app(app(f,g()),h),c)
       
       app#(map_11(x6),x7) = 4x6 + 4x7 + 7 >= 4x6 + 4x7 = map_1{2,#}(x6,x7)
       
       app#(map_22(x6,x5),x7) = 4x5 + x6 + 4x7 + 0 >= 4x5 + x6 + 4x7 = map_2{3,#}(x6,x5,x7)
       
       app#(map_33(x6,x5,x4),x7) = 4x4 + 1x6 + 4x7 + 0 >= 4x4 + 1x6 + 4x7 = map_3{4,#}(x6,x5,x4,x7)
       
       map_12(f,cons2(h,t)) = 4f + 4h + 4t + 7 >= 4f + 4h + 4t + 7 = cons2(app(f,h),map_12(f,t))
       
       map_23(f,c,cons2(h,t)) = 4c + f + 4h + 4t + 6 >= 4c + f + 4h + 4t + 2 = cons2(app(app(f,h),c),map_23(f,c,t))
       
       map_34(f,g(),c,cons2(h,t)) = 4c + f + 4h + 4t + 6 >= 4c + f + 4h + 4t + 5 = cons2(app(app(app(f,g()),h),c),map_34(f,g(),c,t))
       
       app(map_11(x6),x7) = 4x6 + 4x7 + 7 >= 4x6 + 4x7 + 7 = map_12(x6,x7)
       
       app(map_1(),x7) = 4x7 + 7 >= 4x7 + 7 = map_11(x7)
       
       app(cons1(x6),x7) = 4x6 + 4x7 + 7 >= x6 + x7 + 2 = cons2(x6,x7)
       
       app(cons(),x7) = 4x7 + 7 >= 4x7 + 7 = cons1(x7)
       
       app(map_22(x6,x5),x7) = 4x5 + x6 + 4x7 + 0 >= 4x5 + x6 + 4x7 = map_23(x6,x5,x7)
       
       app(map_21(x6),x7) = x6 + 4x7 + 0 >= x6 + 4x7 = map_22(x6,x7)
       
       app(map_2(),x7) = 4x7 + 7 >= x7 = map_21(x7)
       
       app(map_33(x6,x5,x4),x7) = 4x4 + 1x6 + 4x7 + 0 >= 4x4 + x6 + 4x7 = map_34(x6,x5,x4,x7)
       
       app(map_32(x6,x5),x7) = 1x6 + 4x7 + 0 >= 1x6 + 4x7 + 0 = map_33(x6,x5,x7)
       
       app(map_31(x6),x7) = 4x6 + 4x7 + 0 >= 1x6 + 0 = map_32(x6,x7)
       
       app(map_3(),x7) = 4x7 + 5 >= 4x7 = map_31(x7)
      problem:
       DPs:
        map_1{2,#}(f,cons2(h,t)) -> map_1{2,#}(f,t)
        map_1{2,#}(f,cons2(h,t)) -> app#(f,h)
        map_2{3,#}(f,c,cons2(h,t)) -> map_2{3,#}(f,c,t)
        map_2{3,#}(f,c,cons2(h,t)) -> app#(f,h)
        map_2{3,#}(f,c,cons2(h,t)) -> app#(app(f,h),c)
        map_3{4,#}(f,g(),c,cons2(h,t)) -> map_3{4,#}(f,g(),c,t)
        map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(f,g()),h)
        map_3{4,#}(f,g(),c,cons2(h,t)) -> app#(app(app(f,g()),h),c)
        app#(map_11(x6),x7) -> map_1{2,#}(x6,x7)
        app#(map_22(x6,x5),x7) -> map_2{3,#}(x6,x5,x7)
        app#(map_33(x6,x5,x4),x7) -> map_3{4,#}(x6,x5,x4,x7)
       TRS:
        map_12(f,cons2(h,t)) -> cons2(app(f,h),map_12(f,t))
        map_23(f,c,cons2(h,t)) -> cons2(app(app(f,h),c),map_23(f,c,t))
        map_34(f,g(),c,cons2(h,t)) -> cons2(app(app(app(f,g()),h),c),map_34(f,g(),c,t))
        app(map_11(x6),x7) -> map_12(x6,x7)
        app(map_1(),x7) -> map_11(x7)
        app(cons1(x6),x7) -> cons2(x6,x7)
        app(cons(),x7) -> cons1(x7)
        app(map_22(x6,x5),x7) -> map_23(x6,x5,x7)
        app(map_21(x6),x7) -> map_22(x6,x7)
        app(map_2(),x7) -> map_21(x7)
        app(map_33(x6,x5,x4),x7) -> map_34(x6,x5,x4,x7)
        app(map_32(x6,x5),x7) -> map_33(x6,x5,x7)
        app(map_31(x6),x7) -> map_32(x6,x7)
        app(map_3(),x7) -> map_31(x7)
      Open