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))) TDG 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))) graph: tp#(mark(x)) -> tp#(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))) tp#(mark(x)) -> tp#(chk(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))) -> tp#(mark(x)) -> 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))) -> tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(X()))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(X())))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(X()))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(X())) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(X()) tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) -> mat#(f(x),f(y())) -> f#(mat(x,y())) tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) -> mat#(f(x),f(y())) -> mat#(x,y()) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(c())) -> active#(c()) tp#(mark(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))) tp#(mark(x)) -> chk#(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)) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(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)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(X()))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(X())))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(X()))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(X())) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(X()) tp#(mark(x)) -> f#(X()) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(X()) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(X()) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(X()) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(X())) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(X())) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(X())) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(X())) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(X()))) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(X()))) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(X()))) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(f(X()))) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(X())))) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(X())))) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(X())))) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(f(f(X())))) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(X()))))) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(X()))))) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(X()))))) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(f(f(f(X()))))) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) -> f#(active(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) -> f#(mark(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) -> f#(no(x)) -> f#(x) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) -> f#(active(x)) -> active#(f(x)) tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) -> f#(active(x)) -> f#(x) mat#(f(x),f(y())) -> mat#(x,y()) -> mat#(f(x),f(y())) -> f#(mat(x,y())) mat#(f(x),f(y())) -> mat#(x,y()) -> mat#(f(x),f(y())) -> mat#(x,y()) mat#(f(x),f(y())) -> f#(mat(x,y())) -> f#(mark(x)) -> f#(x) mat#(f(x),f(y())) -> f#(mat(x,y())) -> f#(no(x)) -> f#(x) mat#(f(x),f(y())) -> f#(mat(x,y())) -> f#(active(x)) -> active#(f(x)) mat#(f(x),f(y())) -> f#(mat(x,y())) -> f#(active(x)) -> f#(x) chk#(no(c())) -> active#(c()) -> active#(f(x)) -> f#(f(x)) chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) -> mat#(f(x),f(y())) -> f#(mat(x,y())) chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) -> mat#(f(x),f(y())) -> mat#(x,y()) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(c())) -> active#(c()) 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))) chk#(no(f(x))) -> chk#(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))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),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#(f(f(f(f(f(f(f(f(f(X())))))))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(X()))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(X())))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(X()))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(X())) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(X()) chk#(no(f(x))) -> f#(X()) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(X()) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(X()) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(X()) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(X())) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(X())) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(X())) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(X())) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(X()))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(X()))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(X()))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(f(X()))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(X())))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(X())))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(X())))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(f(f(X())))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(X()))))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(X()))))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(X()))))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(f(f(f(X()))))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) -> f#(mark(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) -> f#(active(x)) -> f#(x) f#(no(x)) -> f#(x) -> f#(mark(x)) -> f#(x) f#(no(x)) -> f#(x) -> f#(no(x)) -> f#(x) f#(no(x)) -> f#(x) -> f#(active(x)) -> active#(f(x)) f#(no(x)) -> f#(x) -> f#(active(x)) -> f#(x) f#(mark(x)) -> f#(x) -> f#(mark(x)) -> f#(x) f#(mark(x)) -> f#(x) -> f#(no(x)) -> f#(x) f#(mark(x)) -> f#(x) -> f#(active(x)) -> active#(f(x)) f#(mark(x)) -> f#(x) -> f#(active(x)) -> f#(x) f#(active(x)) -> f#(x) -> f#(mark(x)) -> f#(x) f#(active(x)) -> f#(x) -> f#(no(x)) -> f#(x) f#(active(x)) -> f#(x) -> f#(active(x)) -> active#(f(x)) f#(active(x)) -> f#(x) -> f#(active(x)) -> f#(x) f#(active(x)) -> active#(f(x)) -> active#(f(x)) -> f#(f(x)) active#(f(x)) -> f#(f(x)) -> f#(mark(x)) -> f#(x) active#(f(x)) -> f#(f(x)) -> f#(no(x)) -> f#(x) active#(f(x)) -> f#(f(x)) -> f#(active(x)) -> active#(f(x)) active#(f(x)) -> f#(f(x)) -> f#(active(x)) -> f#(x) EDG 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))) graph: tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(X()) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(X())) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(X()))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(X())))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(X()))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> tp#(mark(x)) -> 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))) -> 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))) -> tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) -> mat#(f(x),f(y())) -> mat#(x,y()) tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) -> mat#(f(x),f(y())) -> f#(mat(x,y())) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(X()) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(X())) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(X()))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(X())))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(X()))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(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)) -> chk#(no(f(x))) -> chk#(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)) -> chk#(no(f(x))) -> f#(chk(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)) -> chk#(no(c())) -> active#(c()) chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) -> mat#(f(x),f(y())) -> mat#(x,y()) chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) -> mat#(f(x),f(y())) -> f#(mat(x,y())) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(X()) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(X())) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(X()))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(X())))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(X()))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),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))) -> chk#(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))) chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) -> chk#(no(c())) -> active#(c()) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> f#(active(x)) -> f#(x) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> f#(active(x)) -> active#(f(x)) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> f#(no(x)) -> f#(x) chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -> f#(mark(x)) -> f#(x) f#(no(x)) -> f#(x) -> f#(active(x)) -> f#(x) f#(no(x)) -> f#(x) -> f#(active(x)) -> active#(f(x)) f#(no(x)) -> f#(x) -> f#(no(x)) -> f#(x) f#(no(x)) -> f#(x) -> f#(mark(x)) -> f#(x) f#(mark(x)) -> f#(x) -> f#(active(x)) -> f#(x) f#(mark(x)) -> f#(x) -> f#(active(x)) -> active#(f(x)) f#(mark(x)) -> f#(x) -> f#(no(x)) -> f#(x) f#(mark(x)) -> f#(x) -> f#(mark(x)) -> f#(x) f#(active(x)) -> f#(x) -> f#(active(x)) -> f#(x) f#(active(x)) -> f#(x) -> f#(active(x)) -> active#(f(x)) f#(active(x)) -> f#(x) -> f#(no(x)) -> f#(x) f#(active(x)) -> f#(x) -> f#(mark(x)) -> f#(x) f#(active(x)) -> active#(f(x)) -> active#(f(x)) -> f#(f(x)) active#(f(x)) -> f#(f(x)) -> f#(active(x)) -> f#(x) active#(f(x)) -> f#(f(x)) -> f#(active(x)) -> active#(f(x)) active#(f(x)) -> f#(f(x)) -> f#(no(x)) -> f#(x) active#(f(x)) -> f#(f(x)) -> f#(mark(x)) -> f#(x) SCC Processor: #sccs: 3 #rules: 7 #arcs: 66/1156 DPs: 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=3 interpretation: [tp#](x0) = [0 1 0]x0 + [1], [0 0 0] [0] [tp](x0) = [0 0 1]x0 + [1] [0 1 0] [1], [1] [c] = [1] [0], [0] [y] = [0] [0], [0 1 1] [0 1 1] [mat](x0, x1) = [0 0 0]x0 + [1 1 0]x1 [0 0 0] [1 0 0] , [0] [X] = [0] [1], [1 1 0] [1] [chk](x0) = [0 0 1]x0 + [0] [0 0 0] [1], [0 0 0] [0] [no](x0) = [1 1 0]x0 + [0] [0 0 1] [1], [0 0 0] [0] [mark](x0) = [1 0 0]x0 + [1] [0 0 0] [1], [0 0 0] [0] [active](x0) = [0 0 0]x0 + [1] [0 0 1] [1], [0 0 0] [f](x0) = [0 0 1]x0 [0 0 1] orientation: tp#(mark(x)) = [1 0 0]x + [2] >= [1 0 0]x + [1] = tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0] [0] [0] active(f(x)) = [0 0 0]x + [1] >= [1] = mark(f(f(x))) [0 0 1] [1] [1] [0 0 1] [1] [0] chk(no(f(x))) = [0 0 1]x + [1] >= [1] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [0 0 0] [1] [1] [0 0 2] [0] mat(f(x),f(y())) = [0 0 0]x >= [0] = f(mat(x,y())) [0 0 0] [0] [3] [0] chk(no(c())) = [1] >= [1] = active(c()) [1] [1] [0 0 2] [1] [0] mat(f(x),c()) = [0 0 0]x + [2] >= [2] = no(c()) [0 0 0] [1] [1] [0 0 0] [0] [0 0 0] [0] f(active(x)) = [0 0 1]x + [1] >= [0 0 0]x + [1] = active(f(x)) [0 0 1] [1] [0 0 1] [1] [0 0 0] [0] [0 0 0] [0] f(no(x)) = [0 0 1]x + [1] >= [0 0 1]x + [0] = no(f(x)) [0 0 1] [1] [0 0 1] [1] [0] [0] f(mark(x)) = [1] >= [1] = mark(f(x)) [1] [1] [0 0 0] [0] [0 0 0] [0] tp(mark(x)) = [0 0 0]x + [2] >= [0 0 0]x + [2] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) [1 0 0] [2] [1 0 0] [1] 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 DPs: chk#(no(f(x))) -> 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=1 interpretation: [chk#](x0) = 2x0 + 4, [tp](x0) = 0, [c] = 1, [y] = 0, [mat](x0, x1) = 4x1, [X] = 0, [chk](x0) = 0, [no](x0) = x0 + 1, [mark](x0) = 0, [active](x0) = 0, [f](x0) = 4x0 orientation: chk#(no(f(x))) = 8x + 6 >= 8x + 4 = chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) active(f(x)) = 0 >= 0 = mark(f(f(x))) chk(no(f(x))) = 0 >= 0 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) = 0 >= 0 = f(mat(x,y())) chk(no(c())) = 0 >= 0 = active(c()) mat(f(x),c()) = 4 >= 2 = no(c()) f(active(x)) = 0 >= 0 = active(f(x)) f(no(x)) = 4x + 4 >= 4x + 1 = no(f(x)) f(mark(x)) = 0 >= 0 = mark(f(x)) tp(mark(x)) = 0 >= 0 = 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 DPs: f#(mark(x)) -> f#(x) f#(no(x)) -> f#(x) f#(active(x)) -> active#(f(x)) active#(f(x)) -> f#(f(x)) f#(active(x)) -> f#(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=1 interpretation: [f#](x0) = 4x0, [active#](x0) = 4x0 + 1, [tp](x0) = 2, [c] = 0, [y] = 1, [mat](x0, x1) = 1, [X] = 7, [chk](x0) = 4x0, [no](x0) = 2x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 4, [f](x0) = x0 orientation: f#(mark(x)) = 4x + 4 >= 4x = f#(x) f#(no(x)) = 8x + 4 >= 4x = f#(x) f#(active(x)) = 4x + 16 >= 4x + 1 = active#(f(x)) active#(f(x)) = 4x + 1 >= 4x = f#(f(x)) f#(active(x)) = 4x + 16 >= 4x = f#(x) active(f(x)) = x + 4 >= x + 1 = mark(f(f(x))) chk(no(f(x))) = 8x + 4 >= 4 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) = 1 >= 1 = f(mat(x,y())) chk(no(c())) = 4 >= 4 = active(c()) mat(f(x),c()) = 1 >= 1 = no(c()) f(active(x)) = x + 4 >= x + 4 = active(f(x)) f(no(x)) = 2x + 1 >= 2x + 1 = no(f(x)) f(mark(x)) = x + 1 >= x + 1 = mark(f(x)) tp(mark(x)) = 2 >= 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