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:
 DP Processor:
  DPs:
   ap#(ap(map(),f),xs) -> ap#(isEmpty(),xs)
   ap#(ap(map(),f),xs) -> ap#(if(),ap(isEmpty(),xs))
   ap#(ap(map(),f),xs) -> ap#(ap(if(),ap(isEmpty(),xs)),f)
   ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs)
   ap#(ap(ap(if(),false()),f),xs) -> ap#(dropLast(),xs)
   ap#(ap(ap(if(),false()),f),xs) -> ap#(map(),f)
   ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs))
   ap#(ap(ap(if(),false()),f),xs) -> ap#(last(),xs)
   ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs))
   ap#(ap(ap(if(),false()),f),xs) -> ap#(cons(),ap(f,ap(last(),xs)))
   ap#(ap(ap(if(),false()),f),xs) ->
   ap#(ap(cons(),ap(f,ap(last(),xs))),ap(ap(map(),f),ap(dropLast(),xs)))
   ap#(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(last(),ap(ap(cons(),y),ys))
   ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(dropLast(),ap(ap(cons(),y),ys))
   ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) ->
   ap#(ap(cons(),x),ap(dropLast(),ap(ap(cons(),y),ys)))
  TRS:
   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)))
  EDG Processor:
   DPs:
    ap#(ap(map(),f),xs) -> ap#(isEmpty(),xs)
    ap#(ap(map(),f),xs) -> ap#(if(),ap(isEmpty(),xs))
    ap#(ap(map(),f),xs) -> ap#(ap(if(),ap(isEmpty(),xs)),f)
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(dropLast(),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(map(),f)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(last(),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(cons(),ap(f,ap(last(),xs)))
    ap#(ap(ap(if(),false()),f),xs) ->
    ap#(ap(cons(),ap(f,ap(last(),xs))),ap(ap(map(),f),ap(dropLast(),xs)))
    ap#(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(last(),ap(ap(cons(),y),ys))
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(dropLast(),ap(ap(cons(),y),ys))
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) ->
    ap#(ap(cons(),x),ap(dropLast(),ap(ap(cons(),y),ys)))
   TRS:
    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)))
   graph:
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(dropLast(),ap(ap(cons(),y),ys)) ->
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(dropLast(),ap(ap(cons(),y),ys))
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(dropLast(),ap(ap(cons(),y),ys)) ->
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) ->
    ap#(ap(cons(),x),ap(dropLast(),ap(ap(cons(),y),ys)))
    ap#(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(last(),ap(ap(cons(),y),ys)) ->
    ap#(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(last(),ap(ap(cons(),y),ys))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(dropLast(),xs) ->
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(dropLast(),ap(ap(cons(),y),ys))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(dropLast(),xs) ->
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) ->
    ap#(ap(cons(),x),ap(dropLast(),ap(ap(cons(),y),ys)))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(last(),xs) ->
    ap#(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(last(),ap(ap(cons(),y),ys))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs)) ->
    ap#(ap(map(),f),xs) -> ap#(isEmpty(),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs)) ->
    ap#(ap(map(),f),xs) -> ap#(if(),ap(isEmpty(),xs))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs)) ->
    ap#(ap(map(),f),xs) -> ap#(ap(if(),ap(isEmpty(),xs)),f)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs)) ->
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(map(),f),xs) -> ap#(isEmpty(),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(map(),f),xs) -> ap#(if(),ap(isEmpty(),xs))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(map(),f),xs) -> ap#(ap(if(),ap(isEmpty(),xs)),f)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(dropLast(),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(map(),f)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(last(),xs)
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(cons(),ap(f,ap(last(),xs)))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(ap(ap(if(),false()),f),xs) ->
    ap#(ap(cons(),ap(f,ap(last(),xs))),ap(ap(map(),f),ap(dropLast(),xs)))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(last(),ap(ap(cons(),y),ys))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(dropLast(),ap(ap(cons(),y),ys))
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs)) ->
    ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) ->
    ap#(ap(cons(),x),ap(dropLast(),ap(ap(cons(),y),ys)))
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(dropLast(),xs)
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(map(),f)
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs))
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(last(),xs)
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs))
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs) ->
    ap#(ap(ap(if(),false()),f),xs) -> ap#(cons(),ap(f,ap(last(),xs)))
    ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs) ->
    ap#(ap(ap(if(),false()),f),xs) ->
    ap#(ap(cons(),ap(f,ap(last(),xs))),ap(ap(map(),f),ap(dropLast(),xs)))
   SCC Processor:
    #sccs: 3
    #rules: 5
    #arcs: 31/196
    DPs:
     ap#(ap(ap(if(),false()),f),xs) -> ap#(ap(map(),f),ap(dropLast(),xs))
     ap#(ap(map(),f),xs) -> ap#(ap(ap(if(),ap(isEmpty(),xs)),f),xs)
     ap#(ap(ap(if(),false()),f),xs) -> ap#(f,ap(last(),xs))
    TRS:
     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)))
    Open
    
    DPs:
     ap#(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(last(),ap(ap(cons(),y),ys))
    TRS:
     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)))
    Open
    
    DPs:
     ap#(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap#(dropLast(),ap(ap(cons(),y),ys))
    TRS:
     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)))
    Open