YES Problem: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) Proof: DP Processor: DPs: active#(f(x)) -> f#(f(x)) chk#(no(f(x))) -> f#(X()) chk#(no(f(x))) -> f#(f(X())) chk#(no(f(x))) -> f#(f(f(X()))) chk#(no(f(x))) -> f#(f(f(f(X())))) chk#(no(f(x))) -> f#(f(f(f(f(X()))))) chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat#(f(x),f(y())) -> mat#(x,y()) mat#(f(x),f(y())) -> f#(mat(x,y())) chk#(no(c())) -> active#(c()) f#(active(x)) -> f#(x) f#(active(x)) -> active#(f(x)) f#(no(x)) -> f#(x) f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(X()) tp#(mark(x)) -> f#(f(X())) tp#(mark(x)) -> f#(f(f(X()))) tp#(mark(x)) -> f#(f(f(f(X())))) tp#(mark(x)) -> f#(f(f(f(f(X()))))) tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) TRS: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) Matrix Interpretation Processor: dim=2 interpretation: [tp#](x0) = [0 2]x0, [mat#](x0, x1) = [0 1]x1, [chk#](x0) = [0 2]x0, [f#](x0) = [1 1]x0, [active#](x0) = [1 1]x0 + [1], [0 0] [2] [tp](x0) = [0 1]x0 + [1], [0] [c] = [1], [1] [y] = [0], [0 3] [0] [mat](x0, x1) = [0 1]x1 + [1], [0] [X] = [0], [0 1] [chk](x0) = [0 1]x0, [0 1] [2] [no](x0) = [2 0]x0 + [2], [1] [mark](x0) = x0 + [2], [0 1] [1] [active](x0) = [2 0]x0 + [2], [0 1] [f](x0) = [2 0]x0 orientation: active#(f(x)) = [2 1]x + [1] >= [2 1]x = f#(f(x)) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(X()) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(X())) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(f(X()))) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(f(f(X())))) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(f(f(f(X()))))) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(f(f(f(f(X())))))) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(f(f(f(f(f(X()))))))) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(f(f(f(f(f(f(X())))))))) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(f(f(f(f(f(f(f(X()))))))))) chk#(no(f(x))) = [0 4]x + [4] >= [0] = f#(f(f(f(f(f(f(f(f(f(X())))))))))) chk#(no(f(x))) = [0 4]x + [4] >= [0 1]x = mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) chk#(no(f(x))) = [0 4]x + [4] >= [0 2]x + [2] = chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) chk#(no(f(x))) = [0 4]x + [4] >= [0 2]x + [2] = f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat#(f(x),f(y())) = [2] >= [0] = mat#(x,y()) mat#(f(x),f(y())) = [2] >= [1] = f#(mat(x,y())) chk#(no(c())) = 4 >= 2 = active#(c()) f#(active(x)) = [2 1]x + [3] >= [1 1]x = f#(x) f#(active(x)) = [2 1]x + [3] >= [2 1]x + [1] = active#(f(x)) f#(no(x)) = [2 1]x + [4] >= [1 1]x = f#(x) f#(mark(x)) = [1 1]x + [3] >= [1 1]x = f#(x) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(X()) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(X())) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(f(X()))) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(f(f(X())))) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(f(f(f(X()))))) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(f(f(f(f(X())))))) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(f(f(f(f(f(X()))))))) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(f(f(f(f(f(f(X())))))))) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(f(f(f(f(f(f(f(X()))))))))) tp#(mark(x)) = [0 2]x + [4] >= [0] = f#(f(f(f(f(f(f(f(f(f(X())))))))))) tp#(mark(x)) = [0 2]x + [4] >= [0 1]x = mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) tp#(mark(x)) = [0 2]x + [4] >= [0 2]x + [2] = chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) tp#(mark(x)) = [0 2]x + [4] >= [0 2]x + [2] = tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [2 0] [1] [2 0] [1] active(f(x)) = [0 2]x + [2] >= [0 2]x + [2] = mark(f(f(x))) [0 2] [2] [0 1] [1] chk(no(f(x))) = [0 2]x + [2] >= [0 2]x + [2] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [6] [1] mat(f(x),f(y())) = [3] >= [0] = f(mat(x,y())) [2] [2] chk(no(c())) = [2] >= [2] = active(c()) [3] [3] mat(f(x),c()) = [2] >= [2] = no(c()) [2 0] [2] [2 0] [1] f(active(x)) = [0 2]x + [2] >= [0 2]x + [2] = active(f(x)) [2 0] [2] [2 0] [2] f(no(x)) = [0 2]x + [4] >= [0 2]x + [2] = no(f(x)) [0 1] [2] [0 1] [1] f(mark(x)) = [2 0]x + [2] >= [2 0]x + [2] = mark(f(x)) [0 0] [2] [0 0] [2] tp(mark(x)) = [0 1]x + [3] >= [0 1]x + [2] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) problem: DPs: TRS: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) Qed