MAYBE
MAYBE
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(U12(X1, X2)) -> U12(active(X1), X2),
        active(U12(tt(), L)) -> mark(s(length(L))),
         active(U11(X1, X2)) -> U11(active(X1), X2),
        active(U11(tt(), L)) -> mark(U12(tt(), L)),
                active(s(X)) -> s(active(X)),
           active(length(X)) -> length(active(X)),
  active(length(cons(N, L))) -> mark(U11(tt(), L)),
       active(length(nil())) -> mark(0()),
           U12(mark(X1), X2) -> mark(U12(X1, X2)),
         U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)),
           U11(mark(X1), X2) -> mark(U11(X1, X2)),
         U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)),
                  s(mark(X)) -> mark(s(X)),
                    s(ok(X)) -> ok(s(X)),
             length(mark(X)) -> mark(length(X)),
               length(ok(X)) -> ok(length(X)),
        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(0()) -> ok(0()),
             proper(zeros()) -> ok(zeros()),
         proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)),
                proper(tt()) -> ok(tt()),
         proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)),
                proper(s(X)) -> s(proper(X)),
           proper(length(X)) -> length(proper(X)),
               proper(nil()) -> ok(nil()),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))
 }
 DUP: We consider a non-duplicating system.
  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(U12(X1, X2)) -> U12(active(X1), X2),
          active(U12(tt(), L)) -> mark(s(length(L))),
           active(U11(X1, X2)) -> U11(active(X1), X2),
          active(U11(tt(), L)) -> mark(U12(tt(), L)),
                  active(s(X)) -> s(active(X)),
             active(length(X)) -> length(active(X)),
    active(length(cons(N, L))) -> mark(U11(tt(), L)),
         active(length(nil())) -> mark(0()),
             U12(mark(X1), X2) -> mark(U12(X1, X2)),
           U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)),
             U11(mark(X1), X2) -> mark(U11(X1, X2)),
           U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
               length(mark(X)) -> mark(length(X)),
                 length(ok(X)) -> ok(length(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                   proper(0()) -> ok(0()),
               proper(zeros()) -> ok(zeros()),
           proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)),
                  proper(tt()) -> ok(tt()),
           proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
             proper(length(X)) -> length(proper(X)),
                 proper(nil()) -> ok(nil()),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))
   }
  Fail