MAYBE
TRS:
 {     incr(nil()) -> nil(),
  incr(cons(X, L)) -> cons(s(X), incr(L)),
        adx(nil()) -> nil(),
   adx(cons(X, L)) -> incr(cons(X, adx(L))),
           zeros() -> cons(0(), zeros()),
            nats() -> adx(zeros()),
  head(cons(X, L)) -> X,
  tail(cons(X, L)) -> L}
 RUF:
  Strict:
   {     incr(nil()) -> nil(),
    incr(cons(X, L)) -> cons(s(X), incr(L)),
          adx(nil()) -> nil(),
     adx(cons(X, L)) -> incr(cons(X, adx(L))),
             zeros() -> cons(0(), zeros())}
  Weak:
   {}
  DP:
   Strict:
    {incr#(cons(X, L)) -> incr#(L),
      adx#(cons(X, L)) -> incr#(cons(X, adx(L))),
      adx#(cons(X, L)) -> adx#(L),
              zeros#() -> zeros#()}
   Weak:
   {     incr(nil()) -> nil(),
    incr(cons(X, L)) -> cons(s(X), incr(L)),
          adx(nil()) -> nil(),
     adx(cons(X, L)) -> incr(cons(X, adx(L))),
             zeros() -> cons(0(), zeros())}
   EDG:
    {(adx#(cons(X, L)) -> incr#(cons(X, adx(L))), incr#(cons(X, L)) -> incr#(L))
     (adx#(cons(X, L)) -> adx#(L), adx#(cons(X, L)) -> adx#(L))
     (adx#(cons(X, L)) -> adx#(L), adx#(cons(X, L)) -> incr#(cons(X, adx(L))))
     (incr#(cons(X, L)) -> incr#(L), incr#(cons(X, L)) -> incr#(L))
     (zeros#() -> zeros#(), zeros#() -> zeros#())}
    SCCS:
     Scc:
      {zeros#() -> zeros#()}
     Scc:
      {adx#(cons(X, L)) -> adx#(L)}
     Scc:
      {incr#(cons(X, L)) -> incr#(L)}
     SCC:
      Strict:
       {zeros#() -> zeros#()}
      Weak:
      {     incr(nil()) -> nil(),
       incr(cons(X, L)) -> cons(s(X), incr(L)),
             adx(nil()) -> nil(),
        adx(cons(X, L)) -> incr(cons(X, adx(L))),
                zeros() -> cons(0(), zeros())}
      Fail
     SCC:
      Strict:
       {adx#(cons(X, L)) -> adx#(L)}
      Weak:
      {     incr(nil()) -> nil(),
       incr(cons(X, L)) -> cons(s(X), incr(L)),
             adx(nil()) -> nil(),
        adx(cons(X, L)) -> incr(cons(X, adx(L))),
                zeros() -> cons(0(), zeros())}
      SPSC:
       Simple Projection:
        pi(adx#) = 0
       Strict:
        {}
       Qed
     SCC:
      Strict:
       {incr#(cons(X, L)) -> incr#(L)}
      Weak:
      {     incr(nil()) -> nil(),
       incr(cons(X, L)) -> cons(s(X), incr(L)),
             adx(nil()) -> nil(),
        adx(cons(X, L)) -> incr(cons(X, adx(L))),
                zeros() -> cons(0(), zeros())}
      SPSC:
       Simple Projection:
        pi(incr#) = 0
       Strict:
        {}
       Qed