MAYBE

Problem:
 ap(ap(map(),f),xs) -> ap(ap(ap(if(),ap(isEmpty(),xs)),f),xs)
 ap(ap(ap(if(),true()),f),xs) -> nil()
 ap(ap(ap(if(),false()),f),xs) ->
 ap(ap(cons(),ap(f,ap(last(),xs))),ap(ap(map(),f),ap(dropLast(),xs)))
 ap(isEmpty(),nil()) -> true()
 ap(isEmpty(),ap(ap(cons(),x),xs)) -> false()
 ap(last(),ap(ap(cons(),x),nil())) -> x
 ap(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap(last(),ap(ap(cons(),y),ys))
 ap(dropLast(),nil()) -> nil()
 ap(dropLast(),ap(ap(cons(),x),nil())) -> nil()
 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) -> nil()
  if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
  isEmpty1(nil()) -> true()
  isEmpty1(cons2(x,xs)) -> false()
  last1(cons2(x,nil())) -> x
  last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
  dropLast1(nil()) -> nil()
  dropLast1(cons2(x,nil())) -> nil()
  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(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,#}(false(),f,xs) -> dropLast{1,#}(xs)
    if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs))
    if{3,#}(false(),f,xs) -> last{1,#}(xs)
    if{3,#}(false(),f,xs) -> ap#(f,last1(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#(dropLast(),x7) -> dropLast{1,#}(x7)
   TRS:
    map2(f,xs) -> if3(isEmpty1(xs),f,xs)
    if3(true(),f,xs) -> nil()
    if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
    isEmpty1(nil()) -> true()
    isEmpty1(cons2(x,xs)) -> false()
    last1(cons2(x,nil())) -> x
    last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
    dropLast1(nil()) -> nil()
    dropLast1(cons2(x,nil())) -> nil()
    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(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,#}(false(),f,xs) -> dropLast{1,#}(xs)
     if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs))
     if{3,#}(false(),f,xs) -> last{1,#}(xs)
     if{3,#}(false(),f,xs) -> ap#(f,last1(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#(dropLast(),x7) -> dropLast{1,#}(x7)
    TRS:
     map2(f,xs) -> if3(isEmpty1(xs),f,xs)
     if3(true(),f,xs) -> nil()
     if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
     isEmpty1(nil()) -> true()
     isEmpty1(cons2(x,xs)) -> false()
     last1(cons2(x,nil())) -> x
     last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
     dropLast1(nil()) -> nil()
     dropLast1(cons2(x,nil())) -> nil()
     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(dropLast(),x7) -> dropLast1(x7)
    graph:
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7) ->
     if{3,#}(false(),f,xs) -> ap#(f,last1(xs))
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7) ->
     if{3,#}(false(),f,xs) -> last{1,#}(xs)
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7) ->
     if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs))
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7) ->
     if{3,#}(false(),f,xs) -> dropLast{1,#}(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))
     dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys)) ->
     dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys))
     if{3,#}(false(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(dropLast(),x7) -> dropLast{1,#}(x7)
     if{3,#}(false(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(last(),x7) -> last{1,#}(x7)
     if{3,#}(false(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(isEmpty(),x7) -> isEmpty{1,#}(x7)
     if{3,#}(false(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     if{3,#}(false(),f,xs) -> ap#(f,last1(xs)) ->
     ap#(map1(x6),x7) -> map{2,#}(x6,x7)
     if{3,#}(false(),f,xs) -> last{1,#}(xs) ->
     last{1,#}(cons2(x,cons2(y,ys))) -> last{1,#}(cons2(y,ys))
     if{3,#}(false(),f,xs) -> dropLast{1,#}(xs) ->
     dropLast{1,#}(cons2(x,cons2(y,ys))) -> dropLast{1,#}(cons2(y,ys))
     if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs)) ->
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
     if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs)) ->
     map{2,#}(f,xs) -> isEmpty{1,#}(xs)
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs) ->
     if{3,#}(false(),f,xs) -> ap#(f,last1(xs))
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs) ->
     if{3,#}(false(),f,xs) -> last{1,#}(xs)
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs) ->
     if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs))
     map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs) -> if{3,#}(false(),f,xs) -> dropLast{1,#}(xs)
    SCC Processor:
     #sccs: 3
     #rules: 7
     #arcs: 23/169
     DPs:
      ap#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
      if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs))
      map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
      if{3,#}(false(),f,xs) -> ap#(f,last1(xs))
      ap#(map1(x6),x7) -> map{2,#}(x6,x7)
     TRS:
      map2(f,xs) -> if3(isEmpty1(xs),f,xs)
      if3(true(),f,xs) -> nil()
      if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
      isEmpty1(nil()) -> true()
      isEmpty1(cons2(x,xs)) -> false()
      last1(cons2(x,nil())) -> x
      last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
      dropLast1(nil()) -> nil()
      dropLast1(cons2(x,nil())) -> nil()
      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(dropLast(),x7) -> dropLast1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(map{2,#}) = 0
       pi(if{3,#}) = 1
       pi(ap#) = 0
      problem:
       DPs:
        if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs))
        map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
        if{3,#}(false(),f,xs) -> ap#(f,last1(xs))
       TRS:
        map2(f,xs) -> if3(isEmpty1(xs),f,xs)
        if3(true(),f,xs) -> nil()
        if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
        isEmpty1(nil()) -> true()
        isEmpty1(cons2(x,xs)) -> false()
        last1(cons2(x,nil())) -> x
        last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
        dropLast1(nil()) -> nil()
        dropLast1(cons2(x,nil())) -> nil()
        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(dropLast(),x7) -> dropLast1(x7)
      SCC Processor:
       #sccs: 1
       #rules: 2
       #arcs: 8/9
       DPs:
        if{3,#}(false(),f,xs) -> map{2,#}(f,dropLast1(xs))
        map{2,#}(f,xs) -> if{3,#}(isEmpty1(xs),f,xs)
       TRS:
        map2(f,xs) -> if3(isEmpty1(xs),f,xs)
        if3(true(),f,xs) -> nil()
        if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
        isEmpty1(nil()) -> true()
        isEmpty1(cons2(x,xs)) -> false()
        last1(cons2(x,nil())) -> x
        last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
        dropLast1(nil()) -> nil()
        dropLast1(cons2(x,nil())) -> nil()
        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(dropLast(),x7) -> dropLast1(x7)
       Open
     
     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) -> nil()
      if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
      isEmpty1(nil()) -> true()
      isEmpty1(cons2(x,xs)) -> false()
      last1(cons2(x,nil())) -> x
      last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
      dropLast1(nil()) -> nil()
      dropLast1(cons2(x,nil())) -> nil()
      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(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) -> nil()
        if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
        isEmpty1(nil()) -> true()
        isEmpty1(cons2(x,xs)) -> false()
        last1(cons2(x,nil())) -> x
        last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
        dropLast1(nil()) -> nil()
        dropLast1(cons2(x,nil())) -> nil()
        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(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) -> nil()
      if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
      isEmpty1(nil()) -> true()
      isEmpty1(cons2(x,xs)) -> false()
      last1(cons2(x,nil())) -> x
      last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
      dropLast1(nil()) -> nil()
      dropLast1(cons2(x,nil())) -> nil()
      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(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) -> nil()
        if3(false(),f,xs) -> cons2(ap(f,last1(xs)),map2(f,dropLast1(xs)))
        isEmpty1(nil()) -> true()
        isEmpty1(cons2(x,xs)) -> false()
        last1(cons2(x,nil())) -> x
        last1(cons2(x,cons2(y,ys))) -> last1(cons2(y,ys))
        dropLast1(nil()) -> nil()
        dropLast1(cons2(x,nil())) -> nil()
        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(dropLast(),x7) -> dropLast1(x7)
      Qed