YES

Problem:
 ap(ap(map(),f),xs) -> ap(ap(ap(if(),ap(isEmpty(),xs)),f),xs)
 ap(ap(ap(if(),true()),f),xs) -> null()
 ap(ap(ap(if(),null()),f),xs) -> ap(ap(cons(),ap(f,ap(last(),xs))),ap(ap(if2(),f),xs))
 ap(ap(if2(),f),xs) -> ap(ap(map(),f),ap(dropLast(),xs))
 ap(isEmpty(),null()) -> true()
 ap(isEmpty(),ap(ap(cons(),x),xs)) -> null()
 ap(last(),ap(ap(cons(),x),null())) -> x
 ap(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap(last(),ap(ap(cons(),y),ys))
 ap(dropLast(),ap(ap(cons(),x),null())) -> null()
 ap(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) ->
 ap(ap(cons(),x),ap(dropLast(),ap(ap(cons(),y),ys)))

Proof:
 Uncurry Processor:
  map2(f,xs) -> if3(isEmpty1(xs),f,xs)
  if3(true(),f,xs) -> null()
  if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
  if22(f,xs) -> map2(f,dropLast1(xs))
  isEmpty1(null()) -> true()
  isEmpty1(cons2(x,xs)) -> null()
  last1(cons2(x,null())) -> x
  last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
  dropLast1(cons2(x,null())) -> null()
  dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
  ap(map1(x6),x7) -> map2(x6,x7)
  ap(map(),x7) -> map1(x7)
  ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
  ap(if1(x6),x7) -> if2(x6,x7)
  ap(if(),x7) -> if1(x7)
  ap(isEmpty(),x7) -> isEmpty1(x7)
  ap(cons1(x6),x7) -> cons2(x6,x7)
  ap(cons(),x7) -> cons1(x7)
  ap(last(),x7) -> last1(x7)
  ap(if21(x6),x7) -> if22(x6,x7)
  ap(if2(),x7) -> if21(x7)
  ap(dropLast(),x7) -> dropLast1(x7)
  DP Processor:
   DPs:
    map{2,#}(f,xs) -> isEmpty{1,#}(xs)
    map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
    if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
    if{3,#}(null(),f,xs) -> last{1,#}(xs)
    if{3,#}(null(),f,xs) -> ap#(f,last1(xs))
    if2{2,#}(f,xs) -> dropLast{1,#}(xs)
    if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs))
    last{1,#}(cons2(x,cons2(y,ys))) -> last{1,#}(cons2(y,ys))
    dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys))
    ap#(map1(x6),x7) -> map{2,#}(x6,x7)
    ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
    ap#(isEmpty(),x7) -> isEmpty{1,#}(x7)
    ap#(last(),x7) -> last{1,#}(x7)
    ap#(if21(x6),x7) -> if2{2,#}(x6,x7)
    ap#(dropLast(),x7) -> dropLast{1,#}(x7)
   TRS:
    map2(f,xs) -> if3(isEmpty1(xs),f,xs)
    if3(true(),f,xs) -> null()
    if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
    if22(f,xs) -> map2(f,dropLast1(xs))
    isEmpty1(null()) -> true()
    isEmpty1(cons2(x,xs)) -> null()
    last1(cons2(x,null())) -> x
    last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
    dropLast1(cons2(x,null())) -> null()
    dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
    ap(map1(x6),x7) -> map2(x6,x7)
    ap(map(),x7) -> map1(x7)
    ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
    ap(if1(x6),x7) -> if2(x6,x7)
    ap(if(),x7) -> if1(x7)
    ap(isEmpty(),x7) -> isEmpty1(x7)
    ap(cons1(x6),x7) -> cons2(x6,x7)
    ap(cons(),x7) -> cons1(x7)
    ap(last(),x7) -> last1(x7)
    ap(if21(x6),x7) -> if22(x6,x7)
    ap(if2(),x7) -> if21(x7)
    ap(dropLast(),x7) -> dropLast1(x7)
   TDG Processor:
    DPs:
     map{2,#}(f,xs) -> isEmpty{1,#}(xs)
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
     if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
     if{3,#}(null(),f,xs) -> last{1,#}(xs)
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs))
     if2{2,#}(f,xs) -> dropLast{1,#}(xs)
     if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs))
     last{1,#}(cons2(x,cons2(y,ys))) -> last{1,#}(cons2(y,ys))
     dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys))
     ap#(map1(x6),x7) -> map{2,#}(x6,x7)
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     ap#(isEmpty(),x7) -> isEmpty{1,#}(x7)
     ap#(last(),x7) -> last{1,#}(x7)
     ap#(if21(x6),x7) -> if2{2,#}(x6,x7)
     ap#(dropLast(),x7) -> dropLast{1,#}(x7)
    TRS:
     map2(f,xs) -> if3(isEmpty1(xs),f,xs)
     if3(true(),f,xs) -> null()
     if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
     if22(f,xs) -> map2(f,dropLast1(xs))
     isEmpty1(null()) -> true()
     isEmpty1(cons2(x,xs)) -> null()
     last1(cons2(x,null())) -> x
     last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
     dropLast1(cons2(x,null())) -> null()
     dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
     ap(map1(x6),x7) -> map2(x6,x7)
     ap(map(),x7) -> map1(x7)
     ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
     ap(if1(x6),x7) -> if2(x6,x7)
     ap(if(),x7) -> if1(x7)
     ap(isEmpty(),x7) -> isEmpty1(x7)
     ap(cons1(x6),x7) -> cons2(x6,x7)
     ap(cons(),x7) -> cons1(x7)
     ap(last(),x7) -> last1(x7)
     ap(if21(x6),x7) -> if22(x6,x7)
     ap(if2(),x7) -> if21(x7)
     ap(dropLast(),x7) -> dropLast1(x7)
    graph:
     dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys)) ->
     dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys))
     ap#(if21(x6),x7) -> if2{2,#}(x6,x7) ->
     if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs))
     ap#(if21(x6),x7) -> if2{2,#}(x6,x7) ->
     if2{2,#}(f,xs) -> dropLast{1,#}(xs)
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7) ->
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs))
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7) ->
     if{3,#}(null(),f,xs) -> last{1,#}(xs)
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7) ->
     if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
     ap#(map1(x6),x7) -> map{2,#}(x6,x7) ->
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
     ap#(map1(x6),x7) -> map{2,#}(x6,x7) ->
     map{2,#}(f,xs) -> isEmpty{1,#}(xs)
     ap#(dropLast(),x7) -> dropLast{1,#}(x7) ->
     dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys))
     ap#(last(),x7) -> last{1,#}(x7) ->
     last{1,#}(cons2(x,cons2(y,ys))) -> last{1,#}(cons2(y,ys))
     last{1,#}(cons2(x,cons2(y,ys))) -> last{1,#}(cons2(y,ys)) ->
     last{1,#}(cons2(x,cons2(y,ys))) -> last{1,#}(cons2(y,ys))
     if2{2,#}(f,xs) -> dropLast{1,#}(xs) ->
     dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys))
     if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs)) ->
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
     if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs)) ->
     map{2,#}(f,xs) -> isEmpty{1,#}(xs)
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(dropLast(),x7) -> dropLast{1,#}(x7)
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(if21(x6),x7) -> if2{2,#}(x6,x7)
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(last(),x7) -> last{1,#}(x7)
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(isEmpty(),x7) -> isEmpty{1,#}(x7)
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(map1(x6),x7) -> map{2,#}(x6,x7)
     if{3,#}(null(),f,xs) -> last{1,#}(xs) ->
     last{1,#}(cons2(x,cons2(y,ys))) -> last{1,#}(cons2(y,ys))
     if{3,#}(null(),f,xs) -> if2{2,#}(f,xs) ->
     if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs))
     if{3,#}(null(),f,xs) -> if2{2,#}(f,xs) ->
     if2{2,#}(f,xs) -> dropLast{1,#}(xs)
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs) ->
     if{3,#}(null(),f,xs) -> ap#(f,last1(xs))
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs) ->
     if{3,#}(null(),f,xs) -> last{1,#}(xs)
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs) -> if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
    SCC Processor:
     #sccs: 3
     #rules: 9
     #arcs: 26/225
     DPs:
      ap#(if21(x6),x7) -> if2{2,#}(x6,x7)
      if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs))
      map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
      if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
      if{3,#}(null(),f,xs) -> ap#(f,last1(xs))
      ap#(map1(x6),x7) -> map{2,#}(x6,x7)
      ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     TRS:
      map2(f,xs) -> if3(isEmpty1(xs),f,xs)
      if3(true(),f,xs) -> null()
      if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
      if22(f,xs) -> map2(f,dropLast1(xs))
      isEmpty1(null()) -> true()
      isEmpty1(cons2(x,xs)) -> null()
      last1(cons2(x,null())) -> x
      last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
      dropLast1(cons2(x,null())) -> null()
      dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
      ap(map1(x6),x7) -> map2(x6,x7)
      ap(map(),x7) -> map1(x7)
      ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
      ap(if1(x6),x7) -> if2(x6,x7)
      ap(if(),x7) -> if1(x7)
      ap(isEmpty(),x7) -> isEmpty1(x7)
      ap(cons1(x6),x7) -> cons2(x6,x7)
      ap(cons(),x7) -> cons1(x7)
      ap(last(),x7) -> last1(x7)
      ap(if21(x6),x7) -> if22(x6,x7)
      ap(if2(),x7) -> if21(x7)
      ap(dropLast(),x7) -> dropLast1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(map{2,#}) = 0
       pi(if{3,#}) = 1
       pi(if2{2,#}) = 0
       pi(ap#) = 0
      problem:
       DPs:
        if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs))
        map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
        if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
        if{3,#}(null(),f,xs) -> ap#(f,last1(xs))
       TRS:
        map2(f,xs) -> if3(isEmpty1(xs),f,xs)
        if3(true(),f,xs) -> null()
        if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
        if22(f,xs) -> map2(f,dropLast1(xs))
        isEmpty1(null()) -> true()
        isEmpty1(cons2(x,xs)) -> null()
        last1(cons2(x,null())) -> x
        last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
        dropLast1(cons2(x,null())) -> null()
        dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
        ap(map1(x6),x7) -> map2(x6,x7)
        ap(map(),x7) -> map1(x7)
        ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
        ap(if1(x6),x7) -> if2(x6,x7)
        ap(if(),x7) -> if1(x7)
        ap(isEmpty(),x7) -> isEmpty1(x7)
        ap(cons1(x6),x7) -> cons2(x6,x7)
        ap(cons(),x7) -> cons1(x7)
        ap(last(),x7) -> last1(x7)
        ap(if21(x6),x7) -> if22(x6,x7)
        ap(if2(),x7) -> if21(x7)
        ap(dropLast(),x7) -> dropLast1(x7)
      SCC Processor:
       #sccs: 1
       #rules: 3
       #arcs: 11/16
       DPs:
        if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs))
        map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
        if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
       TRS:
        map2(f,xs) -> if3(isEmpty1(xs),f,xs)
        if3(true(),f,xs) -> null()
        if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
        if22(f,xs) -> map2(f,dropLast1(xs))
        isEmpty1(null()) -> true()
        isEmpty1(cons2(x,xs)) -> null()
        last1(cons2(x,null())) -> x
        last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
        dropLast1(cons2(x,null())) -> null()
        dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
        ap(map1(x6),x7) -> map2(x6,x7)
        ap(map(),x7) -> map1(x7)
        ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
        ap(if1(x6),x7) -> if2(x6,x7)
        ap(if(),x7) -> if1(x7)
        ap(isEmpty(),x7) -> isEmpty1(x7)
        ap(cons1(x6),x7) -> cons2(x6,x7)
        ap(cons(),x7) -> cons1(x7)
        ap(last(),x7) -> last1(x7)
        ap(if21(x6),x7) -> if22(x6,x7)
        ap(if2(),x7) -> if21(x7)
        ap(dropLast(),x7) -> dropLast1(x7)
       Usable Rule Processor:
        DPs:
         if2{2,#}(f,xs) -> map{2,#}(f,dropLast1(xs))
         map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
         if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
        TRS:
         dropLast1(cons2(x,null())) -> null()
         dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
         isEmpty1(null()) -> true()
         isEmpty1(cons2(x,xs)) -> null()
        Arctic Interpretation Processor:
         dimension: 1
         usable rules:
          dropLast1(cons2(x,null())) -> null()
          dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
          isEmpty1(null()) -> true()
          isEmpty1(cons2(x,xs)) -> null()
         interpretation:
          [if2{2,#}](x0, x1) = -1x1 + 2,
          
          [if{3,#}](x0, x1, x2) = -2x0 + x2 + -16,
          
          [map{2,#}](x0, x1) = x1 + 1,
          
          [dropLast1](x0) = -2x0 + 0,
          
          [cons2](x0, x1) = 2x1 + 4,
          
          [isEmpty1](x0) = x0 + 0,
          
          [null] = 4,
          
          [true] = 1
         orientation:
          if2{2,#}(f,xs) = -1xs + 2 >= -2xs + 1 = map{2,#}(f,dropLast1(xs))
          
          map{2,#}(f,xs) = xs + 1 >= xs + -2 = if{3,#}(isEmpty1(xs),f,xs)
          
          if{3,#}(null(),f,xs) = xs + 2 >= -1xs + 2 = if2{2,#}(f,xs)
          
          dropLast1(cons2(x,null())) = 4 >= 4 = null()
          
          dropLast1(cons2(x,cons2(y,ys))) = 2ys + 4 >= 2ys + 4 = cons2(x,dropLast1(cons2(y,ys)))
          
          isEmpty1(null()) = 4 >= 1 = true()
          
          isEmpty1(cons2(x,xs)) = 2xs + 4 >= 4 = null()
         problem:
          DPs:
           map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
           if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
          TRS:
           dropLast1(cons2(x,null())) -> null()
           dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
           isEmpty1(null()) -> true()
           isEmpty1(cons2(x,xs)) -> null()
         Restore Modifier:
          DPs:
           map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
           if{3,#}(null(),f,xs) -> if2{2,#}(f,xs)
          TRS:
           map2(f,xs) -> if3(isEmpty1(xs),f,xs)
           if3(true(),f,xs) -> null()
           if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
           if22(f,xs) -> map2(f,dropLast1(xs))
           isEmpty1(null()) -> true()
           isEmpty1(cons2(x,xs)) -> null()
           last1(cons2(x,null())) -> x
           last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
           dropLast1(cons2(x,null())) -> null()
           dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
           ap(map1(x6),x7) -> map2(x6,x7)
           ap(map(),x7) -> map1(x7)
           ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
           ap(if1(x6),x7) -> if2(x6,x7)
           ap(if(),x7) -> if1(x7)
           ap(isEmpty(),x7) -> isEmpty1(x7)
           ap(cons1(x6),x7) -> cons2(x6,x7)
           ap(cons(),x7) -> cons1(x7)
           ap(last(),x7) -> last1(x7)
           ap(if21(x6),x7) -> if22(x6,x7)
           ap(if2(),x7) -> if21(x7)
           ap(dropLast(),x7) -> dropLast1(x7)
          SCC Processor:
           #sccs: 0
           #rules: 0
           #arcs: 3/4
           
     
     DPs:
      last{1,#}(cons2(x,cons2(y,ys))) -> last{1,#}(cons2(y,ys))
     TRS:
      map2(f,xs) -> if3(isEmpty1(xs),f,xs)
      if3(true(),f,xs) -> null()
      if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
      if22(f,xs) -> map2(f,dropLast1(xs))
      isEmpty1(null()) -> true()
      isEmpty1(cons2(x,xs)) -> null()
      last1(cons2(x,null())) -> x
      last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
      dropLast1(cons2(x,null())) -> null()
      dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
      ap(map1(x6),x7) -> map2(x6,x7)
      ap(map(),x7) -> map1(x7)
      ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
      ap(if1(x6),x7) -> if2(x6,x7)
      ap(if(),x7) -> if1(x7)
      ap(isEmpty(),x7) -> isEmpty1(x7)
      ap(cons1(x6),x7) -> cons2(x6,x7)
      ap(cons(),x7) -> cons1(x7)
      ap(last(),x7) -> last1(x7)
      ap(if21(x6),x7) -> if22(x6,x7)
      ap(if2(),x7) -> if21(x7)
      ap(dropLast(),x7) -> dropLast1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(last{1,#}) = 0
      problem:
       DPs:
        
       TRS:
        map2(f,xs) -> if3(isEmpty1(xs),f,xs)
        if3(true(),f,xs) -> null()
        if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
        if22(f,xs) -> map2(f,dropLast1(xs))
        isEmpty1(null()) -> true()
        isEmpty1(cons2(x,xs)) -> null()
        last1(cons2(x,null())) -> x
        last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
        dropLast1(cons2(x,null())) -> null()
        dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
        ap(map1(x6),x7) -> map2(x6,x7)
        ap(map(),x7) -> map1(x7)
        ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
        ap(if1(x6),x7) -> if2(x6,x7)
        ap(if(),x7) -> if1(x7)
        ap(isEmpty(),x7) -> isEmpty1(x7)
        ap(cons1(x6),x7) -> cons2(x6,x7)
        ap(cons(),x7) -> cons1(x7)
        ap(last(),x7) -> last1(x7)
        ap(if21(x6),x7) -> if22(x6,x7)
        ap(if2(),x7) -> if21(x7)
        ap(dropLast(),x7) -> dropLast1(x7)
      Qed
     
     DPs:
      dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys))
     TRS:
      map2(f,xs) -> if3(isEmpty1(xs),f,xs)
      if3(true(),f,xs) -> null()
      if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
      if22(f,xs) -> map2(f,dropLast1(xs))
      isEmpty1(null()) -> true()
      isEmpty1(cons2(x,xs)) -> null()
      last1(cons2(x,null())) -> x
      last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
      dropLast1(cons2(x,null())) -> null()
      dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
      ap(map1(x6),x7) -> map2(x6,x7)
      ap(map(),x7) -> map1(x7)
      ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
      ap(if1(x6),x7) -> if2(x6,x7)
      ap(if(),x7) -> if1(x7)
      ap(isEmpty(),x7) -> isEmpty1(x7)
      ap(cons1(x6),x7) -> cons2(x6,x7)
      ap(cons(),x7) -> cons1(x7)
      ap(last(),x7) -> last1(x7)
      ap(if21(x6),x7) -> if22(x6,x7)
      ap(if2(),x7) -> if21(x7)
      ap(dropLast(),x7) -> dropLast1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(dropLast{1,#}) = 0
      problem:
       DPs:
        
       TRS:
        map2(f,xs) -> if3(isEmpty1(xs),f,xs)
        if3(true(),f,xs) -> null()
        if3(null(),f,xs) -> cons2(ap(f,last1(xs)),if22(f,xs))
        if22(f,xs) -> map2(f,dropLast1(xs))
        isEmpty1(null()) -> true()
        isEmpty1(cons2(x,xs)) -> null()
        last1(cons2(x,null())) -> x
        last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
        dropLast1(cons2(x,null())) -> null()
        dropLast1(cons2(x,cons2(y,ys))) -> cons2(x,dropLast1(cons2(y,ys)))
        ap(map1(x6),x7) -> map2(x6,x7)
        ap(map(),x7) -> map1(x7)
        ap(if2(x6,x5),x7) -> if3(x6,x5,x7)
        ap(if1(x6),x7) -> if2(x6,x7)
        ap(if(),x7) -> if1(x7)
        ap(isEmpty(),x7) -> isEmpty1(x7)
        ap(cons1(x6),x7) -> cons2(x6,x7)
        ap(cons(),x7) -> cons1(x7)
        ap(last(),x7) -> last1(x7)
        ap(if21(x6),x7) -> if22(x6,x7)
        ap(if2(),x7) -> if21(x7)
        ap(dropLast(),x7) -> dropLast1(x7)
      Qed