MAYBE
Time: 0.000848
TRS:
 { adx cons(X, Y) -> incr cons(X, adx Y),
          zeros() -> cons(0(), zeros()),
           nats() -> adx zeros(),
  incr cons(X, Y) -> cons(s X, incr Y),
    hd cons(X, Y) -> X,
    tl cons(X, Y) -> Y}
 DP:
  DP:
   { adx# cons(X, Y) -> adx# Y,
     adx# cons(X, Y) -> incr# cons(X, adx Y),
            zeros#() -> zeros#(),
             nats#() -> adx# zeros(),
             nats#() -> zeros#(),
    incr# cons(X, Y) -> incr# Y}
  TRS:
  { adx cons(X, Y) -> incr cons(X, adx Y),
           zeros() -> cons(0(), zeros()),
            nats() -> adx zeros(),
   incr cons(X, Y) -> cons(s X, incr Y),
     hd cons(X, Y) -> X,
     tl cons(X, Y) -> Y}
  EDG:
   {(incr# cons(X, Y) -> incr# Y, incr# cons(X, Y) -> incr# Y)
    (nats#() -> adx# zeros(), adx# cons(X, Y) -> incr# cons(X, adx Y))
    (nats#() -> adx# zeros(), adx# cons(X, Y) -> adx# Y)
    (nats#() -> zeros#(), zeros#() -> zeros#())
    (zeros#() -> zeros#(), zeros#() -> zeros#())
    (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))}
   STATUS:
    arrows: 0.777778
    SCCS (3):
     Scc:
      {zeros#() -> zeros#()}
     Scc:
      {adx# cons(X, Y) -> adx# Y}
     Scc:
      {incr# cons(X, Y) -> incr# Y}
     
     
     SCC (1):
      Strict:
       {zeros#() -> zeros#()}
      Weak:
      { adx cons(X, Y) -> incr cons(X, adx Y),
               zeros() -> cons(0(), zeros()),
                nats() -> adx zeros(),
       incr cons(X, Y) -> cons(s X, incr Y),
         hd cons(X, Y) -> X,
         tl cons(X, Y) -> Y}
      Open
     
     SCC (1):
      Strict:
       {adx# cons(X, Y) -> adx# Y}
      Weak:
      { adx cons(X, Y) -> incr cons(X, adx Y),
               zeros() -> cons(0(), zeros()),
                nats() -> adx zeros(),
       incr cons(X, Y) -> cons(s X, incr Y),
         hd cons(X, Y) -> X,
         tl cons(X, Y) -> Y}
      Open
     
     SCC (1):
      Strict:
       {incr# cons(X, Y) -> incr# Y}
      Weak:
      { adx cons(X, Y) -> incr cons(X, adx Y),
               zeros() -> cons(0(), zeros()),
                nats() -> adx zeros(),
       incr cons(X, Y) -> cons(s X, incr Y),
         hd cons(X, Y) -> X,
         tl cons(X, Y) -> Y}
      Open