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) SCC Processor: #sccs: 4 #rules: 8 #arcs: 153/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))) CDG Processor: 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))) graph: 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))) CDG Processor: 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))) graph: Qed DPs: mat#(f(x),f(y())) -> mat#(x,y()) 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))) Subterm Criterion Processor: simple projection: pi(mat#) = 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: f#(active(x)) -> f#(x) f#(active(x)) -> active#(f(x)) active#(f(x)) -> f#(f(x)) f#(no(x)) -> f#(x) f#(mark(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))) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0) = 1x0 + 1, [active#](x0) = 1x0 + 0, [tp](x0) = x0 + 0, [c] = 0, [y] = 2, [mat](x0, x1) = 6x0 + 0, [X] = 0, [chk](x0) = 0, [no](x0) = 6x0 + 6, [mark](x0) = x0 + 0, [active](x0) = x0, [f](x0) = x0 + 0 orientation: f#(active(x)) = 1x + 1 >= 1x + 1 = f#(x) f#(active(x)) = 1x + 1 >= 1x + 1 = active#(f(x)) active#(f(x)) = 1x + 1 >= 1x + 1 = f#(f(x)) f#(no(x)) = 7x + 7 >= 1x + 1 = f#(x) f#(mark(x)) = 1x + 1 >= 1x + 1 = f#(x) active(f(x)) = x + 0 >= x + 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())) = 6x + 6 >= 6x + 0 = f(mat(x,y())) chk(no(c())) = 0 >= 0 = active(c()) mat(f(x),c()) = 6x + 6 >= 6 = no(c()) f(active(x)) = x + 0 >= x + 0 = active(f(x)) f(no(x)) = 6x + 6 >= 6x + 6 = no(f(x)) f(mark(x)) = x + 0 >= x + 0 = mark(f(x)) tp(mark(x)) = x + 0 >= 0 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) problem: DPs: f#(active(x)) -> f#(x) f#(active(x)) -> active#(f(x)) active#(f(x)) -> f#(f(x)) f#(mark(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))) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0) = x0, [active#](x0) = 2x0 + 0, [tp](x0) = 1, [c] = 2, [y] = 2, [mat](x0, x1) = x0 + 2, [X] = 0, [chk](x0) = x0 + 5, [no](x0) = x0 + 1, [mark](x0) = 2x0 + 0, [active](x0) = 3x0 + 0, [f](x0) = x0 orientation: f#(active(x)) = 3x + 0 >= x = f#(x) f#(active(x)) = 3x + 0 >= 2x + 0 = active#(f(x)) active#(f(x)) = 2x + 0 >= x = f#(f(x)) f#(mark(x)) = 2x + 0 >= x = f#(x) active(f(x)) = 3x + 0 >= 2x + 0 = mark(f(f(x))) chk(no(f(x))) = x + 5 >= 5 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) = x + 2 >= x + 2 = f(mat(x,y())) chk(no(c())) = 5 >= 5 = active(c()) mat(f(x),c()) = x + 2 >= 2 = no(c()) f(active(x)) = 3x + 0 >= 3x + 0 = active(f(x)) f(no(x)) = x + 1 >= x + 1 = no(f(x)) f(mark(x)) = 2x + 0 >= 2x + 0 = mark(f(x)) tp(mark(x)) = 1 >= 1 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) problem: DPs: f#(active(x)) -> active#(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))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 17/1