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(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))
 }
 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(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))
   }
  Fail