MAYBE MAYBE TRS: { sel(X1, mark(X2)) -> mark(sel(X1, X2)), sel(mark(X1), X2) -> mark(sel(X1, X2)), sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)), fib1(X1, mark(X2)) -> mark(fib1(X1, X2)), fib1(mark(X1), X2) -> mark(fib1(X1, X2)), fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(sel(X1, X2)) -> sel(X1, active(X2)), active(sel(X1, X2)) -> sel(active(X1), X2), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib1(X1, X2)) -> fib1(X1, active(X2)), active(fib1(X1, X2)) -> fib1(active(X1), X2), active(s(X)) -> s(active(X)), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(fib(X)) -> fib(active(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> mark(fib(X)), fib(ok(X)) -> ok(fib(X)), cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)), proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(fib(X)) -> fib(proper(X)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X)) } DUP: We consider a duplicating system. Trs: { sel(X1, mark(X2)) -> mark(sel(X1, X2)), sel(mark(X1), X2) -> mark(sel(X1, X2)), sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)), fib1(X1, mark(X2)) -> mark(fib1(X1, X2)), fib1(mark(X1), X2) -> mark(fib1(X1, X2)), fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), active(sel(X1, X2)) -> sel(X1, active(X2)), active(sel(X1, X2)) -> sel(active(X1), X2), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib1(X1, X2)) -> fib1(X1, active(X2)), active(fib1(X1, X2)) -> fib1(active(X1), X2), active(s(X)) -> s(active(X)), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(fib(X)) -> fib(active(X)), active(cons(X1, X2)) -> cons(active(X1), X2), active(add(X1, X2)) -> add(X1, active(X2)), active(add(X1, X2)) -> add(active(X1), X2), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> mark(fib(X)), fib(ok(X)) -> ok(fib(X)), cons(mark(X1), X2) -> mark(cons(X1, X2)), cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)), add(X1, mark(X2)) -> mark(add(X1, X2)), add(mark(X1), X2) -> mark(add(X1, X2)), add(ok(X1), ok(X2)) -> ok(add(X1, X2)), proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)), proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)), proper(s(X)) -> s(proper(X)), proper(0()) -> ok(0()), proper(fib(X)) -> fib(proper(X)), proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)), proper(add(X1, X2)) -> add(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X)) } Fail