MAYBE
MAYBE
TRS:
 {
        if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
        if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                  f(mark(X)) -> mark(f(X)),
                    f(ok(X)) -> ok(f(X)),
      active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
    active(if(true(), X, Y)) -> mark(X),
   active(if(false(), X, Y)) -> mark(Y),
                active(f(X)) -> mark(if(X, c(), f(true()))),
                active(f(X)) -> f(active(X)),
      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(c()) -> ok(c()),
                proper(f(X)) -> f(proper(X)),
              proper(true()) -> ok(true()),
             proper(false()) -> ok(false()),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
          if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
          if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
    if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    f(mark(X)) -> mark(f(X)),
                      f(ok(X)) -> ok(f(X)),
        active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
        active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
      active(if(true(), X, Y)) -> mark(X),
     active(if(false(), X, Y)) -> mark(Y),
                  active(f(X)) -> mark(if(X, c(), f(true()))),
                  active(f(X)) -> f(active(X)),
        proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                   proper(c()) -> ok(c()),
                  proper(f(X)) -> f(proper(X)),
                proper(true()) -> ok(true()),
               proper(false()) -> ok(false()),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))
   }
  Fail