MAYBE 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()) CDG 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()) 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) Restore Modifier: 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))) 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))) Open 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))) Open 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))) Open