MAYBE
Time: 0.009694
TRS:
 {       cons(mark X1, X2) -> mark cons(X1, X2),
        cons(ok X1, ok X2) -> ok cons(X1, X2),
       active cons(X1, X2) -> cons(active X1, X2),
            active zeros() -> mark cons(0(), zeros()),
        active and(X1, X2) -> and(active X1, X2),
       active and(tt(), X) -> mark X,
           active length X -> length active X,
  active length cons(N, L) -> mark s length L,
       active length nil() -> mark 0(),
                active s X -> s active X,
          and(mark X1, X2) -> mark and(X1, X2),
         and(ok X1, ok X2) -> ok and(X1, X2),
             length mark X -> mark length X,
               length ok X -> ok length X,
                  s mark X -> mark s X,
                    s ok X -> ok s X,
       proper cons(X1, X2) -> cons(proper X1, proper X2),
                proper 0() -> ok 0(),
            proper zeros() -> ok zeros(),
        proper and(X1, X2) -> and(proper X1, proper X2),
               proper tt() -> ok tt(),
           proper length X -> length proper X,
              proper nil() -> ok nil(),
                proper s X -> s 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),
         active# cons(X1, X2) -> cons#(active X1, X2),
         active# cons(X1, X2) -> active# X1,
              active# zeros() -> cons#(0(), zeros()),
          active# and(X1, X2) -> active# X1,
          active# and(X1, X2) -> and#(active X1, X2),
             active# length X -> active# X,
             active# length X -> length# active X,
    active# length cons(N, L) -> length# L,
    active# length cons(N, L) -> s# length L,
                  active# s X -> active# X,
                  active# s X -> s# active X,
            and#(mark X1, X2) -> and#(X1, X2),
           and#(ok X1, ok X2) -> and#(X1, X2),
               length# mark X -> length# X,
                 length# ok X -> length# X,
                    s# mark X -> s# X,
                      s# ok X -> s# X,
         proper# cons(X1, X2) -> cons#(proper X1, proper X2),
         proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
          proper# and(X1, X2) -> and#(proper X1, proper X2),
          proper# and(X1, X2) -> proper# X1,
          proper# and(X1, X2) -> proper# X2,
             proper# length X -> length# proper X,
             proper# length X -> proper# X,
                  proper# s X -> s# proper X,
                  proper# s 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),
        active cons(X1, X2) -> cons(active X1, X2),
             active zeros() -> mark cons(0(), zeros()),
         active and(X1, X2) -> and(active X1, X2),
        active and(tt(), X) -> mark X,
            active length X -> length active X,
   active length cons(N, L) -> mark s length L,
        active length nil() -> mark 0(),
                 active s X -> s active X,
           and(mark X1, X2) -> mark and(X1, X2),
          and(ok X1, ok X2) -> ok and(X1, X2),
              length mark X -> mark length X,
                length ok X -> ok length X,
                   s mark X -> mark s X,
                     s ok X -> ok s X,
        proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper 0() -> ok 0(),
             proper zeros() -> ok zeros(),
         proper and(X1, X2) -> and(proper X1, proper X2),
                proper tt() -> ok tt(),
            proper length X -> length proper X,
               proper nil() -> ok nil(),
                 proper s X -> s proper X,
                 top mark X -> top proper X,
                   top ok X -> top active X}
  EDG:
   {
    (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(N, L) -> s# length L)
    (active# s X -> active# X, active# length cons(N, L) -> length# L)
    (active# s X -> active# X, active# length X -> length# active X)
    (active# s X -> active# X, active# length X -> active# X)
    (active# s X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
    (active# s X -> active# X, active# and(X1, X2) -> active# X1)
    (active# s X -> active# X, active# zeros() -> cons#(0(), zeros()))
    (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (length# ok X -> length# X, length# ok X -> length# X)
    (length# ok X -> length# X, length# mark X -> length# X)
    (s# ok X -> s# X, s# ok X -> s# X)
    (s# ok X -> s# X, s# mark X -> s# 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# length X -> proper# X)
    (proper# s X -> proper# X, proper# length X -> length# proper X)
    (proper# s X -> proper# X, proper# and(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# and(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
    (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))
    (top# ok X -> active# X, active# s X -> s# active X)
    (top# ok X -> active# X, active# s X -> active# X)
    (top# ok X -> active# X, active# length cons(N, L) -> s# length L)
    (top# ok X -> active# X, active# length cons(N, L) -> length# L)
    (top# ok X -> active# X, active# length X -> length# active X)
    (top# ok X -> active# X, active# length X -> active# X)
    (top# ok X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
    (top# ok X -> active# X, active# and(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# zeros() -> cons#(0(), zeros()))
    (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# and(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# and(X1, X2) -> active# X1, active# s X -> active# X)
    (active# and(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
    (active# and(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
    (active# and(X1, X2) -> active# X1, active# length X -> length# active X)
    (active# and(X1, X2) -> active# X1, active# length X -> active# X)
    (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
    (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
    (active# and(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
    (active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (proper# and(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# and(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# and(X1, X2) -> proper# X1, proper# length X -> proper# X)
    (proper# and(X1, X2) -> proper# X1, proper# length X -> length# proper X)
    (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
    (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
    (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
    (proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
    (active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
    (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
    (active# zeros() -> cons#(0(), zeros()), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# zeros() -> cons#(0(), zeros()), cons#(mark X1, X2) -> cons#(X1, X2))
    (proper# and(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# and(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# and(X1, X2) -> proper# X2, proper# length X -> proper# X)
    (proper# and(X1, X2) -> proper# X2, proper# length X -> length# proper X)
    (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
    (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
    (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
    (proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (active# length X -> length# active X, length# ok X -> length# X)
    (active# length X -> length# active X, length# mark X -> length# X)
    (proper# length X -> length# proper X, length# ok X -> length# X)
    (proper# length X -> length# proper X, length# mark 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))
    (and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(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# 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# length cons(N, L) -> s# length L, s# mark X -> s# X)
    (active# length cons(N, L) -> s# length L, s# ok X -> s# 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# and(X1, X2) -> and#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
    (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# s X -> s# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (active# length cons(N, L) -> length# L, length# mark X -> length# X)
    (active# length cons(N, L) -> length# L, length# ok X -> length# 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) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# length X -> length# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# length X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (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# zeros() -> cons#(0(), zeros()))
    (active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# length X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# length X -> length# active X)
    (active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
    (active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
    (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# s X -> s# active 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# and(X1, X2) -> and#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
    (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# s X -> s# proper X)
    (top# mark X -> proper# X, proper# s 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# and(X1, X2) -> and#(proper X1, proper X2))
    (proper# length X -> proper# X, proper# and(X1, X2) -> proper# X1)
    (proper# length X -> proper# X, proper# and(X1, X2) -> proper# X2)
    (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# s X -> s# proper X)
    (proper# length X -> proper# X, proper# s X -> proper# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (s# mark X -> s# X, s# ok X -> s# X)
    (length# mark X -> length# X, length# mark X -> length# X)
    (length# mark X -> length# X, length# ok X -> length# X)
    (active# length X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# length X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# length X -> active# X, active# zeros() -> cons#(0(), zeros()))
    (active# length X -> active# X, active# and(X1, X2) -> active# X1)
    (active# length X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
    (active# length X -> active# X, active# length X -> active# X)
    (active# length X -> active# X, active# length X -> length# active X)
    (active# length X -> active# X, active# length cons(N, L) -> length# L)
    (active# length X -> active# X, active# length cons(N, L) -> s# length L)
    (active# length X -> active# X, active# s X -> active# X)
    (active# length X -> active# X, active# s X -> s# active X)
   }
   STATUS:
    arrows: 0.842975
    SCCS (7):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      {proper# cons(X1, X2) -> proper# X1,
       proper# cons(X1, X2) -> proper# X2,
        proper# and(X1, X2) -> proper# X1,
        proper# and(X1, X2) -> proper# X2,
           proper# length X -> proper# X,
                proper# s X -> proper# X}
     Scc:
      {active# cons(X1, X2) -> active# X1,
        active# and(X1, X2) -> active# X1,
           active# length X -> active# X,
                active# s X -> active# X}
     Scc:
      {s# mark X -> s# X,
         s# ok X -> s# X}
     Scc:
      {length# mark X -> length# X,
         length# ok X -> length# X}
     Scc:
      { and#(mark X1, X2) -> and#(X1, X2),
       and#(ok X1, ok X2) -> and#(X1, X2)}
     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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active and(X1, X2) -> and(active X1, X2),
            active and(tt(), X) -> mark X,
                active length X -> length active X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
                     active s X -> s active X,
               and(mark X1, X2) -> mark and(X1, X2),
              and(ok X1, ok X2) -> ok and(X1, X2),
                  length mark X -> mark length X,
                    length ok X -> ok length X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper and(X1, X2) -> and(proper X1, proper X2),
                    proper tt() -> ok tt(),
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     proper s X -> s proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     SCC (6):
      Strict:
       {proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
         proper# and(X1, X2) -> proper# X1,
         proper# and(X1, X2) -> proper# X2,
            proper# length 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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active and(X1, X2) -> and(active X1, X2),
            active and(tt(), X) -> mark X,
                active length X -> length active X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
                     active s X -> s active X,
               and(mark X1, X2) -> mark and(X1, X2),
              and(ok X1, ok X2) -> ok and(X1, X2),
                  length mark X -> mark length X,
                    length ok X -> ok length X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper and(X1, X2) -> and(proper X1, proper X2),
                    proper tt() -> ok tt(),
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     proper s X -> s proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     
     
     SCC (4):
      Strict:
       {active# cons(X1, X2) -> active# X1,
         active# and(X1, X2) -> active# X1,
            active# length 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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active and(X1, X2) -> and(active X1, X2),
            active and(tt(), X) -> mark X,
                active length X -> length active X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
                     active s X -> s active X,
               and(mark X1, X2) -> mark and(X1, X2),
              and(ok X1, ok X2) -> ok and(X1, X2),
                  length mark X -> mark length X,
                    length ok X -> ok length X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper and(X1, X2) -> and(proper X1, proper X2),
                    proper tt() -> ok tt(),
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     proper s X -> s proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active and(X1, X2) -> and(active X1, X2),
            active and(tt(), X) -> mark X,
                active length X -> length active X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
                     active s X -> s active X,
               and(mark X1, X2) -> mark and(X1, X2),
              and(ok X1, ok X2) -> ok and(X1, X2),
                  length mark X -> mark length X,
                    length ok X -> ok length X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper and(X1, X2) -> and(proper X1, proper X2),
                    proper tt() -> ok tt(),
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     proper s X -> s proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     SCC (2):
      Strict:
       {length# mark X -> length# X,
          length# ok X -> length# X}
      Weak:
      {       cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active and(X1, X2) -> and(active X1, X2),
            active and(tt(), X) -> mark X,
                active length X -> length active X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
                     active s X -> s active X,
               and(mark X1, X2) -> mark and(X1, X2),
              and(ok X1, ok X2) -> ok and(X1, X2),
                  length mark X -> mark length X,
                    length ok X -> ok length X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper and(X1, X2) -> and(proper X1, proper X2),
                    proper tt() -> ok tt(),
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     proper s X -> s proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (2):
      Strict:
       { and#(mark X1, X2) -> and#(X1, X2),
        and#(ok X1, ok X2) -> and#(X1, X2)}
      Weak:
      {       cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active and(X1, X2) -> and(active X1, X2),
            active and(tt(), X) -> mark X,
                active length X -> length active X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
                     active s X -> s active X,
               and(mark X1, X2) -> mark and(X1, X2),
              and(ok X1, ok X2) -> ok and(X1, X2),
                  length mark X -> mark length X,
                    length ok X -> ok length X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper and(X1, X2) -> and(proper X1, proper X2),
                    proper tt() -> ok tt(),
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     proper s X -> s proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active and(X1, X2) -> and(active X1, X2),
            active and(tt(), X) -> mark X,
                active length X -> length active X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
                     active s X -> s active X,
               and(mark X1, X2) -> mark and(X1, X2),
              and(ok X1, ok X2) -> ok and(X1, X2),
                  length mark X -> mark length X,
                    length ok X -> ok length X,
                       s mark X -> mark s X,
                         s ok X -> ok s X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper and(X1, X2) -> and(proper X1, proper X2),
                    proper tt() -> ok tt(),
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     proper s X -> s proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open