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))) Usable Rule 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: f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) active(f(x)) -> mark(f(f(x))) mat(f(x),f(y())) -> f(mat(x,y())) mat(f(x),c()) -> no(c()) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) chk(no(c())) -> active(c()) Matrix Interpretation Processor: dim=3 usable rules: f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) active(f(x)) -> mark(f(f(x))) mat(f(x),f(y())) -> f(mat(x,y())) mat(f(x),c()) -> no(c()) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) chk(no(c())) -> active(c()) interpretation: [tp#](x0) = [0 1 1]x0 + [1], [mat#](x0, x1) = [0 1 0]x1 + [1], [chk#](x0) = [0 1 1]x0 + [1], [f#](x0) = [0 1 1]x0, [active#](x0) = [0 1 1]x0 + [1], [1] [c] = [0] [0], [0] [y] = [0] [1], [0 0 0] [1] [mat](x0, x1) = [1 1 0]x1 + [1] [1 1 0] [0], [0] [X] = [0] [0], [1 0 0] [1] [chk](x0) = [0 0 1]x0 + [1] [0 0 1] [0], [1 0 0] [0] [no](x0) = [1 1 1]x0 + [1] [0 1 1] [1], [0 0 0] [0] [mark](x0) = [1 1 1]x0 + [1] [1 1 1] [1], [1 0 0] [0] [active](x0) = [1 1 1]x0 + [1] [0 1 1] [1], [0 0 0] [f](x0) = [1 0 1]x0 [0 1 0] orientation: active#(f(x)) = [1 1 1]x + [1] >= [1 1 1]x = f#(f(x)) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(X()) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(X())) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(f(X()))) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(f(f(X())))) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(X()))))) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(X())))))) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(f(X()))))))) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(f(f(X())))))))) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(f(f(f(X()))))))))) chk#(no(f(x))) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(f(f(f(f(X())))))))))) chk#(no(f(x))) = [2 2 2]x + [3] >= [0 1 0]x + [1] = mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) chk#(no(f(x))) = [2 2 2]x + [3] >= [2 2 0]x + [2] = chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) chk#(no(f(x))) = [2 2 2]x + [3] >= [2 2 0]x + [1] = f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat#(f(x),f(y())) = [2] >= [1] = mat#(x,y()) mat#(f(x),f(y())) = [2] >= [1] = f#(mat(x,y())) chk#(no(c())) = 4 >= 1 = active#(c()) f#(active(x)) = [1 2 2]x + [2] >= [0 1 1]x = f#(x) f#(active(x)) = [1 2 2]x + [2] >= [1 1 1]x + [1] = active#(f(x)) f#(no(x)) = [1 2 2]x + [2] >= [0 1 1]x = f#(x) f#(mark(x)) = [2 2 2]x + [2] >= [0 1 1]x = f#(x) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(X()) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(X())) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(f(X()))) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(f(f(X())))) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(X()))))) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(X())))))) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(f(X()))))))) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(f(f(X())))))))) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(f(f(f(X()))))))))) tp#(mark(x)) = [2 2 2]x + [3] >= [0] = f#(f(f(f(f(f(f(f(f(f(X())))))))))) tp#(mark(x)) = [2 2 2]x + [3] >= [0 1 0]x + [1] = mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) tp#(mark(x)) = [2 2 2]x + [3] >= [2 2 0]x + [2] = chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) tp#(mark(x)) = [2 2 2]x + [3] >= [2 2 0]x + [2] = tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0] [0] [0 0 0] [0] f(active(x)) = [1 1 1]x + [1] >= [1 1 1]x + [1] = active(f(x)) [1 1 1] [1] [1 1 1] [1] [0 0 0] [0] [0 0 0] [0] f(no(x)) = [1 1 1]x + [1] >= [1 1 1]x + [1] = no(f(x)) [1 1 1] [1] [1 1 1] [1] [0 0 0] [0] [0 0 0] [0] f(mark(x)) = [1 1 1]x + [1] >= [1 1 1]x + [1] = mark(f(x)) [1 1 1] [1] [1 1 1] [1] [0 0 0] [0] [0 0 0] [0] active(f(x)) = [1 1 1]x + [1] >= [1 1 1]x + [1] = mark(f(f(x))) [1 1 1] [1] [1 1 1] [1] [1] [0] mat(f(x),f(y())) = [2] >= [1] = f(mat(x,y())) [1] [1] [1] [1] mat(f(x),c()) = [2] >= [2] = no(c()) [1] [1] [0 0 0] [1] [0 0 0] [0] chk(no(f(x))) = [1 1 1]x + [2] >= [1 1 0]x + [2] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [1 1 1] [1] [1 1 0] [1] [2] [1] chk(no(c())) = [2] >= [2] = active(c()) [1] [1] problem: DPs: TRS: f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) active(f(x)) -> mark(f(f(x))) mat(f(x),f(y())) -> f(mat(x,y())) mat(f(x),c()) -> no(c()) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) chk(no(c())) -> active(c()) Qed