MAYBE

Problem:
 nats() -> adx(zeros())
 zeros() -> cons(0(),zeros())
 incr(cons(X,Y)) -> cons(s(X),incr(Y))
 adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
 hd(cons(X,Y)) -> X
 tl(cons(X,Y)) -> Y

Proof:
 DP Processor:
  DPs:
   nats#() -> zeros#()
   nats#() -> adx#(zeros())
   zeros#() -> zeros#()
   incr#(cons(X,Y)) -> incr#(Y)
   adx#(cons(X,Y)) -> adx#(Y)
   adx#(cons(X,Y)) -> incr#(cons(X,adx(Y)))
  TRS:
   nats() -> adx(zeros())
   zeros() -> cons(0(),zeros())
   incr(cons(X,Y)) -> cons(s(X),incr(Y))
   adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
   hd(cons(X,Y)) -> X
   tl(cons(X,Y)) -> Y
  EDG Processor:
   DPs:
    nats#() -> zeros#()
    nats#() -> adx#(zeros())
    zeros#() -> zeros#()
    incr#(cons(X,Y)) -> incr#(Y)
    adx#(cons(X,Y)) -> adx#(Y)
    adx#(cons(X,Y)) -> incr#(cons(X,adx(Y)))
   TRS:
    nats() -> adx(zeros())
    zeros() -> cons(0(),zeros())
    incr(cons(X,Y)) -> cons(s(X),incr(Y))
    adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
    hd(cons(X,Y)) -> X
    tl(cons(X,Y)) -> Y
   graph:
    incr#(cons(X,Y)) -> incr#(Y) ->
    incr#(cons(X,Y)) -> incr#(Y)
    adx#(cons(X,Y)) -> incr#(cons(X,adx(Y))) ->
    incr#(cons(X,Y)) -> incr#(Y)
    adx#(cons(X,Y)) -> adx#(Y) -> adx#(cons(X,Y)) -> adx#(Y)
    adx#(cons(X,Y)) -> adx#(Y) -> adx#(cons(X,Y)) -> incr#(cons(X,adx(Y)))
    zeros#() -> zeros#() -> zeros#() -> zeros#()
    nats#() -> adx#(zeros()) -> adx#(cons(X,Y)) -> adx#(Y)
    nats#() -> adx#(zeros()) -> adx#(cons(X,Y)) -> incr#(cons(X,adx(Y)))
    nats#() -> zeros#() -> zeros#() -> zeros#()
   SCC Processor:
    #sccs: 3
    #rules: 3
    #arcs: 8/36
    DPs:
     zeros#() -> zeros#()
    TRS:
     nats() -> adx(zeros())
     zeros() -> cons(0(),zeros())
     incr(cons(X,Y)) -> cons(s(X),incr(Y))
     adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
     hd(cons(X,Y)) -> X
     tl(cons(X,Y)) -> Y
    Open
    
    DPs:
     adx#(cons(X,Y)) -> adx#(Y)
    TRS:
     nats() -> adx(zeros())
     zeros() -> cons(0(),zeros())
     incr(cons(X,Y)) -> cons(s(X),incr(Y))
     adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
     hd(cons(X,Y)) -> X
     tl(cons(X,Y)) -> Y
    Open
    
    DPs:
     incr#(cons(X,Y)) -> incr#(Y)
    TRS:
     nats() -> adx(zeros())
     zeros() -> cons(0(),zeros())
     incr(cons(X,Y)) -> cons(s(X),incr(Y))
     adx(cons(X,Y)) -> incr(cons(X,adx(Y)))
     hd(cons(X,Y)) -> X
     tl(cons(X,Y)) -> Y
    Open