MAYBE

Problem:
 isEmpty(nil()) -> true()
 isEmpty(cons(x,xs)) -> false()
 last(cons(x,nil())) -> x
 last(cons(x,cons(y,ys))) -> last(cons(y,ys))
 dropLast(nil()) -> nil()
 dropLast(cons(x,nil())) -> nil()
 dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
 append(nil(),ys) -> ys
 append(cons(x,xs),ys) -> cons(x,append(xs,ys))
 reverse(xs) -> rev(xs,nil())
 rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
 if(true(),xs,ys,zs) -> zs
 if(false(),xs,ys,zs) -> rev(xs,ys)

Proof:
 DP Processor:
  DPs:
   last#(cons(x,cons(y,ys))) -> last#(cons(y,ys))
   dropLast#(cons(x,cons(y,ys))) -> dropLast#(cons(y,ys))
   append#(cons(x,xs),ys) -> append#(xs,ys)
   reverse#(xs) -> rev#(xs,nil())
   rev#(xs,ys) -> last#(xs)
   rev#(xs,ys) -> append#(ys,last(xs))
   rev#(xs,ys) -> dropLast#(xs)
   rev#(xs,ys) -> isEmpty#(xs)
   rev#(xs,ys) -> if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
   if#(false(),xs,ys,zs) -> rev#(xs,ys)
  TRS:
   isEmpty(nil()) -> true()
   isEmpty(cons(x,xs)) -> false()
   last(cons(x,nil())) -> x
   last(cons(x,cons(y,ys))) -> last(cons(y,ys))
   dropLast(nil()) -> nil()
   dropLast(cons(x,nil())) -> nil()
   dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
   append(nil(),ys) -> ys
   append(cons(x,xs),ys) -> cons(x,append(xs,ys))
   reverse(xs) -> rev(xs,nil())
   rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
   if(true(),xs,ys,zs) -> zs
   if(false(),xs,ys,zs) -> rev(xs,ys)
  TDG Processor:
   DPs:
    last#(cons(x,cons(y,ys))) -> last#(cons(y,ys))
    dropLast#(cons(x,cons(y,ys))) -> dropLast#(cons(y,ys))
    append#(cons(x,xs),ys) -> append#(xs,ys)
    reverse#(xs) -> rev#(xs,nil())
    rev#(xs,ys) -> last#(xs)
    rev#(xs,ys) -> append#(ys,last(xs))
    rev#(xs,ys) -> dropLast#(xs)
    rev#(xs,ys) -> isEmpty#(xs)
    rev#(xs,ys) -> if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
    if#(false(),xs,ys,zs) -> rev#(xs,ys)
   TRS:
    isEmpty(nil()) -> true()
    isEmpty(cons(x,xs)) -> false()
    last(cons(x,nil())) -> x
    last(cons(x,cons(y,ys))) -> last(cons(y,ys))
    dropLast(nil()) -> nil()
    dropLast(cons(x,nil())) -> nil()
    dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
    append(nil(),ys) -> ys
    append(cons(x,xs),ys) -> cons(x,append(xs,ys))
    reverse(xs) -> rev(xs,nil())
    rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
    if(true(),xs,ys,zs) -> zs
    if(false(),xs,ys,zs) -> rev(xs,ys)
   graph:
    if#(false(),xs,ys,zs) -> rev#(xs,ys) ->
    rev#(xs,ys) -> if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
    if#(false(),xs,ys,zs) -> rev#(xs,ys) ->
    rev#(xs,ys) -> isEmpty#(xs)
    if#(false(),xs,ys,zs) -> rev#(xs,ys) ->
    rev#(xs,ys) -> dropLast#(xs)
    if#(false(),xs,ys,zs) -> rev#(xs,ys) ->
    rev#(xs,ys) -> append#(ys,last(xs))
    if#(false(),xs,ys,zs) -> rev#(xs,ys) ->
    rev#(xs,ys) -> last#(xs)
    rev#(xs,ys) -> if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys) ->
    if#(false(),xs,ys,zs) -> rev#(xs,ys)
    rev#(xs,ys) -> append#(ys,last(xs)) ->
    append#(cons(x,xs),ys) -> append#(xs,ys)
    rev#(xs,ys) -> dropLast#(xs) ->
    dropLast#(cons(x,cons(y,ys))) -> dropLast#(cons(y,ys))
    rev#(xs,ys) -> last#(xs) ->
    last#(cons(x,cons(y,ys))) -> last#(cons(y,ys))
    reverse#(xs) -> rev#(xs,nil()) ->
    rev#(xs,ys) -> if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
    reverse#(xs) -> rev#(xs,nil()) -> rev#(xs,ys) -> isEmpty#(xs)
    reverse#(xs) -> rev#(xs,nil()) -> rev#(xs,ys) -> dropLast#(xs)
    reverse#(xs) -> rev#(xs,nil()) ->
    rev#(xs,ys) -> append#(ys,last(xs))
    reverse#(xs) -> rev#(xs,nil()) ->
    rev#(xs,ys) -> last#(xs)
    append#(cons(x,xs),ys) -> append#(xs,ys) ->
    append#(cons(x,xs),ys) -> append#(xs,ys)
    dropLast#(cons(x,cons(y,ys))) -> dropLast#(cons(y,ys)) ->
    dropLast#(cons(x,cons(y,ys))) -> dropLast#(cons(y,ys))
    last#(cons(x,cons(y,ys))) -> last#(cons(y,ys)) ->
    last#(cons(x,cons(y,ys))) -> last#(cons(y,ys))
   SCC Processor:
    #sccs: 4
    #rules: 5
    #arcs: 17/100
    DPs:
     if#(false(),xs,ys,zs) -> rev#(xs,ys)
     rev#(xs,ys) -> if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
    TRS:
     isEmpty(nil()) -> true()
     isEmpty(cons(x,xs)) -> false()
     last(cons(x,nil())) -> x
     last(cons(x,cons(y,ys))) -> last(cons(y,ys))
     dropLast(nil()) -> nil()
     dropLast(cons(x,nil())) -> nil()
     dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
     append(nil(),ys) -> ys
     append(cons(x,xs),ys) -> cons(x,append(xs,ys))
     reverse(xs) -> rev(xs,nil())
     rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
     if(true(),xs,ys,zs) -> zs
     if(false(),xs,ys,zs) -> rev(xs,ys)
    Open
    
    DPs:
     dropLast#(cons(x,cons(y,ys))) -> dropLast#(cons(y,ys))
    TRS:
     isEmpty(nil()) -> true()
     isEmpty(cons(x,xs)) -> false()
     last(cons(x,nil())) -> x
     last(cons(x,cons(y,ys))) -> last(cons(y,ys))
     dropLast(nil()) -> nil()
     dropLast(cons(x,nil())) -> nil()
     dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
     append(nil(),ys) -> ys
     append(cons(x,xs),ys) -> cons(x,append(xs,ys))
     reverse(xs) -> rev(xs,nil())
     rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
     if(true(),xs,ys,zs) -> zs
     if(false(),xs,ys,zs) -> rev(xs,ys)
    Subterm Criterion Processor:
     simple projection:
      pi(dropLast#) = 0
     problem:
      DPs:
       
      TRS:
       isEmpty(nil()) -> true()
       isEmpty(cons(x,xs)) -> false()
       last(cons(x,nil())) -> x
       last(cons(x,cons(y,ys))) -> last(cons(y,ys))
       dropLast(nil()) -> nil()
       dropLast(cons(x,nil())) -> nil()
       dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
       append(nil(),ys) -> ys
       append(cons(x,xs),ys) -> cons(x,append(xs,ys))
       reverse(xs) -> rev(xs,nil())
       rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
       if(true(),xs,ys,zs) -> zs
       if(false(),xs,ys,zs) -> rev(xs,ys)
     Qed
    
    DPs:
     append#(cons(x,xs),ys) -> append#(xs,ys)
    TRS:
     isEmpty(nil()) -> true()
     isEmpty(cons(x,xs)) -> false()
     last(cons(x,nil())) -> x
     last(cons(x,cons(y,ys))) -> last(cons(y,ys))
     dropLast(nil()) -> nil()
     dropLast(cons(x,nil())) -> nil()
     dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
     append(nil(),ys) -> ys
     append(cons(x,xs),ys) -> cons(x,append(xs,ys))
     reverse(xs) -> rev(xs,nil())
     rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
     if(true(),xs,ys,zs) -> zs
     if(false(),xs,ys,zs) -> rev(xs,ys)
    Subterm Criterion Processor:
     simple projection:
      pi(append#) = 0
     problem:
      DPs:
       
      TRS:
       isEmpty(nil()) -> true()
       isEmpty(cons(x,xs)) -> false()
       last(cons(x,nil())) -> x
       last(cons(x,cons(y,ys))) -> last(cons(y,ys))
       dropLast(nil()) -> nil()
       dropLast(cons(x,nil())) -> nil()
       dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
       append(nil(),ys) -> ys
       append(cons(x,xs),ys) -> cons(x,append(xs,ys))
       reverse(xs) -> rev(xs,nil())
       rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
       if(true(),xs,ys,zs) -> zs
       if(false(),xs,ys,zs) -> rev(xs,ys)
     Qed
    
    DPs:
     last#(cons(x,cons(y,ys))) -> last#(cons(y,ys))
    TRS:
     isEmpty(nil()) -> true()
     isEmpty(cons(x,xs)) -> false()
     last(cons(x,nil())) -> x
     last(cons(x,cons(y,ys))) -> last(cons(y,ys))
     dropLast(nil()) -> nil()
     dropLast(cons(x,nil())) -> nil()
     dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
     append(nil(),ys) -> ys
     append(cons(x,xs),ys) -> cons(x,append(xs,ys))
     reverse(xs) -> rev(xs,nil())
     rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
     if(true(),xs,ys,zs) -> zs
     if(false(),xs,ys,zs) -> rev(xs,ys)
    Subterm Criterion Processor:
     simple projection:
      pi(last#) = 0
     problem:
      DPs:
       
      TRS:
       isEmpty(nil()) -> true()
       isEmpty(cons(x,xs)) -> false()
       last(cons(x,nil())) -> x
       last(cons(x,cons(y,ys))) -> last(cons(y,ys))
       dropLast(nil()) -> nil()
       dropLast(cons(x,nil())) -> nil()
       dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
       append(nil(),ys) -> ys
       append(cons(x,xs),ys) -> cons(x,append(xs,ys))
       reverse(xs) -> rev(xs,nil())
       rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
       if(true(),xs,ys,zs) -> zs
       if(false(),xs,ys,zs) -> rev(xs,ys)
     Qed