MAYBE
Time: 26.230802
TRS:
 {       cons(mark X1, X2) -> mark cons(X1, X2),
        cons(ok X1, ok X2) -> ok cons(X1, X2),
               from mark X -> mark from X,
                 from ok X -> ok from X,
                  s mark X -> mark s X,
                    s ok X -> ok s X,
       active cons(X1, X2) -> cons(active X1, X2),
             active from X -> mark cons(X, from s X),
             active from X -> from active X,
                active s X -> s active X,
  active length cons(X, Y) -> mark s length1 Y,
       active length nil() -> mark 0(),
          active length1 X -> mark length X,
               length ok X -> ok length X,
              length1 ok X -> ok length1 X,
       proper cons(X1, X2) -> cons(proper X1, proper X2),
             proper from X -> from proper X,
                proper s X -> s proper X,
                proper 0() -> ok 0(),
           proper length X -> length proper X,
              proper nil() -> ok nil(),
          proper length1 X -> length1 proper X,
                top mark X -> top proper X,
                  top ok X -> top active X}
 DP:
  DP:
   {       cons#(mark X1, X2) -> cons#(X1, X2),
          cons#(ok X1, ok X2) -> cons#(X1, X2),
                 from# mark X -> from# X,
                   from# ok X -> from# X,
                    s# mark X -> s# X,
                      s# ok X -> s# X,
         active# cons(X1, X2) -> cons#(active X1, X2),
         active# cons(X1, X2) -> active# X1,
               active# from X -> cons#(X, from s X),
               active# from X -> from# s X,
               active# from X -> from# active X,
               active# from X -> s# X,
               active# from X -> active# X,
                  active# s X -> s# active X,
                  active# s X -> active# X,
    active# length cons(X, Y) -> s# length1 Y,
    active# length cons(X, Y) -> length1# Y,
            active# length1 X -> length# X,
                 length# ok X -> length# X,
                length1# ok X -> length1# X,
         proper# cons(X1, X2) -> cons#(proper X1, proper X2),
         proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
               proper# from X -> from# proper X,
               proper# from X -> proper# X,
                  proper# s X -> s# proper X,
                  proper# s X -> proper# X,
             proper# length X -> length# proper X,
             proper# length X -> proper# X,
            proper# length1 X -> length1# proper X,
            proper# length1 X -> proper# X,
                  top# mark X -> proper# X,
                  top# mark X -> top# proper X,
                    top# ok X -> active# X,
                    top# ok X -> top# active X}
  TRS:
  {       cons(mark X1, X2) -> mark cons(X1, X2),
         cons(ok X1, ok X2) -> ok cons(X1, X2),
                from mark X -> mark from X,
                  from ok X -> ok from X,
                   s mark X -> mark s X,
                     s ok X -> ok s X,
        active cons(X1, X2) -> cons(active X1, X2),
              active from X -> mark cons(X, from s X),
              active from X -> from active X,
                 active s X -> s active X,
   active length cons(X, Y) -> mark s length1 Y,
        active length nil() -> mark 0(),
           active length1 X -> mark length X,
                length ok X -> ok length X,
               length1 ok X -> ok length1 X,
        proper cons(X1, X2) -> cons(proper X1, proper X2),
              proper from X -> from proper X,
                 proper s X -> s proper X,
                 proper 0() -> ok 0(),
            proper length X -> length proper X,
               proper nil() -> ok nil(),
           proper length1 X -> length1 proper X,
                 top mark X -> top proper X,
                   top ok X -> top active X}
  UR:
   {       cons(mark X1, X2) -> mark cons(X1, X2),
          cons(ok X1, ok X2) -> ok cons(X1, X2),
                 from mark X -> mark from X,
                   from ok X -> ok from X,
                    s mark X -> mark s X,
                      s ok X -> ok s X,
         active cons(X1, X2) -> cons(active X1, X2),
               active from X -> mark cons(X, from s X),
               active from X -> from active X,
                  active s X -> s active X,
    active length cons(X, Y) -> mark s length1 Y,
         active length nil() -> mark 0(),
            active length1 X -> mark length X,
                 length ok X -> ok length X,
                length1 ok X -> ok length1 X,
         proper cons(X1, X2) -> cons(proper X1, proper X2),
               proper from X -> from proper X,
                  proper s X -> s proper X,
                  proper 0() -> ok 0(),
             proper length X -> length proper X,
                proper nil() -> ok nil(),
            proper length1 X -> length1 proper X,
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {
     (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
     (from# ok X -> from# X, from# ok X -> from# X)
     (from# ok X -> from# X, from# mark X -> from# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (s# ok X -> s# X, s# mark X -> s# X)
     (active# from X -> active# X, active# length1 X -> length# X)
     (active# from X -> active# X, active# length cons(X, Y) -> length1# Y)
     (active# from X -> active# X, active# length cons(X, Y) -> s# length1 Y)
     (active# from X -> active# X, active# s X -> active# X)
     (active# from X -> active# X, active# s X -> s# active X)
     (active# from X -> active# X, active# from X -> active# X)
     (active# from X -> active# X, active# from X -> s# X)
     (active# from X -> active# X, active# from X -> from# active X)
     (active# from X -> active# X, active# from X -> from# s X)
     (active# from X -> active# X, active# from X -> cons#(X, from s X))
     (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# length1 X -> length# X, length# ok X -> length# X)
     (length1# ok X -> length1# X, length1# ok X -> length1# X)
     (proper# s X -> proper# X, proper# length1 X -> proper# X)
     (proper# s X -> proper# X, proper# length1 X -> length1# proper X)
     (proper# s X -> proper# X, proper# length X -> proper# X)
     (proper# s X -> proper# X, proper# length X -> length# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# from X -> proper# X)
     (proper# s X -> proper# X, proper# from X -> from# proper X)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# length1 X -> proper# X, proper# length1 X -> proper# X)
     (proper# length1 X -> proper# X, proper# length1 X -> length1# proper X)
     (proper# length1 X -> proper# X, proper# length X -> proper# X)
     (proper# length1 X -> proper# X, proper# length X -> length# proper X)
     (proper# length1 X -> proper# X, proper# s X -> proper# X)
     (proper# length1 X -> proper# X, proper# s X -> s# proper X)
     (proper# length1 X -> proper# X, proper# from X -> proper# X)
     (proper# length1 X -> proper# X, proper# from X -> from# proper X)
     (proper# length1 X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# length1 X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# length1 X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# ok X -> active# X, active# length1 X -> length# X)
     (top# ok X -> active# X, active# length cons(X, Y) -> length1# Y)
     (top# ok X -> active# X, active# length cons(X, Y) -> s# length1 Y)
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# from X -> active# X)
     (top# ok X -> active# X, active# from X -> s# X)
     (top# ok X -> active# X, active# from X -> from# active X)
     (top# ok X -> active# X, active# from X -> from# s X)
     (top# ok X -> active# X, active# from X -> cons#(X, from s X))
     (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (proper# cons(X1, X2) -> proper# X1, proper# length1 X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# length1 X -> length1# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# length X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# length X -> length# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# length cons(X, Y) -> s# length1 Y, s# ok X -> s# X)
     (active# from X -> from# active X, from# ok X -> from# X)
     (active# from X -> from# active X, from# mark X -> from# X)
     (proper# from X -> from# proper X, from# ok X -> from# X)
     (proper# from X -> from# proper X, from# mark X -> from# X)
     (proper# length X -> length# proper X, length# ok X -> length# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (proper# length1 X -> length1# proper X, length1# ok X -> length1# X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (active# s X -> s# active X, s# ok X -> s# X)
     (active# from X -> from# s X, from# mark X -> from# X)
     (active# from X -> from# s X, from# ok X -> from# X)
     (active# length cons(X, Y) -> length1# Y, length1# ok X -> length1# X)
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
     (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# cons(X1, X2) -> active# X1, active# from X -> from# s X)
     (active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
     (active# cons(X1, X2) -> active# X1, active# from X -> s# X)
     (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# length cons(X, Y) -> s# length1 Y)
     (active# cons(X1, X2) -> active# X1, active# length cons(X, Y) -> length1# Y)
     (active# cons(X1, X2) -> active# X1, active# length1 X -> length# X)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# from X -> from# proper X)
     (top# mark X -> proper# X, proper# from X -> proper# X)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# length X -> length# proper X)
     (top# mark X -> proper# X, proper# length X -> proper# X)
     (top# mark X -> proper# X, proper# length1 X -> length1# proper X)
     (top# mark X -> proper# X, proper# length1 X -> proper# X)
     (proper# length X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# length X -> proper# X, proper# from X -> from# proper X)
     (proper# length X -> proper# X, proper# from X -> proper# X)
     (proper# length X -> proper# X, proper# s X -> s# proper X)
     (proper# length X -> proper# X, proper# s X -> proper# X)
     (proper# length X -> proper# X, proper# length X -> length# proper X)
     (proper# length X -> proper# X, proper# length X -> proper# X)
     (proper# length X -> proper# X, proper# length1 X -> length1# proper X)
     (proper# length X -> proper# X, proper# length1 X -> proper# X)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# from X -> from# proper X)
     (proper# from X -> proper# X, proper# from X -> proper# X)
     (proper# from X -> proper# X, proper# s X -> s# proper X)
     (proper# from X -> proper# X, proper# s X -> proper# X)
     (proper# from X -> proper# X, proper# length X -> length# proper X)
     (proper# from X -> proper# X, proper# length X -> proper# X)
     (proper# from X -> proper# X, proper# length1 X -> length1# proper X)
     (proper# from X -> proper# X, proper# length1 X -> proper# X)
     (length# ok X -> length# X, length# ok X -> length# X)
     (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# s X -> active# X, active# from X -> cons#(X, from s X))
     (active# s X -> active# X, active# from X -> from# s X)
     (active# s X -> active# X, active# from X -> from# active X)
     (active# s X -> active# X, active# from X -> s# X)
     (active# s X -> active# X, active# from X -> active# X)
     (active# s X -> active# X, active# s X -> s# active X)
     (active# s X -> active# X, active# s X -> active# X)
     (active# s X -> active# X, active# length cons(X, Y) -> s# length1 Y)
     (active# s X -> active# X, active# length cons(X, Y) -> length1# Y)
     (active# s X -> active# X, active# length1 X -> length# X)
     (active# from X -> s# X, s# mark X -> s# X)
     (active# from X -> s# X, s# ok X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# ok X -> s# X)
     (from# mark X -> from# X, from# mark X -> from# X)
     (from# mark X -> from# X, from# ok X -> from# X)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# length X -> length# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# length X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# length1 X -> length1# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# length1 X -> proper# X)
    }
    STATUS:
     arrows: 0.861224
     SCCS (8):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {active# cons(X1, X2) -> active# X1,
              active# from X -> active# X,
                 active# s X -> active# X}
      Scc:
       {proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
              proper# from X -> proper# X,
                 proper# s X -> proper# X,
            proper# length X -> proper# X,
           proper# length1 X -> proper# X}
      Scc:
       {length1# ok X -> length1# X}
      Scc:
       {length# ok X -> length# X}
      Scc:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      Scc:
       {from# mark X -> from# X,
          from# ok X -> from# X}
      Scc:
       { cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(ok X1, ok X2) -> cons#(X1, X2)}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {       cons(mark X1, X2) -> mark cons(X1, X2),
              cons(ok X1, ok X2) -> ok cons(X1, X2),
                     from mark X -> mark from X,
                       from ok X -> ok from X,
                        s mark X -> mark s X,
                          s ok X -> ok s X,
             active cons(X1, X2) -> cons(active X1, X2),
                   active from X -> mark cons(X, from s X),
                   active from X -> from active X,
                      active s X -> s active X,
        active length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 proper X,
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Fail
      
      
      SCC (3):
       Strict:
        {active# cons(X1, X2) -> active# X1,
               active# from X -> active# X,
                  active# s X -> active# X}
       Weak:
       {       cons(mark X1, X2) -> mark cons(X1, X2),
              cons(ok X1, ok X2) -> ok cons(X1, X2),
                     from mark X -> mark from X,
                       from ok X -> ok from X,
                        s mark X -> mark s X,
                          s ok X -> ok s X,
             active cons(X1, X2) -> cons(active X1, X2),
                   active from X -> mark cons(X, from s X),
                   active from X -> from active X,
                      active s X -> s active X,
        active length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 proper X,
                      top mark X -> top proper X,
                        top ok X -> top active X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = x0 + x1,
         
         [mark](x0) = 0,
         
         [from](x0) = x0,
         
         [s](x0) = x0 + 1,
         
         [active](x0) = 0,
         
         [length](x0) = 0,
         
         [length1](x0) = 1,
         
         [proper](x0) = x0 + 1,
         
         [ok](x0) = x0 + 1,
         
         [top](x0) = 0,
         
         [0] = 1,
         
         [nil] = 1,
         
         [active#](x0) = x0
        Strict:
         active# s X -> active# X
         1 + 1X >= 0 + 1X
         active# from X -> active# X
         0 + 1X >= 0 + 1X
         active# cons(X1, X2) -> active# X1
         0 + 1X1 + 1X2 >= 0 + 1X1
        Weak:
         top ok X -> top active X
         0 + 0X >= 0 + 0X
         top mark X -> top proper X
         0 + 0X >= 0 + 0X
         proper length1 X -> length1 proper X
         2 + 0X >= 1 + 0X
         proper nil() -> ok nil()
         2 >= 2
         proper length X -> length proper X
         1 + 0X >= 0 + 0X
         proper 0() -> ok 0()
         2 >= 2
         proper s X -> s proper X
         2 + 1X >= 2 + 1X
         proper from X -> from proper X
         1 + 1X >= 1 + 1X
         proper cons(X1, X2) -> cons(proper X1, proper X2)
         1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
         length1 ok X -> ok length1 X
         1 + 0X >= 2 + 0X
         length ok X -> ok length X
         0 + 0X >= 1 + 0X
         active length1 X -> mark length X
         0 + 0X >= 0 + 0X
         active length nil() -> mark 0()
         0 >= 0
         active length cons(X, Y) -> mark s length1 Y
         0 + 0X + 0Y >= 0 + 0Y
         active s X -> s active X
         0 + 0X >= 1 + 0X
         active from X -> from active X
         0 + 0X >= 0 + 0X
         active from X -> mark cons(X, from s X)
         0 + 0X >= 0 + 0X
         active cons(X1, X2) -> cons(active X1, X2)
         0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
         s ok X -> ok s X
         2 + 1X >= 2 + 1X
         s mark X -> mark s X
         1 + 0X >= 0 + 0X
         from ok X -> ok from X
         1 + 1X >= 1 + 1X
         from mark X -> mark from X
         0 + 0X >= 0 + 0X
         cons(ok X1, ok X2) -> ok cons(X1, X2)
         2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
         cons(mark X1, X2) -> mark cons(X1, X2)
         0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
       SCCS (1):
        Scc:
         {active# cons(X1, X2) -> active# X1,
                active# from X -> active# X}
        
        SCC (2):
         Strict:
          {active# cons(X1, X2) -> active# X1,
                 active# from X -> active# X}
         Weak:
         {       cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
          active length cons(X, Y) -> mark s length1 Y,
               active length nil() -> mark 0(),
                  active length1 X -> mark length X,
                       length ok X -> ok length X,
                      length1 ok X -> ok length1 X,
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                   proper length X -> length proper X,
                      proper nil() -> ok nil(),
                  proper length1 X -> length1 proper X,
                        top mark X -> top proper X,
                          top ok X -> top active X}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [cons](x0, x1) = x0 + x1,
           
           [mark](x0) = 0,
           
           [from](x0) = x0 + 1,
           
           [s](x0) = x0 + 1,
           
           [active](x0) = 0,
           
           [length](x0) = 0,
           
           [length1](x0) = 1,
           
           [proper](x0) = x0 + 1,
           
           [ok](x0) = x0 + 1,
           
           [top](x0) = 0,
           
           [0] = 1,
           
           [nil] = 1,
           
           [active#](x0) = x0
          Strict:
           active# from X -> active# X
           1 + 1X >= 0 + 1X
           active# cons(X1, X2) -> active# X1
           0 + 1X1 + 1X2 >= 0 + 1X1
          Weak:
           top ok X -> top active X
           0 + 0X >= 0 + 0X
           top mark X -> top proper X
           0 + 0X >= 0 + 0X
           proper length1 X -> length1 proper X
           2 + 0X >= 1 + 0X
           proper nil() -> ok nil()
           2 >= 2
           proper length X -> length proper X
           1 + 0X >= 0 + 0X
           proper 0() -> ok 0()
           2 >= 2
           proper s X -> s proper X
           2 + 1X >= 2 + 1X
           proper from X -> from proper X
           2 + 1X >= 2 + 1X
           proper cons(X1, X2) -> cons(proper X1, proper X2)
           1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
           length1 ok X -> ok length1 X
           1 + 0X >= 2 + 0X
           length ok X -> ok length X
           0 + 0X >= 1 + 0X
           active length1 X -> mark length X
           0 + 0X >= 0 + 0X
           active length nil() -> mark 0()
           0 >= 0
           active length cons(X, Y) -> mark s length1 Y
           0 + 0X + 0Y >= 0 + 0Y
           active s X -> s active X
           0 + 0X >= 1 + 0X
           active from X -> from active X
           0 + 0X >= 1 + 0X
           active from X -> mark cons(X, from s X)
           0 + 0X >= 0 + 0X
           active cons(X1, X2) -> cons(active X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
           s ok X -> ok s X
           2 + 1X >= 2 + 1X
           s mark X -> mark s X
           1 + 0X >= 0 + 0X
           from ok X -> ok from X
           2 + 1X >= 2 + 1X
           from mark X -> mark from X
           1 + 0X >= 0 + 0X
           cons(ok X1, ok X2) -> ok cons(X1, X2)
           2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
           cons(mark X1, X2) -> mark cons(X1, X2)
           0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
         SCCS (1):
          Scc:
           {active# cons(X1, X2) -> active# X1}
          
          SCC (1):
           Strict:
            {active# cons(X1, X2) -> active# X1}
           Weak:
           {       cons(mark X1, X2) -> mark cons(X1, X2),
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                         from mark X -> mark from X,
                           from ok X -> ok from X,
                            s mark X -> mark s X,
                              s ok X -> ok s X,
                 active cons(X1, X2) -> cons(active X1, X2),
                       active from X -> mark cons(X, from s X),
                       active from X -> from active X,
                          active s X -> s active X,
            active length cons(X, Y) -> mark s length1 Y,
                 active length nil() -> mark 0(),
                    active length1 X -> mark length X,
                         length ok X -> ok length X,
                        length1 ok X -> ok length1 X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                       proper from X -> from proper X,
                          proper s X -> s proper X,
                          proper 0() -> ok 0(),
                     proper length X -> length proper X,
                        proper nil() -> ok nil(),
                    proper length1 X -> length1 proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [cons](x0, x1) = x0 + 1,
             
             [mark](x0) = x0 + 1,
             
             [from](x0) = x0 + 1,
             
             [s](x0) = x0 + 1,
             
             [active](x0) = x0 + 1,
             
             [length](x0) = 1,
             
             [length1](x0) = 1,
             
             [proper](x0) = x0 + 1,
             
             [ok](x0) = x0 + 1,
             
             [top](x0) = x0 + 1,
             
             [0] = 1,
             
             [nil] = 1,
             
             [active#](x0) = x0
            Strict:
             active# cons(X1, X2) -> active# X1
             1 + 1X1 + 0X2 >= 0 + 1X1
            Weak:
             top ok X -> top active X
             2 + 1X >= 2 + 1X
             top mark X -> top proper X
             2 + 1X >= 2 + 1X
             proper length1 X -> length1 proper X
             2 + 0X >= 1 + 0X
             proper nil() -> ok nil()
             2 >= 2
             proper length X -> length proper X
             2 + 0X >= 1 + 0X
             proper 0() -> ok 0()
             2 >= 2
             proper s X -> s proper X
             2 + 1X >= 2 + 1X
             proper from X -> from proper X
             2 + 1X >= 2 + 1X
             proper cons(X1, X2) -> cons(proper X1, proper X2)
             2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
             length1 ok X -> ok length1 X
             1 + 0X >= 2 + 0X
             length ok X -> ok length X
             1 + 0X >= 2 + 0X
             active length1 X -> mark length X
             2 + 0X >= 2 + 0X
             active length nil() -> mark 0()
             2 >= 2
             active length cons(X, Y) -> mark s length1 Y
             2 + 0X + 0Y >= 3 + 0Y
             active s X -> s active X
             2 + 1X >= 2 + 1X
             active from X -> from active X
             2 + 1X >= 2 + 1X
             active from X -> mark cons(X, from s X)
             2 + 1X >= 2 + 1X
             active cons(X1, X2) -> cons(active X1, X2)
             2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
             s ok X -> ok s X
             2 + 1X >= 2 + 1X
             s mark X -> mark s X
             2 + 1X >= 2 + 1X
             from ok X -> ok from X
             2 + 1X >= 2 + 1X
             from mark X -> mark from X
             2 + 1X >= 2 + 1X
             cons(ok X1, ok X2) -> ok cons(X1, X2)
             2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
             cons(mark X1, X2) -> mark cons(X1, X2)
             2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
           Qed
    
    
    
    
    
    
    
    
    
    SCC (6):
     Strict:
      {proper# cons(X1, X2) -> proper# X1,
       proper# cons(X1, X2) -> proper# X2,
             proper# from X -> proper# X,
                proper# s X -> proper# X,
           proper# length X -> proper# X,
          proper# length1 X -> proper# X}
     Weak:
     {       cons(mark X1, X2) -> mark cons(X1, X2),
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                   from mark X -> mark from X,
                     from ok X -> ok from X,
                      s mark X -> mark s X,
                        s ok X -> ok s X,
           active cons(X1, X2) -> cons(active X1, X2),
                 active from X -> mark cons(X, from s X),
                 active from X -> from active X,
                    active s X -> s active X,
      active length cons(X, Y) -> mark s length1 Y,
           active length nil() -> mark 0(),
              active length1 X -> mark length X,
                   length ok X -> ok length X,
                  length1 ok X -> ok length1 X,
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper from X -> from proper X,
                    proper s X -> s proper X,
                    proper 0() -> ok 0(),
               proper length X -> length proper X,
                  proper nil() -> ok nil(),
              proper length1 X -> length1 proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [cons](x0, x1) = x0 + x1,
       
       [mark](x0) = 0,
       
       [from](x0) = x0,
       
       [s](x0) = x0,
       
       [active](x0) = 0,
       
       [length](x0) = x0,
       
       [length1](x0) = x0 + 1,
       
       [proper](x0) = 0,
       
       [ok](x0) = 0,
       
       [top](x0) = 0,
       
       [0] = 0,
       
       [nil] = 0,
       
       [proper#](x0) = x0
      Strict:
       proper# length1 X -> proper# X
       1 + 1X >= 0 + 1X
       proper# length X -> proper# X
       0 + 1X >= 0 + 1X
       proper# s X -> proper# X
       0 + 1X >= 0 + 1X
       proper# from X -> proper# X
       0 + 1X >= 0 + 1X
       proper# cons(X1, X2) -> proper# X2
       0 + 1X1 + 1X2 >= 0 + 1X2
       proper# cons(X1, X2) -> proper# X1
       0 + 1X1 + 1X2 >= 0 + 1X1
      Weak:
       top ok X -> top active X
       0 + 0X >= 0 + 0X
       top mark X -> top proper X
       0 + 0X >= 0 + 0X
       proper length1 X -> length1 proper X
       0 + 0X >= 1 + 0X
       proper nil() -> ok nil()
       0 >= 0
       proper length X -> length proper X
       0 + 0X >= 0 + 0X
       proper 0() -> ok 0()
       0 >= 0
       proper s X -> s proper X
       0 + 0X >= 0 + 0X
       proper from X -> from proper X
       0 + 0X >= 0 + 0X
       proper cons(X1, X2) -> cons(proper X1, proper X2)
       0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
       length1 ok X -> ok length1 X
       1 + 0X >= 0 + 0X
       length ok X -> ok length X
       0 + 0X >= 0 + 0X
       active length1 X -> mark length X
       0 + 0X >= 0 + 0X
       active length nil() -> mark 0()
       0 >= 0
       active length cons(X, Y) -> mark s length1 Y
       0 + 0X + 0Y >= 0 + 0Y
       active s X -> s active X
       0 + 0X >= 0 + 0X
       active from X -> from active X
       0 + 0X >= 0 + 0X
       active from X -> mark cons(X, from s X)
       0 + 0X >= 0 + 0X
       active cons(X1, X2) -> cons(active X1, X2)
       0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
       s ok X -> ok s X
       0 + 0X >= 0 + 0X
       s mark X -> mark s X
       0 + 0X >= 0 + 0X
       from ok X -> ok from X
       0 + 0X >= 0 + 0X
       from mark X -> mark from X
       0 + 0X >= 0 + 0X
       cons(ok X1, ok X2) -> ok cons(X1, X2)
       0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
       cons(mark X1, X2) -> mark cons(X1, X2)
       0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
     SCCS (1):
      Scc:
       {proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
              proper# from X -> proper# X,
                 proper# s X -> proper# X,
            proper# length X -> proper# X}
      
      SCC (5):
       Strict:
        {proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
               proper# from X -> proper# X,
                  proper# s X -> proper# X,
             proper# length X -> proper# X}
       Weak:
       {       cons(mark X1, X2) -> mark cons(X1, X2),
              cons(ok X1, ok X2) -> ok cons(X1, X2),
                     from mark X -> mark from X,
                       from ok X -> ok from X,
                        s mark X -> mark s X,
                          s ok X -> ok s X,
             active cons(X1, X2) -> cons(active X1, X2),
                   active from X -> mark cons(X, from s X),
                   active from X -> from active X,
                      active s X -> s active X,
        active length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 proper X,
                      top mark X -> top proper X,
                        top ok X -> top active X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = x0 + x1,
         
         [mark](x0) = 0,
         
         [from](x0) = x0,
         
         [s](x0) = x0,
         
         [active](x0) = 0,
         
         [length](x0) = x0 + 1,
         
         [length1](x0) = 0,
         
         [proper](x0) = x0 + 1,
         
         [ok](x0) = x0 + 1,
         
         [top](x0) = 0,
         
         [0] = 1,
         
         [nil] = 1,
         
         [proper#](x0) = x0
        Strict:
         proper# length X -> proper# X
         1 + 1X >= 0 + 1X
         proper# s X -> proper# X
         0 + 1X >= 0 + 1X
         proper# from X -> proper# X
         0 + 1X >= 0 + 1X
         proper# cons(X1, X2) -> proper# X2
         0 + 1X1 + 1X2 >= 0 + 1X2
         proper# cons(X1, X2) -> proper# X1
         0 + 1X1 + 1X2 >= 0 + 1X1
        Weak:
         top ok X -> top active X
         0 + 0X >= 0 + 0X
         top mark X -> top proper X
         0 + 0X >= 0 + 0X
         proper length1 X -> length1 proper X
         1 + 0X >= 0 + 0X
         proper nil() -> ok nil()
         2 >= 2
         proper length X -> length proper X
         2 + 1X >= 2 + 1X
         proper 0() -> ok 0()
         2 >= 2
         proper s X -> s proper X
         1 + 1X >= 1 + 1X
         proper from X -> from proper X
         1 + 1X >= 1 + 1X
         proper cons(X1, X2) -> cons(proper X1, proper X2)
         1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
         length1 ok X -> ok length1 X
         0 + 0X >= 1 + 0X
         length ok X -> ok length X
         2 + 1X >= 2 + 1X
         active length1 X -> mark length X
         0 + 0X >= 0 + 0X
         active length nil() -> mark 0()
         0 >= 0
         active length cons(X, Y) -> mark s length1 Y
         0 + 0X + 0Y >= 0 + 0Y
         active s X -> s active X
         0 + 0X >= 0 + 0X
         active from X -> from active X
         0 + 0X >= 0 + 0X
         active from X -> mark cons(X, from s X)
         0 + 0X >= 0 + 0X
         active cons(X1, X2) -> cons(active X1, X2)
         0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
         s ok X -> ok s X
         1 + 1X >= 1 + 1X
         s mark X -> mark s X
         0 + 0X >= 0 + 0X
         from ok X -> ok from X
         1 + 1X >= 1 + 1X
         from mark X -> mark from X
         0 + 0X >= 0 + 0X
         cons(ok X1, ok X2) -> ok cons(X1, X2)
         2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
         cons(mark X1, X2) -> mark cons(X1, X2)
         0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
       SCCS (1):
        Scc:
         {proper# cons(X1, X2) -> proper# X1,
          proper# cons(X1, X2) -> proper# X2,
                proper# from X -> proper# X,
                   proper# s X -> proper# X}
        
        SCC (4):
         Strict:
          {proper# cons(X1, X2) -> proper# X1,
           proper# cons(X1, X2) -> proper# X2,
                 proper# from X -> proper# X,
                    proper# s X -> proper# X}
         Weak:
         {       cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
          active length cons(X, Y) -> mark s length1 Y,
               active length nil() -> mark 0(),
                  active length1 X -> mark length X,
                       length ok X -> ok length X,
                      length1 ok X -> ok length1 X,
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                   proper length X -> length proper X,
                      proper nil() -> ok nil(),
                  proper length1 X -> length1 proper X,
                        top mark X -> top proper X,
                          top ok X -> top active X}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [cons](x0, x1) = x0 + x1,
           
           [mark](x0) = 0,
           
           [from](x0) = x0,
           
           [s](x0) = x0 + 1,
           
           [active](x0) = 0,
           
           [length](x0) = 0,
           
           [length1](x0) = 1,
           
           [proper](x0) = x0 + 1,
           
           [ok](x0) = x0 + 1,
           
           [top](x0) = 0,
           
           [0] = 1,
           
           [nil] = 1,
           
           [proper#](x0) = x0
          Strict:
           proper# s X -> proper# X
           1 + 1X >= 0 + 1X
           proper# from X -> proper# X
           0 + 1X >= 0 + 1X
           proper# cons(X1, X2) -> proper# X2
           0 + 1X1 + 1X2 >= 0 + 1X2
           proper# cons(X1, X2) -> proper# X1
           0 + 1X1 + 1X2 >= 0 + 1X1
          Weak:
           top ok X -> top active X
           0 + 0X >= 0 + 0X
           top mark X -> top proper X
           0 + 0X >= 0 + 0X
           proper length1 X -> length1 proper X
           2 + 0X >= 1 + 0X
           proper nil() -> ok nil()
           2 >= 2
           proper length X -> length proper X
           1 + 0X >= 0 + 0X
           proper 0() -> ok 0()
           2 >= 2
           proper s X -> s proper X
           2 + 1X >= 2 + 1X
           proper from X -> from proper X
           1 + 1X >= 1 + 1X
           proper cons(X1, X2) -> cons(proper X1, proper X2)
           1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
           length1 ok X -> ok length1 X
           1 + 0X >= 2 + 0X
           length ok X -> ok length X
           0 + 0X >= 1 + 0X
           active length1 X -> mark length X
           0 + 0X >= 0 + 0X
           active length nil() -> mark 0()
           0 >= 0
           active length cons(X, Y) -> mark s length1 Y
           0 + 0X + 0Y >= 0 + 0Y
           active s X -> s active X
           0 + 0X >= 1 + 0X
           active from X -> from active X
           0 + 0X >= 0 + 0X
           active from X -> mark cons(X, from s X)
           0 + 0X >= 0 + 0X
           active cons(X1, X2) -> cons(active X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
           s ok X -> ok s X
           2 + 1X >= 2 + 1X
           s mark X -> mark s X
           1 + 0X >= 0 + 0X
           from ok X -> ok from X
           1 + 1X >= 1 + 1X
           from mark X -> mark from X
           0 + 0X >= 0 + 0X
           cons(ok X1, ok X2) -> ok cons(X1, X2)
           2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
           cons(mark X1, X2) -> mark cons(X1, X2)
           0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
         SCCS (1):
          Scc:
           {proper# cons(X1, X2) -> proper# X1,
            proper# cons(X1, X2) -> proper# X2,
                  proper# from X -> proper# X}
          
          SCC (3):
           Strict:
            {proper# cons(X1, X2) -> proper# X1,
             proper# cons(X1, X2) -> proper# X2,
                   proper# from X -> proper# X}
           Weak:
           {       cons(mark X1, X2) -> mark cons(X1, X2),
                  cons(ok X1, ok X2) -> ok cons(X1, X2),
                         from mark X -> mark from X,
                           from ok X -> ok from X,
                            s mark X -> mark s X,
                              s ok X -> ok s X,
                 active cons(X1, X2) -> cons(active X1, X2),
                       active from X -> mark cons(X, from s X),
                       active from X -> from active X,
                          active s X -> s active X,
            active length cons(X, Y) -> mark s length1 Y,
                 active length nil() -> mark 0(),
                    active length1 X -> mark length X,
                         length ok X -> ok length X,
                        length1 ok X -> ok length1 X,
                 proper cons(X1, X2) -> cons(proper X1, proper X2),
                       proper from X -> from proper X,
                          proper s X -> s proper X,
                          proper 0() -> ok 0(),
                     proper length X -> length proper X,
                        proper nil() -> ok nil(),
                    proper length1 X -> length1 proper X,
                          top mark X -> top proper X,
                            top ok X -> top active X}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [cons](x0, x1) = x0 + x1,
             
             [mark](x0) = 0,
             
             [from](x0) = x0 + 1,
             
             [s](x0) = x0 + 1,
             
             [active](x0) = 0,
             
             [length](x0) = 0,
             
             [length1](x0) = 1,
             
             [proper](x0) = x0 + 1,
             
             [ok](x0) = x0 + 1,
             
             [top](x0) = 0,
             
             [0] = 1,
             
             [nil] = 1,
             
             [proper#](x0) = x0
            Strict:
             proper# from X -> proper# X
             1 + 1X >= 0 + 1X
             proper# cons(X1, X2) -> proper# X2
             0 + 1X1 + 1X2 >= 0 + 1X2
             proper# cons(X1, X2) -> proper# X1
             0 + 1X1 + 1X2 >= 0 + 1X1
            Weak:
             top ok X -> top active X
             0 + 0X >= 0 + 0X
             top mark X -> top proper X
             0 + 0X >= 0 + 0X
             proper length1 X -> length1 proper X
             2 + 0X >= 1 + 0X
             proper nil() -> ok nil()
             2 >= 2
             proper length X -> length proper X
             1 + 0X >= 0 + 0X
             proper 0() -> ok 0()
             2 >= 2
             proper s X -> s proper X
             2 + 1X >= 2 + 1X
             proper from X -> from proper X
             2 + 1X >= 2 + 1X
             proper cons(X1, X2) -> cons(proper X1, proper X2)
             1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
             length1 ok X -> ok length1 X
             1 + 0X >= 2 + 0X
             length ok X -> ok length X
             0 + 0X >= 1 + 0X
             active length1 X -> mark length X
             0 + 0X >= 0 + 0X
             active length nil() -> mark 0()
             0 >= 0
             active length cons(X, Y) -> mark s length1 Y
             0 + 0X + 0Y >= 0 + 0Y
             active s X -> s active X
             0 + 0X >= 1 + 0X
             active from X -> from active X
             0 + 0X >= 1 + 0X
             active from X -> mark cons(X, from s X)
             0 + 0X >= 0 + 0X
             active cons(X1, X2) -> cons(active X1, X2)
             0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
             s ok X -> ok s X
             2 + 1X >= 2 + 1X
             s mark X -> mark s X
             1 + 0X >= 0 + 0X
             from ok X -> ok from X
             2 + 1X >= 2 + 1X
             from mark X -> mark from X
             1 + 0X >= 0 + 0X
             cons(ok X1, ok X2) -> ok cons(X1, X2)
             2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
             cons(mark X1, X2) -> mark cons(X1, X2)
             0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
           SCCS (1):
            Scc:
             {proper# cons(X1, X2) -> proper# X1,
              proper# cons(X1, X2) -> proper# X2}
            
            SCC (2):
             Strict:
              {proper# cons(X1, X2) -> proper# X1,
               proper# cons(X1, X2) -> proper# X2}
             Weak:
             {       cons(mark X1, X2) -> mark cons(X1, X2),
                    cons(ok X1, ok X2) -> ok cons(X1, X2),
                           from mark X -> mark from X,
                             from ok X -> ok from X,
                              s mark X -> mark s X,
                                s ok X -> ok s X,
                   active cons(X1, X2) -> cons(active X1, X2),
                         active from X -> mark cons(X, from s X),
                         active from X -> from active X,
                            active s X -> s active X,
              active length cons(X, Y) -> mark s length1 Y,
                   active length nil() -> mark 0(),
                      active length1 X -> mark length X,
                           length ok X -> ok length X,
                          length1 ok X -> ok length1 X,
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            proper 0() -> ok 0(),
                       proper length X -> length proper X,
                          proper nil() -> ok nil(),
                      proper length1 X -> length1 proper X,
                            top mark X -> top proper X,
                              top ok X -> top active X}
             POLY:
              Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
              Interpretation:
               [cons](x0, x1) = x0 + x1 + 1,
               
               [mark](x0) = x0 + 1,
               
               [from](x0) = 0,
               
               [s](x0) = x0 + 1,
               
               [active](x0) = x0 + 1,
               
               [length](x0) = x0,
               
               [length1](x0) = 1,
               
               [proper](x0) = x0 + 1,
               
               [ok](x0) = x0,
               
               [top](x0) = 0,
               
               [0] = 1,
               
               [nil] = 1,
               
               [proper#](x0) = x0 + 1
              Strict:
               proper# cons(X1, X2) -> proper# X2
               2 + 1X1 + 1X2 >= 1 + 1X2
               proper# cons(X1, X2) -> proper# X1
               2 + 1X1 + 1X2 >= 1 + 1X1
              Weak:
               top ok X -> top active X
               0 + 0X >= 0 + 0X
               top mark X -> top proper X
               0 + 0X >= 0 + 0X
               proper length1 X -> length1 proper X
               2 + 0X >= 1 + 0X
               proper nil() -> ok nil()
               2 >= 1
               proper length X -> length proper X
               1 + 1X >= 1 + 1X
               proper 0() -> ok 0()
               2 >= 1
               proper s X -> s proper X
               2 + 1X >= 2 + 1X
               proper from X -> from proper X
               1 + 0X >= 0 + 0X
               proper cons(X1, X2) -> cons(proper X1, proper X2)
               2 + 1X1 + 1X2 >= 3 + 1X1 + 1X2
               length1 ok X -> ok length1 X
               1 + 0X >= 1 + 0X
               length ok X -> ok length X
               0 + 1X >= 0 + 1X
               active length1 X -> mark length X
               2 + 0X >= 1 + 1X
               active length nil() -> mark 0()
               2 >= 2
               active length cons(X, Y) -> mark s length1 Y
               2 + 1X + 1Y >= 3 + 0Y
               active s X -> s active X
               2 + 1X >= 2 + 1X
               active from X -> from active X
               1 + 0X >= 0 + 0X
               active from X -> mark cons(X, from s X)
               1 + 0X >= 2 + 1X
               active cons(X1, X2) -> cons(active X1, X2)
               2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
               s ok X -> ok s X
               1 + 1X >= 1 + 1X
               s mark X -> mark s X
               2 + 1X >= 2 + 1X
               from ok X -> ok from X
               0 + 0X >= 0 + 0X
               from mark X -> mark from X
               0 + 0X >= 1 + 0X
               cons(ok X1, ok X2) -> ok cons(X1, X2)
               1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
               cons(mark X1, X2) -> mark cons(X1, X2)
               2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
             Qed
  
  SCC (1):
   Strict:
    {length1# ok X -> length1# X}
   Weak:
   {       cons(mark X1, X2) -> mark cons(X1, X2),
          cons(ok X1, ok X2) -> ok cons(X1, X2),
                 from mark X -> mark from X,
                   from ok X -> ok from X,
                    s mark X -> mark s X,
                      s ok X -> ok s X,
         active cons(X1, X2) -> cons(active X1, X2),
               active from X -> mark cons(X, from s X),
               active from X -> from active X,
                  active s X -> s active X,
    active length cons(X, Y) -> mark s length1 Y,
         active length nil() -> mark 0(),
            active length1 X -> mark length X,
                 length ok X -> ok length X,
                length1 ok X -> ok length1 X,
         proper cons(X1, X2) -> cons(proper X1, proper X2),
               proper from X -> from proper X,
                  proper s X -> s proper X,
                  proper 0() -> ok 0(),
             proper length X -> length proper X,
                proper nil() -> ok nil(),
            proper length1 X -> length1 proper X,
                  top mark X -> top proper X,
                    top ok X -> top active X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [cons](x0, x1) = x0 + 1,
     
     [mark](x0) = x0 + 1,
     
     [from](x0) = x0 + 1,
     
     [s](x0) = x0 + 1,
     
     [active](x0) = x0 + 1,
     
     [length](x0) = 1,
     
     [length1](x0) = 1,
     
     [proper](x0) = x0 + 1,
     
     [ok](x0) = x0 + 1,
     
     [top](x0) = x0 + 1,
     
     [0] = 1,
     
     [nil] = 1,
     
     [length1#](x0) = x0
    Strict:
     length1# ok X -> length1# X
     1 + 1X >= 0 + 1X
    Weak:
     top ok X -> top active X
     2 + 1X >= 2 + 1X
     top mark X -> top proper X
     2 + 1X >= 2 + 1X
     proper length1 X -> length1 proper X
     2 + 0X >= 1 + 0X
     proper nil() -> ok nil()
     2 >= 2
     proper length X -> length proper X
     2 + 0X >= 1 + 0X
     proper 0() -> ok 0()
     2 >= 2
     proper s X -> s proper X
     2 + 1X >= 2 + 1X
     proper from X -> from proper X
     2 + 1X >= 2 + 1X
     proper cons(X1, X2) -> cons(proper X1, proper X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     length1 ok X -> ok length1 X
     1 + 0X >= 2 + 0X
     length ok X -> ok length X
     1 + 0X >= 2 + 0X
     active length1 X -> mark length X
     2 + 0X >= 2 + 0X
     active length nil() -> mark 0()
     2 >= 2
     active length cons(X, Y) -> mark s length1 Y
     2 + 0X + 0Y >= 3 + 0Y
     active s X -> s active X
     2 + 1X >= 2 + 1X
     active from X -> from active X
     2 + 1X >= 2 + 1X
     active from X -> mark cons(X, from s X)
     2 + 1X >= 2 + 1X
     active cons(X1, X2) -> cons(active X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     s ok X -> ok s X
     2 + 1X >= 2 + 1X
     s mark X -> mark s X
     2 + 1X >= 2 + 1X
     from ok X -> ok from X
     2 + 1X >= 2 + 1X
     from mark X -> mark from X
     2 + 1X >= 2 + 1X
     cons(ok X1, ok X2) -> ok cons(X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     cons(mark X1, X2) -> mark cons(X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
   Qed
 
 SCC (1):
  Strict:
   {length# ok X -> length# X}
  Weak:
  {       cons(mark X1, X2) -> mark cons(X1, X2),
         cons(ok X1, ok X2) -> ok cons(X1, X2),
                from mark X -> mark from X,
                  from ok X -> ok from X,
                   s mark X -> mark s X,
                     s ok X -> ok s X,
        active cons(X1, X2) -> cons(active X1, X2),
              active from X -> mark cons(X, from s X),
              active from X -> from active X,
                 active s X -> s active X,
   active length cons(X, Y) -> mark s length1 Y,
        active length nil() -> mark 0(),
           active length1 X -> mark length X,
                length ok X -> ok length X,
               length1 ok X -> ok length1 X,
        proper cons(X1, X2) -> cons(proper X1, proper X2),
              proper from X -> from proper X,
                 proper s X -> s proper X,
                 proper 0() -> ok 0(),
            proper length X -> length proper X,
               proper nil() -> ok nil(),
           proper length1 X -> length1 proper X,
                 top mark X -> top proper X,
                   top ok X -> top active X}
  POLY:
   Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
   Interpretation:
    [cons](x0, x1) = x0 + 1,
    
    [mark](x0) = x0 + 1,
    
    [from](x0) = x0 + 1,
    
    [s](x0) = x0 + 1,
    
    [active](x0) = x0 + 1,
    
    [length](x0) = 1,
    
    [length1](x0) = 1,
    
    [proper](x0) = x0 + 1,
    
    [ok](x0) = x0 + 1,
    
    [top](x0) = x0 + 1,
    
    [0] = 1,
    
    [nil] = 1,
    
    [length#](x0) = x0
   Strict:
    length# ok X -> length# X
    1 + 1X >= 0 + 1X
   Weak:
    top ok X -> top active X
    2 + 1X >= 2 + 1X
    top mark X -> top proper X
    2 + 1X >= 2 + 1X
    proper length1 X -> length1 proper X
    2 + 0X >= 1 + 0X
    proper nil() -> ok nil()
    2 >= 2
    proper length X -> length proper X
    2 + 0X >= 1 + 0X
    proper 0() -> ok 0()
    2 >= 2
    proper s X -> s proper X
    2 + 1X >= 2 + 1X
    proper from X -> from proper X
    2 + 1X >= 2 + 1X
    proper cons(X1, X2) -> cons(proper X1, proper X2)
    2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
    length1 ok X -> ok length1 X
    1 + 0X >= 2 + 0X
    length ok X -> ok length X
    1 + 0X >= 2 + 0X
    active length1 X -> mark length X
    2 + 0X >= 2 + 0X
    active length nil() -> mark 0()
    2 >= 2
    active length cons(X, Y) -> mark s length1 Y
    2 + 0X + 0Y >= 3 + 0Y
    active s X -> s active X
    2 + 1X >= 2 + 1X
    active from X -> from active X
    2 + 1X >= 2 + 1X
    active from X -> mark cons(X, from s X)
    2 + 1X >= 2 + 1X
    active cons(X1, X2) -> cons(active X1, X2)
    2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
    s ok X -> ok s X
    2 + 1X >= 2 + 1X
    s mark X -> mark s X
    2 + 1X >= 2 + 1X
    from ok X -> ok from X
    2 + 1X >= 2 + 1X
    from mark X -> mark from X
    2 + 1X >= 2 + 1X
    cons(ok X1, ok X2) -> ok cons(X1, X2)
    2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
    cons(mark X1, X2) -> mark cons(X1, X2)
    2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
  Qed
 
 SCC (2):
  Strict:
   {s# mark X -> s# X,
      s# ok X -> s# X}
  Weak:
  {       cons(mark X1, X2) -> mark cons(X1, X2),
         cons(ok X1, ok X2) -> ok cons(X1, X2),
                from mark X -> mark from X,
                  from ok X -> ok from X,
                   s mark X -> mark s X,
                     s ok X -> ok s X,
        active cons(X1, X2) -> cons(active X1, X2),
              active from X -> mark cons(X, from s X),
              active from X -> from active X,
                 active s X -> s active X,
   active length cons(X, Y) -> mark s length1 Y,
        active length nil() -> mark 0(),
           active length1 X -> mark length X,
                length ok X -> ok length X,
               length1 ok X -> ok length1 X,
        proper cons(X1, X2) -> cons(proper X1, proper X2),
              proper from X -> from proper X,
                 proper s X -> s proper X,
                 proper 0() -> ok 0(),
            proper length X -> length proper X,
               proper nil() -> ok nil(),
           proper length1 X -> length1 proper X,
                 top mark X -> top proper X,
                   top ok X -> top active X}
  POLY:
   Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
   Interpretation:
    [cons](x0, x1) = 0,
    
    [mark](x0) = x0,
    
    [from](x0) = 0,
    
    [s](x0) = x0 + 1,
    
    [active](x0) = 0,
    
    [length](x0) = 0,
    
    [length1](x0) = 1,
    
    [proper](x0) = x0 + 1,
    
    [ok](x0) = x0 + 1,
    
    [top](x0) = 0,
    
    [0] = 0,
    
    [nil] = 1,
    
    [s#](x0) = x0
   Strict:
    s# ok X -> s# X
    1 + 1X >= 0 + 1X
    s# mark X -> s# X
    0 + 1X >= 0 + 1X
   Weak:
    top ok X -> top active X
    0 + 0X >= 0 + 0X
    top mark X -> top proper X
    0 + 0X >= 0 + 0X
    proper length1 X -> length1 proper X
    2 + 0X >= 1 + 0X
    proper nil() -> ok nil()
    2 >= 2
    proper length X -> length proper X
    1 + 0X >= 0 + 0X
    proper 0() -> ok 0()
    1 >= 1
    proper s X -> s proper X
    2 + 1X >= 2 + 1X
    proper from X -> from proper X
    1 + 0X >= 0 + 0X
    proper cons(X1, X2) -> cons(proper X1, proper X2)
    1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
    length1 ok X -> ok length1 X
    1 + 0X >= 2 + 0X
    length ok X -> ok length X
    0 + 0X >= 1 + 0X
    active length1 X -> mark length X
    0 + 0X >= 0 + 0X
    active length nil() -> mark 0()
    0 >= 0
    active length cons(X, Y) -> mark s length1 Y
    0 + 0X + 0Y >= 2 + 0Y
    active s X -> s active X
    0 + 0X >= 1 + 0X
    active from X -> from active X
    0 + 0X >= 0 + 0X
    active from X -> mark cons(X, from s X)
    0 + 0X >= 0 + 0X
    active cons(X1, X2) -> cons(active X1, X2)
    0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
    s ok X -> ok s X
    2 + 1X >= 2 + 1X
    s mark X -> mark s X
    1 + 1X >= 1 + 1X
    from ok X -> ok from X
    0 + 0X >= 1 + 0X
    from mark X -> mark from X
    0 + 0X >= 0 + 0X
    cons(ok X1, ok X2) -> ok cons(X1, X2)
    0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
    cons(mark X1, X2) -> mark cons(X1, X2)
    0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
  SCCS (1):
   Scc:
    {s# mark X -> s# X}
   
   SCC (1):
    Strict:
     {s# mark X -> s# X}
    Weak:
    {       cons(mark X1, X2) -> mark cons(X1, X2),
           cons(ok X1, ok X2) -> ok cons(X1, X2),
                  from mark X -> mark from X,
                    from ok X -> ok from X,
                     s mark X -> mark s X,
                       s ok X -> ok s X,
          active cons(X1, X2) -> cons(active X1, X2),
                active from X -> mark cons(X, from s X),
                active from X -> from active X,
                   active s X -> s active X,
     active length cons(X, Y) -> mark s length1 Y,
          active length nil() -> mark 0(),
             active length1 X -> mark length X,
                  length ok X -> ok length X,
                 length1 ok X -> ok length1 X,
          proper cons(X1, X2) -> cons(proper X1, proper X2),
                proper from X -> from proper X,
                   proper s X -> s proper X,
                   proper 0() -> ok 0(),
              proper length X -> length proper X,
                 proper nil() -> ok nil(),
             proper length1 X -> length1 proper X,
                   top mark X -> top proper X,
                     top ok X -> top active X}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [cons](x0, x1) = x0 + 1,
      
      [mark](x0) = x0 + 1,
      
      [from](x0) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [active](x0) = x0 + 1,
      
      [length](x0) = 1,
      
      [length1](x0) = 1,
      
      [proper](x0) = x0 + 1,
      
      [ok](x0) = x0 + 1,
      
      [top](x0) = x0 + 1,
      
      [0] = 1,
      
      [nil] = 1,
      
      [s#](x0) = x0
     Strict:
      s# mark X -> s# X
      1 + 1X >= 0 + 1X
     Weak:
      top ok X -> top active X
      2 + 1X >= 2 + 1X
      top mark X -> top proper X
      2 + 1X >= 2 + 1X
      proper length1 X -> length1 proper X
      2 + 0X >= 1 + 0X
      proper nil() -> ok nil()
      2 >= 2
      proper length X -> length proper X
      2 + 0X >= 1 + 0X
      proper 0() -> ok 0()
      2 >= 2
      proper s X -> s proper X
      2 + 1X >= 2 + 1X
      proper from X -> from proper X
      2 + 1X >= 2 + 1X
      proper cons(X1, X2) -> cons(proper X1, proper X2)
      2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
      length1 ok X -> ok length1 X
      1 + 0X >= 2 + 0X
      length ok X -> ok length X
      1 + 0X >= 2 + 0X
      active length1 X -> mark length X
      2 + 0X >= 2 + 0X
      active length nil() -> mark 0()
      2 >= 2
      active length cons(X, Y) -> mark s length1 Y
      2 + 0X + 0Y >= 3 + 0Y
      active s X -> s active X
      2 + 1X >= 2 + 1X
      active from X -> from active X
      2 + 1X >= 2 + 1X
      active from X -> mark cons(X, from s X)
      2 + 1X >= 2 + 1X
      active cons(X1, X2) -> cons(active X1, X2)
      2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
      s ok X -> ok s X
      2 + 1X >= 2 + 1X
      s mark X -> mark s X
      2 + 1X >= 2 + 1X
      from ok X -> ok from X
      2 + 1X >= 2 + 1X
      from mark X -> mark from X
      2 + 1X >= 2 + 1X
      cons(ok X1, ok X2) -> ok cons(X1, X2)
      2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
      cons(mark X1, X2) -> mark cons(X1, X2)
      2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
    Qed

SCC (2):
 Strict:
  {from# mark X -> from# X,
     from# ok X -> from# X}
 Weak:
 {       cons(mark X1, X2) -> mark cons(X1, X2),
        cons(ok X1, ok X2) -> ok cons(X1, X2),
               from mark X -> mark from X,
                 from ok X -> ok from X,
                  s mark X -> mark s X,
                    s ok X -> ok s X,
       active cons(X1, X2) -> cons(active X1, X2),
             active from X -> mark cons(X, from s X),
             active from X -> from active X,
                active s X -> s active X,
  active length cons(X, Y) -> mark s length1 Y,
       active length nil() -> mark 0(),
          active length1 X -> mark length X,
               length ok X -> ok length X,
              length1 ok X -> ok length1 X,
       proper cons(X1, X2) -> cons(proper X1, proper X2),
             proper from X -> from proper X,
                proper s X -> s proper X,
                proper 0() -> ok 0(),
           proper length X -> length proper X,
              proper nil() -> ok nil(),
          proper length1 X -> length1 proper X,
                top mark X -> top proper X,
                  top ok X -> top active X}
 POLY:
  Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
  Interpretation:
   [cons](x0, x1) = 0,
   
   [mark](x0) = x0,
   
   [from](x0) = 0,
   
   [s](x0) = x0 + 1,
   
   [active](x0) = 0,
   
   [length](x0) = 0,
   
   [length1](x0) = 1,
   
   [proper](x0) = x0 + 1,
   
   [ok](x0) = x0 + 1,
   
   [top](x0) = 0,
   
   [0] = 0,
   
   [nil] = 1,
   
   [from#](x0) = x0
  Strict:
   from# ok X -> from# X
   1 + 1X >= 0 + 1X
   from# mark X -> from# X
   0 + 1X >= 0 + 1X
  Weak:
   top ok X -> top active X
   0 + 0X >= 0 + 0X
   top mark X -> top proper X
   0 + 0X >= 0 + 0X
   proper length1 X -> length1 proper X
   2 + 0X >= 1 + 0X
   proper nil() -> ok nil()
   2 >= 2
   proper length X -> length proper X
   1 + 0X >= 0 + 0X
   proper 0() -> ok 0()
   1 >= 1
   proper s X -> s proper X
   2 + 1X >= 2 + 1X
   proper from X -> from proper X
   1 + 0X >= 0 + 0X
   proper cons(X1, X2) -> cons(proper X1, proper X2)
   1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
   length1 ok X -> ok length1 X
   1 + 0X >= 2 + 0X
   length ok X -> ok length X
   0 + 0X >= 1 + 0X
   active length1 X -> mark length X
   0 + 0X >= 0 + 0X
   active length nil() -> mark 0()
   0 >= 0
   active length cons(X, Y) -> mark s length1 Y
   0 + 0X + 0Y >= 2 + 0Y
   active s X -> s active X
   0 + 0X >= 1 + 0X
   active from X -> from active X
   0 + 0X >= 0 + 0X
   active from X -> mark cons(X, from s X)
   0 + 0X >= 0 + 0X
   active cons(X1, X2) -> cons(active X1, X2)
   0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
   s ok X -> ok s X
   2 + 1X >= 2 + 1X
   s mark X -> mark s X
   1 + 1X >= 1 + 1X
   from ok X -> ok from X
   0 + 0X >= 1 + 0X
   from mark X -> mark from X
   0 + 0X >= 0 + 0X
   cons(ok X1, ok X2) -> ok cons(X1, X2)
   0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
   cons(mark X1, X2) -> mark cons(X1, X2)
   0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
 SCCS (1):
  Scc:
   {from# mark X -> from# X}
  
  SCC (1):
   Strict:
    {from# mark X -> from# X}
   Weak:
   {       cons(mark X1, X2) -> mark cons(X1, X2),
          cons(ok X1, ok X2) -> ok cons(X1, X2),
                 from mark X -> mark from X,
                   from ok X -> ok from X,
                    s mark X -> mark s X,
                      s ok X -> ok s X,
         active cons(X1, X2) -> cons(active X1, X2),
               active from X -> mark cons(X, from s X),
               active from X -> from active X,
                  active s X -> s active X,
    active length cons(X, Y) -> mark s length1 Y,
         active length nil() -> mark 0(),
            active length1 X -> mark length X,
                 length ok X -> ok length X,
                length1 ok X -> ok length1 X,
         proper cons(X1, X2) -> cons(proper X1, proper X2),
               proper from X -> from proper X,
                  proper s X -> s proper X,
                  proper 0() -> ok 0(),
             proper length X -> length proper X,
                proper nil() -> ok nil(),
            proper length1 X -> length1 proper X,
                  top mark X -> top proper X,
                    top ok X -> top active X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [cons](x0, x1) = x0 + 1,
     
     [mark](x0) = x0 + 1,
     
     [from](x0) = x0 + 1,
     
     [s](x0) = x0 + 1,
     
     [active](x0) = x0 + 1,
     
     [length](x0) = 1,
     
     [length1](x0) = 1,
     
     [proper](x0) = x0 + 1,
     
     [ok](x0) = x0 + 1,
     
     [top](x0) = x0 + 1,
     
     [0] = 1,
     
     [nil] = 1,
     
     [from#](x0) = x0
    Strict:
     from# mark X -> from# X
     1 + 1X >= 0 + 1X
    Weak:
     top ok X -> top active X
     2 + 1X >= 2 + 1X
     top mark X -> top proper X
     2 + 1X >= 2 + 1X
     proper length1 X -> length1 proper X
     2 + 0X >= 1 + 0X
     proper nil() -> ok nil()
     2 >= 2
     proper length X -> length proper X
     2 + 0X >= 1 + 0X
     proper 0() -> ok 0()
     2 >= 2
     proper s X -> s proper X
     2 + 1X >= 2 + 1X
     proper from X -> from proper X
     2 + 1X >= 2 + 1X
     proper cons(X1, X2) -> cons(proper X1, proper X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     length1 ok X -> ok length1 X
     1 + 0X >= 2 + 0X
     length ok X -> ok length X
     1 + 0X >= 2 + 0X
     active length1 X -> mark length X
     2 + 0X >= 2 + 0X
     active length nil() -> mark 0()
     2 >= 2
     active length cons(X, Y) -> mark s length1 Y
     2 + 0X + 0Y >= 3 + 0Y
     active s X -> s active X
     2 + 1X >= 2 + 1X
     active from X -> from active X
     2 + 1X >= 2 + 1X
     active from X -> mark cons(X, from s X)
     2 + 1X >= 2 + 1X
     active cons(X1, X2) -> cons(active X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     s ok X -> ok s X
     2 + 1X >= 2 + 1X
     s mark X -> mark s X
     2 + 1X >= 2 + 1X
     from ok X -> ok from X
     2 + 1X >= 2 + 1X
     from mark X -> mark from X
     2 + 1X >= 2 + 1X
     cons(ok X1, ok X2) -> ok cons(X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     cons(mark X1, X2) -> mark cons(X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
   Qed

SCC (2):
 Strict:
  { cons#(mark X1, X2) -> cons#(X1, X2),
   cons#(ok X1, ok X2) -> cons#(X1, X2)}
 Weak:
 {       cons(mark X1, X2) -> mark cons(X1, X2),
        cons(ok X1, ok X2) -> ok cons(X1, X2),
               from mark X -> mark from X,
                 from ok X -> ok from X,
                  s mark X -> mark s X,
                    s ok X -> ok s X,
       active cons(X1, X2) -> cons(active X1, X2),
             active from X -> mark cons(X, from s X),
             active from X -> from active X,
                active s X -> s active X,
  active length cons(X, Y) -> mark s length1 Y,
       active length nil() -> mark 0(),
          active length1 X -> mark length X,
               length ok X -> ok length X,
              length1 ok X -> ok length1 X,
       proper cons(X1, X2) -> cons(proper X1, proper X2),
             proper from X -> from proper X,
                proper s X -> s proper X,
                proper 0() -> ok 0(),
           proper length X -> length proper X,
              proper nil() -> ok nil(),
          proper length1 X -> length1 proper X,
                top mark X -> top proper X,
                  top ok X -> top active X}
 POLY:
  Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
  Interpretation:
   [cons](x0, x1) = x0 + 1,
   
   [mark](x0) = x0 + 1,
   
   [from](x0) = 0,
   
   [s](x0) = x0 + 1,
   
   [active](x0) = x0 + 1,
   
   [length](x0) = 1,
   
   [length1](x0) = 1,
   
   [proper](x0) = x0 + 1,
   
   [ok](x0) = x0 + 1,
   
   [top](x0) = x0,
   
   [0] = 1,
   
   [nil] = 0,
   
   [cons#](x0, x1) = x0
  Strict:
   cons#(ok X1, ok X2) -> cons#(X1, X2)
   1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
   cons#(mark X1, X2) -> cons#(X1, X2)
   0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
  Weak:
   top ok X -> top active X
   1 + 1X >= 1 + 1X
   top mark X -> top proper X
   1 + 1X >= 1 + 1X
   proper length1 X -> length1 proper X
   2 + 0X >= 1 + 0X
   proper nil() -> ok nil()
   1 >= 1
   proper length X -> length proper X
   2 + 0X >= 1 + 0X
   proper 0() -> ok 0()
   2 >= 2
   proper s X -> s proper X
   2 + 1X >= 2 + 1X
   proper from X -> from proper X
   1 + 0X >= 0 + 0X
   proper cons(X1, X2) -> cons(proper X1, proper X2)
   2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
   length1 ok X -> ok length1 X
   1 + 0X >= 2 + 0X
   length ok X -> ok length X
   1 + 0X >= 2 + 0X
   active length1 X -> mark length X
   2 + 0X >= 2 + 0X
   active length nil() -> mark 0()
   2 >= 2
   active length cons(X, Y) -> mark s length1 Y
   2 + 0X + 0Y >= 3 + 0Y
   active s X -> s active X
   2 + 1X >= 2 + 1X
   active from X -> from active X
   1 + 0X >= 0 + 0X
   active from X -> mark cons(X, from s X)
   1 + 0X >= 2 + 1X
   active cons(X1, X2) -> cons(active X1, X2)
   2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
   s ok X -> ok s X
   2 + 1X >= 2 + 1X
   s mark X -> mark s X
   2 + 1X >= 2 + 1X
   from ok X -> ok from X
   0 + 0X >= 1 + 0X
   from mark X -> mark from X
   0 + 0X >= 1 + 0X
   cons(ok X1, ok X2) -> ok cons(X1, X2)
   2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
   cons(mark X1, X2) -> mark cons(X1, X2)
   2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
 SCCS (1):
  Scc:
   {cons#(mark X1, X2) -> cons#(X1, X2)}
  
  SCC (1):
   Strict:
    {cons#(mark X1, X2) -> cons#(X1, X2)}
   Weak:
   {       cons(mark X1, X2) -> mark cons(X1, X2),
          cons(ok X1, ok X2) -> ok cons(X1, X2),
                 from mark X -> mark from X,
                   from ok X -> ok from X,
                    s mark X -> mark s X,
                      s ok X -> ok s X,
         active cons(X1, X2) -> cons(active X1, X2),
               active from X -> mark cons(X, from s X),
               active from X -> from active X,
                  active s X -> s active X,
    active length cons(X, Y) -> mark s length1 Y,
         active length nil() -> mark 0(),
            active length1 X -> mark length X,
                 length ok X -> ok length X,
                length1 ok X -> ok length1 X,
         proper cons(X1, X2) -> cons(proper X1, proper X2),
               proper from X -> from proper X,
                  proper s X -> s proper X,
                  proper 0() -> ok 0(),
             proper length X -> length proper X,
                proper nil() -> ok nil(),
            proper length1 X -> length1 proper X,
                  top mark X -> top proper X,
                    top ok X -> top active X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [cons](x0, x1) = x0 + 1,
     
     [mark](x0) = x0 + 1,
     
     [from](x0) = x0 + 1,
     
     [s](x0) = x0 + 1,
     
     [active](x0) = x0 + 1,
     
     [length](x0) = 1,
     
     [length1](x0) = 1,
     
     [proper](x0) = x0 + 1,
     
     [ok](x0) = x0 + 1,
     
     [top](x0) = x0 + 1,
     
     [0] = 1,
     
     [nil] = 1,
     
     [cons#](x0, x1) = x0
    Strict:
     cons#(mark X1, X2) -> cons#(X1, X2)
     1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
    Weak:
     top ok X -> top active X
     2 + 1X >= 2 + 1X
     top mark X -> top proper X
     2 + 1X >= 2 + 1X
     proper length1 X -> length1 proper X
     2 + 0X >= 1 + 0X
     proper nil() -> ok nil()
     2 >= 2
     proper length X -> length proper X
     2 + 0X >= 1 + 0X
     proper 0() -> ok 0()
     2 >= 2
     proper s X -> s proper X
     2 + 1X >= 2 + 1X
     proper from X -> from proper X
     2 + 1X >= 2 + 1X
     proper cons(X1, X2) -> cons(proper X1, proper X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     length1 ok X -> ok length1 X
     1 + 0X >= 2 + 0X
     length ok X -> ok length X
     1 + 0X >= 2 + 0X
     active length1 X -> mark length X
     2 + 0X >= 2 + 0X
     active length nil() -> mark 0()
     2 >= 2
     active length cons(X, Y) -> mark s length1 Y
     2 + 0X + 0Y >= 3 + 0Y
     active s X -> s active X
     2 + 1X >= 2 + 1X
     active from X -> from active X
     2 + 1X >= 2 + 1X
     active from X -> mark cons(X, from s X)
     2 + 1X >= 2 + 1X
     active cons(X1, X2) -> cons(active X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     s ok X -> ok s X
     2 + 1X >= 2 + 1X
     s mark X -> mark s X
     2 + 1X >= 2 + 1X
     from ok X -> ok from X
     2 + 1X >= 2 + 1X
     from mark X -> mark from X
     2 + 1X >= 2 + 1X
     cons(ok X1, ok X2) -> ok cons(X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     cons(mark X1, X2) -> mark cons(X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
   Qed