MAYBE
Time: 0.050637
TRS:
 {            nats() -> cons(0(), n__incr nats()),
              odds() -> incr pairs(),
             pairs() -> cons(0(), n__incr odds()),
              incr X -> n__incr X,
    incr cons(X, XS) -> cons(s X, n__incr activate XS),
          activate X -> X,
  activate n__incr X -> incr X,
    head cons(X, XS) -> X,
    tail cons(X, XS) -> activate XS}
 DP:
  DP:
   {            nats#() -> nats#(),
                odds#() -> pairs#(),
                odds#() -> incr# pairs(),
               pairs#() -> odds#(),
      incr# cons(X, XS) -> activate# XS,
    activate# n__incr X -> incr# X,
      tail# cons(X, XS) -> activate# XS}
  TRS:
  {            nats() -> cons(0(), n__incr nats()),
               odds() -> incr pairs(),
              pairs() -> cons(0(), n__incr odds()),
               incr X -> n__incr X,
     incr cons(X, XS) -> cons(s X, n__incr activate XS),
           activate X -> X,
   activate n__incr X -> incr X,
     head cons(X, XS) -> X,
     tail cons(X, XS) -> activate XS}
  UR:
   {            odds() -> incr pairs(),
               pairs() -> cons(0(), n__incr odds()),
                incr X -> n__incr X,
      incr cons(X, XS) -> cons(s X, n__incr activate XS),
            activate X -> X,
    activate n__incr X -> incr X}
   EDG:
    {(tail# cons(X, XS) -> activate# XS, activate# n__incr X -> incr# X)
     (odds#() -> pairs#(), pairs#() -> odds#())
     (activate# n__incr X -> incr# X, incr# cons(X, XS) -> activate# XS)
     (odds#() -> incr# pairs(), incr# cons(X, XS) -> activate# XS)
     (pairs#() -> odds#(), odds#() -> pairs#())
     (pairs#() -> odds#(), odds#() -> incr# pairs())
     (nats#() -> nats#(), nats#() -> nats#())
     (incr# cons(X, XS) -> activate# XS, activate# n__incr X -> incr# X)}
    STATUS:
     arrows: 0.836735
     SCCS (3):
      Scc:
       { odds#() -> pairs#(),
        pairs#() -> odds#()}
      Scc:
       {nats#() -> nats#()}
      Scc:
       {  incr# cons(X, XS) -> activate# XS,
        activate# n__incr X -> incr# X}
      
      SCC (2):
       Strict:
        { odds#() -> pairs#(),
         pairs#() -> odds#()}
       Weak:
       {            nats() -> cons(0(), n__incr nats()),
                    odds() -> incr pairs(),
                   pairs() -> cons(0(), n__incr odds()),
                    incr X -> n__incr X,
          incr cons(X, XS) -> cons(s X, n__incr activate XS),
                activate X -> X,
        activate n__incr X -> incr X,
          head cons(X, XS) -> X,
          tail cons(X, XS) -> activate XS}
       Fail
      
      SCC (1):
       Strict:
        {nats#() -> nats#()}
       Weak:
       {            nats() -> cons(0(), n__incr nats()),
                    odds() -> incr pairs(),
                   pairs() -> cons(0(), n__incr odds()),
                    incr X -> n__incr X,
          incr cons(X, XS) -> cons(s X, n__incr activate XS),
                activate X -> X,
        activate n__incr X -> incr X,
          head cons(X, XS) -> X,
          tail cons(X, XS) -> activate XS}
       Fail
      
      SCC (2):
       Strict:
        {  incr# cons(X, XS) -> activate# XS,
         activate# n__incr X -> incr# X}
       Weak:
       {            nats() -> cons(0(), n__incr nats()),
                    odds() -> incr pairs(),
                   pairs() -> cons(0(), n__incr odds()),
                    incr X -> n__incr X,
          incr cons(X, XS) -> cons(s X, n__incr activate XS),
                activate X -> X,
        activate n__incr X -> incr X,
          head cons(X, XS) -> X,
          tail cons(X, XS) -> activate XS}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = x0 + x1 + 1,
         
         [n__incr](x0) = x0 + 1,
         
         [incr](x0) = x0 + 1,
         
         [s](x0) = 1,
         
         [activate](x0) = x0 + 1,
         
         [head](x0) = 0,
         
         [tail](x0) = 0,
         
         [0] = 1,
         
         [nats] = 1,
         
         [odds] = 1,
         
         [pairs] = 1,
         
         [incr#](x0) = x0 + 1,
         
         [activate#](x0) = x0 + 1
        Strict:
         activate# n__incr X -> incr# X
         2 + 1X >= 1 + 1X
         incr# cons(X, XS) -> activate# XS
         2 + 1X + 1XS >= 1 + 1XS
        Weak:
         tail cons(X, XS) -> activate XS
         0 + 0X + 0XS >= 1 + 1XS
         head cons(X, XS) -> X
         0 + 0X + 0XS >= 1X
         activate n__incr X -> incr X
         2 + 1X >= 1 + 1X
         activate X -> X
         1 + 1X >= 1X
         incr cons(X, XS) -> cons(s X, n__incr activate XS)
         2 + 1X + 1XS >= 4 + 0X + 1XS
         incr X -> n__incr X
         1 + 1X >= 1 + 1X
         pairs() -> cons(0(), n__incr odds())
         1 >= 4
         odds() -> incr pairs()
         1 >= 2
         nats() -> cons(0(), n__incr nats())
         1 >= 4
       Qed