MAYBE

Problem:
 length(nil()) -> 0()
 length(cons(x,l)) -> s(length(l))
 lt(x,0()) -> false()
 lt(0(),s(y)) -> true()
 lt(s(x),s(y)) -> lt(x,y)
 head(cons(x,l)) -> x
 head(nil()) -> undefined()
 tail(nil()) -> nil()
 tail(cons(x,l)) -> l
 reverse(l) -> rev(0(),l,nil(),l)
 rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
 if(true(),x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
 if(false(),x,l,accu,orig) -> accu

Proof:
 DP Processor:
  DPs:
   length#(cons(x,l)) -> length#(l)
   lt#(s(x),s(y)) -> lt#(x,y)
   reverse#(l) -> rev#(0(),l,nil(),l)
   rev#(x,l,accu,orig) -> length#(orig)
   rev#(x,l,accu,orig) -> lt#(x,length(orig))
   rev#(x,l,accu,orig) -> if#(lt(x,length(orig)),x,l,accu,orig)
   if#(true(),x,l,accu,orig) -> head#(l)
   if#(true(),x,l,accu,orig) -> tail#(l)
   if#(true(),x,l,accu,orig) -> rev#(s(x),tail(l),cons(head(l),accu),orig)
  TRS:
   length(nil()) -> 0()
   length(cons(x,l)) -> s(length(l))
   lt(x,0()) -> false()
   lt(0(),s(y)) -> true()
   lt(s(x),s(y)) -> lt(x,y)
   head(cons(x,l)) -> x
   head(nil()) -> undefined()
   tail(nil()) -> nil()
   tail(cons(x,l)) -> l
   reverse(l) -> rev(0(),l,nil(),l)
   rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
   if(true(),x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
   if(false(),x,l,accu,orig) -> accu
  TDG Processor:
   DPs:
    length#(cons(x,l)) -> length#(l)
    lt#(s(x),s(y)) -> lt#(x,y)
    reverse#(l) -> rev#(0(),l,nil(),l)
    rev#(x,l,accu,orig) -> length#(orig)
    rev#(x,l,accu,orig) -> lt#(x,length(orig))
    rev#(x,l,accu,orig) -> if#(lt(x,length(orig)),x,l,accu,orig)
    if#(true(),x,l,accu,orig) -> head#(l)
    if#(true(),x,l,accu,orig) -> tail#(l)
    if#(true(),x,l,accu,orig) -> rev#(s(x),tail(l),cons(head(l),accu),orig)
   TRS:
    length(nil()) -> 0()
    length(cons(x,l)) -> s(length(l))
    lt(x,0()) -> false()
    lt(0(),s(y)) -> true()
    lt(s(x),s(y)) -> lt(x,y)
    head(cons(x,l)) -> x
    head(nil()) -> undefined()
    tail(nil()) -> nil()
    tail(cons(x,l)) -> l
    reverse(l) -> rev(0(),l,nil(),l)
    rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
    if(true(),x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
    if(false(),x,l,accu,orig) -> accu
   graph:
    if#(true(),x,l,accu,orig) -> rev#(s(x),tail(l),cons(head(l),accu),orig) ->
    rev#(x,l,accu,orig) -> if#(lt(x,length(orig)),x,l,accu,orig)
    if#(true(),x,l,accu,orig) -> rev#(s(x),tail(l),cons(head(l),accu),orig) ->
    rev#(x,l,accu,orig) -> lt#(x,length(orig))
    if#(true(),x,l,accu,orig) -> rev#(s(x),tail(l),cons(head(l),accu),orig) ->
    rev#(x,l,accu,orig) -> length#(orig)
    rev#(x,l,accu,orig) -> if#(lt(x,length(orig)),x,l,accu,orig) ->
    if#(true(),x,l,accu,orig) -> rev#(s(x),tail(l),cons(head(l),accu),orig)
    rev#(x,l,accu,orig) -> if#(lt(x,length(orig)),x,l,accu,orig) ->
    if#(true(),x,l,accu,orig) -> tail#(l)
    rev#(x,l,accu,orig) -> if#(lt(x,length(orig)),x,l,accu,orig) ->
    if#(true(),x,l,accu,orig) -> head#(l)
    rev#(x,l,accu,orig) -> lt#(x,length(orig)) ->
    lt#(s(x),s(y)) -> lt#(x,y)
    rev#(x,l,accu,orig) -> length#(orig) ->
    length#(cons(x,l)) -> length#(l)
    reverse#(l) -> rev#(0(),l,nil(),l) ->
    rev#(x,l,accu,orig) -> if#(lt(x,length(orig)),x,l,accu,orig)
    reverse#(l) -> rev#(0(),l,nil(),l) ->
    rev#(x,l,accu,orig) -> lt#(x,length(orig))
    reverse#(l) -> rev#(0(),l,nil(),l) ->
    rev#(x,l,accu,orig) -> length#(orig)
    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
    length#(cons(x,l)) -> length#(l) -> length#(cons(x,l)) -> length#(l)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 13/81
    DPs:
     if#(true(),x,l,accu,orig) -> rev#(s(x),tail(l),cons(head(l),accu),orig)
     rev#(x,l,accu,orig) -> if#(lt(x,length(orig)),x,l,accu,orig)
    TRS:
     length(nil()) -> 0()
     length(cons(x,l)) -> s(length(l))
     lt(x,0()) -> false()
     lt(0(),s(y)) -> true()
     lt(s(x),s(y)) -> lt(x,y)
     head(cons(x,l)) -> x
     head(nil()) -> undefined()
     tail(nil()) -> nil()
     tail(cons(x,l)) -> l
     reverse(l) -> rev(0(),l,nil(),l)
     rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
     if(true(),x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
     if(false(),x,l,accu,orig) -> accu
    Open
    
    DPs:
     lt#(s(x),s(y)) -> lt#(x,y)
    TRS:
     length(nil()) -> 0()
     length(cons(x,l)) -> s(length(l))
     lt(x,0()) -> false()
     lt(0(),s(y)) -> true()
     lt(s(x),s(y)) -> lt(x,y)
     head(cons(x,l)) -> x
     head(nil()) -> undefined()
     tail(nil()) -> nil()
     tail(cons(x,l)) -> l
     reverse(l) -> rev(0(),l,nil(),l)
     rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
     if(true(),x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
     if(false(),x,l,accu,orig) -> accu
    Subterm Criterion Processor:
     simple projection:
      pi(lt#) = 1
     problem:
      DPs:
       
      TRS:
       length(nil()) -> 0()
       length(cons(x,l)) -> s(length(l))
       lt(x,0()) -> false()
       lt(0(),s(y)) -> true()
       lt(s(x),s(y)) -> lt(x,y)
       head(cons(x,l)) -> x
       head(nil()) -> undefined()
       tail(nil()) -> nil()
       tail(cons(x,l)) -> l
       reverse(l) -> rev(0(),l,nil(),l)
       rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
       if(true(),x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
       if(false(),x,l,accu,orig) -> accu
     Qed
    
    DPs:
     length#(cons(x,l)) -> length#(l)
    TRS:
     length(nil()) -> 0()
     length(cons(x,l)) -> s(length(l))
     lt(x,0()) -> false()
     lt(0(),s(y)) -> true()
     lt(s(x),s(y)) -> lt(x,y)
     head(cons(x,l)) -> x
     head(nil()) -> undefined()
     tail(nil()) -> nil()
     tail(cons(x,l)) -> l
     reverse(l) -> rev(0(),l,nil(),l)
     rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
     if(true(),x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
     if(false(),x,l,accu,orig) -> accu
    Subterm Criterion Processor:
     simple projection:
      pi(length#) = 0
     problem:
      DPs:
       
      TRS:
       length(nil()) -> 0()
       length(cons(x,l)) -> s(length(l))
       lt(x,0()) -> false()
       lt(0(),s(y)) -> true()
       lt(s(x),s(y)) -> lt(x,y)
       head(cons(x,l)) -> x
       head(nil()) -> undefined()
       tail(nil()) -> nil()
       tail(cons(x,l)) -> l
       reverse(l) -> rev(0(),l,nil(),l)
       rev(x,l,accu,orig) -> if(lt(x,length(orig)),x,l,accu,orig)
       if(true(),x,l,accu,orig) -> rev(s(x),tail(l),cons(head(l),accu),orig)
       if(false(),x,l,accu,orig) -> accu
     Qed