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))) 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))) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {12} transitions: tp{#,0}(24) -> 12* mark0(10) -> 5* mark0(5) -> 5* mark0(7) -> 5* mark0(2) -> 4,2,6,5 mark0(9) -> 5* mark0(4) -> 5* mark0(6) -> 5* mark0(1) -> 5* mark0(8) -> 5* mark0(3) -> 5* chk0(10) -> 4* chk0(5) -> 4* chk0(7) -> 4* chk0(2) -> 4* chk0(9) -> 4* chk0(4) -> 4* chk0(6) -> 4* chk0(1) -> 4* chk0(23) -> 24* chk0(8) -> 4* chk0(3) -> 4* mat0(2,10) -> 3* mat0(8,1) -> 3* mat0(3,1) -> 3* mat0(8,3) -> 3* mat0(3,3) -> 3* mat0(8,5) -> 3* mat0(3,5) -> 3* mat0(8,7) -> 3* mat0(3,7) -> 3* mat0(8,9) -> 3* mat0(3,9) -> 3* mat0(9,2) -> 3* mat0(4,2) -> 3* mat0(9,4) -> 3* mat0(4,4) -> 3* mat0(9,6) -> 3* mat0(4,6) -> 3* mat0(9,8) -> 3* mat0(4,8) -> 3* mat0(9,10) -> 3* mat0(4,10) -> 3* mat0(10,1) -> 3* mat0(5,1) -> 3* mat0(10,3) -> 3* mat0(5,3) -> 3* mat0(10,5) -> 3* mat0(5,5) -> 3* mat0(10,7) -> 3* mat0(5,7) -> 3* mat0(10,9) -> 3* mat0(5,9) -> 3* mat0(6,2) -> 3* mat0(1,2) -> 3* mat0(6,4) -> 3* mat0(21,8) -> 25* mat0(1,4) -> 3* mat0(6,6) -> 3* mat0(1,6) -> 3* mat0(6,8) -> 3* mat0(1,8) -> 3* mat0(6,10) -> 3* mat0(1,10) -> 3* mat0(7,1) -> 3* mat0(2,1) -> 3* mat0(7,3) -> 3* mat0(2,3) -> 3* mat0(7,5) -> 3* mat0(2,5) -> 3* mat0(7,7) -> 3* mat0(22,11) -> 23* mat0(2,7) -> 3* mat0(7,9) -> 3* mat0(2,9) -> 3* mat0(8,2) -> 3* mat0(3,2) -> 3* mat0(8,4) -> 3* mat0(3,4) -> 3* mat0(8,6) -> 3* mat0(3,6) -> 3* mat0(8,8) -> 3* mat0(3,8) -> 3* mat0(8,10) -> 3* mat0(3,10) -> 3* mat0(9,1) -> 3* mat0(4,1) -> 3* mat0(9,3) -> 3* mat0(4,3) -> 3* mat0(9,5) -> 3* mat0(4,5) -> 3* mat0(9,7) -> 3* mat0(4,7) -> 3* mat0(9,9) -> 3* mat0(4,9) -> 3* mat0(10,2) -> 3* mat0(5,2) -> 3* mat0(10,4) -> 3* mat0(5,4) -> 3* mat0(10,6) -> 3* mat0(5,6) -> 3* mat0(10,8) -> 3* mat0(5,8) -> 3* mat0(10,10) -> 3* mat0(5,10) -> 3* mat0(6,1) -> 3* mat0(1,1) -> 3* mat0(6,3) -> 3* mat0(1,3) -> 3* mat0(6,5) -> 3* mat0(1,5) -> 3* mat0(6,7) -> 3* mat0(1,7) -> 3* mat0(6,9) -> 3* mat0(1,9) -> 3* mat0(7,2) -> 3* mat0(2,2) -> 3* mat0(7,4) -> 3* mat0(2,4) -> 3* mat0(7,6) -> 3* mat0(2,6) -> 3* mat0(7,8) -> 3* mat0(2,8) -> 3* mat0(7,10) -> 3* f0(25) -> 23* f0(20) -> 21* f0(15) -> 16* f0(10) -> 2* f0(5) -> 2* f0(17) -> 18* f0(7) -> 2* f0(2) -> 2* f0(19) -> 20* f0(14) -> 15* f0(9) -> 2* f0(4) -> 4,2 f0(21) -> 22* f0(16) -> 17* f0(6) -> 2* f0(1) -> 13,2 f0(18) -> 19* f0(13) -> 14* f0(8) -> 2* f0(3) -> 3,2 X0() -> 1* active0(10) -> 6* active0(5) -> 6* active0(7) -> 6* active0(2) -> 4,2,6 active0(9) -> 24,4,6 active0(4) -> 6* active0(6) -> 6* active0(1) -> 6* active0(8) -> 6* active0(3) -> 6* no0(10) -> 7* no0(5) -> 7* no0(7) -> 7* no0(2) -> 3,2,7 no0(9) -> 23,3,7 no0(4) -> 7* no0(6) -> 7* no0(1) -> 7* no0(8) -> 7* no0(3) -> 7* y0() -> 8* c0() -> 9* tp0(10) -> 10* tp0(5) -> 10* tp0(7) -> 10* tp0(2) -> 10* tp0(9) -> 10* tp0(4) -> 10* tp0(6) -> 10* tp0(1) -> 10* tp0(8) -> 10* tp0(3) -> 10* 1 -> 11* 2 -> 11* 3 -> 11* 4 -> 11* 5 -> 11* 6 -> 11* 7 -> 11* 8 -> 11* 9 -> 11* 10 -> 11* 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))) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {12} transitions: no0(10) -> 4* no0(5) -> 4* no0(7) -> 4* no0(2) -> 4* no0(9) -> 2,23,4 no0(4) -> 4* no0(6) -> 4* no0(1) -> 4* no0(8) -> 4* no0(3) -> 2,3,4 y0() -> 8* c0() -> 9* tp0(10) -> 10* tp0(5) -> 10* tp0(7) -> 10* tp0(2) -> 10* tp0(9) -> 10* tp0(4) -> 10* tp0(6) -> 10* tp0(1) -> 10* tp0(8) -> 10* tp0(3) -> 10* chk{#,0}(23) -> 12* mark0(10) -> 6* mark0(5) -> 6* mark0(7) -> 6* mark0(2) -> 6* mark0(9) -> 6* mark0(4) -> 6* mark0(6) -> 6* mark0(1) -> 6* mark0(8) -> 6* mark0(3) -> 7,3,5,6 chk0(10) -> 7* chk0(5) -> 7* chk0(7) -> 7* chk0(2) -> 7* chk0(9) -> 7* chk0(4) -> 7* chk0(6) -> 7* chk0(1) -> 7* chk0(8) -> 7* chk0(3) -> 7* mat0(2,10) -> 2* mat0(8,1) -> 2* mat0(3,1) -> 2* mat0(8,3) -> 2* mat0(3,3) -> 2* mat0(8,5) -> 2* mat0(3,5) -> 2* mat0(8,7) -> 2* mat0(3,7) -> 2* mat0(8,9) -> 2* mat0(3,9) -> 2* mat0(9,2) -> 2* mat0(4,2) -> 2* mat0(9,4) -> 2* mat0(4,4) -> 2* mat0(9,6) -> 2* mat0(4,6) -> 2* mat0(9,8) -> 2* mat0(4,8) -> 2* mat0(9,10) -> 2* mat0(4,10) -> 2* mat0(10,1) -> 2* mat0(5,1) -> 2* mat0(10,3) -> 2* mat0(5,3) -> 2* mat0(10,5) -> 2* mat0(5,5) -> 2* mat0(10,7) -> 2* mat0(5,7) -> 2* mat0(10,9) -> 2* mat0(5,9) -> 2* mat0(6,2) -> 2* mat0(1,2) -> 2* mat0(6,4) -> 2* mat0(21,8) -> 24* mat0(1,4) -> 2* mat0(6,6) -> 2* mat0(1,6) -> 2* mat0(6,8) -> 2* mat0(1,8) -> 2* mat0(6,10) -> 2* mat0(1,10) -> 2* mat0(7,1) -> 2* mat0(2,1) -> 2* mat0(7,3) -> 2* mat0(2,3) -> 2* mat0(7,5) -> 2* mat0(2,5) -> 2* mat0(7,7) -> 2* mat0(22,11) -> 23* mat0(2,7) -> 2* mat0(7,9) -> 2* mat0(2,9) -> 2* mat0(8,2) -> 2* mat0(3,2) -> 2* mat0(8,4) -> 2* mat0(3,4) -> 2* mat0(8,6) -> 2* mat0(3,6) -> 2* mat0(8,8) -> 2* mat0(3,8) -> 2* mat0(8,10) -> 2* mat0(3,10) -> 2* mat0(9,1) -> 2* mat0(4,1) -> 2* mat0(9,3) -> 2* mat0(4,3) -> 2* mat0(9,5) -> 2* mat0(4,5) -> 2* mat0(9,7) -> 2* mat0(4,7) -> 2* mat0(9,9) -> 2* mat0(4,9) -> 2* mat0(10,2) -> 2* mat0(5,2) -> 2* mat0(10,4) -> 2* mat0(5,4) -> 2* mat0(10,6) -> 2* mat0(5,6) -> 2* mat0(10,8) -> 2* mat0(5,8) -> 2* mat0(10,10) -> 2* mat0(5,10) -> 2* mat0(6,1) -> 2* mat0(1,1) -> 2* mat0(6,3) -> 2* mat0(1,3) -> 2* mat0(6,5) -> 2* mat0(1,5) -> 2* mat0(6,7) -> 2* mat0(1,7) -> 2* mat0(6,9) -> 2* mat0(1,9) -> 2* mat0(7,2) -> 2* mat0(2,2) -> 2* mat0(7,4) -> 2* mat0(2,4) -> 2* mat0(7,6) -> 2* mat0(2,6) -> 2* mat0(7,8) -> 2* mat0(2,8) -> 2* mat0(7,10) -> 2* f0(20) -> 21* f0(15) -> 16* f0(10) -> 3* f0(5) -> 3* f0(17) -> 18* f0(7) -> 7,3 f0(2) -> 2,3 f0(24) -> 23* f0(19) -> 20* f0(14) -> 15* f0(9) -> 3* f0(4) -> 3* f0(21) -> 22* f0(16) -> 17* f0(6) -> 3* f0(1) -> 13,3 f0(18) -> 19* f0(13) -> 14* f0(8) -> 3* f0(3) -> 3* X0() -> 1* active0(10) -> 5* active0(5) -> 5* active0(7) -> 5* active0(2) -> 5* active0(9) -> 7,5 active0(4) -> 5* active0(6) -> 5* active0(1) -> 5* active0(8) -> 5* active0(3) -> 7,3,5 1 -> 11* 2 -> 11* 3 -> 11* 4 -> 11* 5 -> 11* 6 -> 11* 7 -> 11* 8 -> 11* 9 -> 11* 10 -> 11* 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: dimension: 1 interpretation: [f#](x0) = x0 + 1, [active#](x0) = x0 + 1, [tp](x0) = 0, [c] = 0, [y] = 0, [mat](x0, x1) = 1, [X] = 0, [chk](x0) = 1, [no](x0) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [f](x0) = x0 orientation: f#(mark(x)) = x + 2 >= x + 1 = f#(x) f#(no(x)) = x + 2 >= x + 1 = f#(x) f#(active(x)) = x + 2 >= x + 1 = active#(f(x)) active#(f(x)) = x + 1 >= x + 1 = f#(f(x)) f#(active(x)) = x + 2 >= x + 1 = f#(x) active(f(x)) = x + 1 >= x + 1 = mark(f(f(x))) chk(no(f(x))) = 1 >= 1 = 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())) = 1 >= 1 = active(c()) mat(f(x),c()) = 1 >= 1 = no(c()) f(active(x)) = x + 1 >= x + 1 = active(f(x)) f(no(x)) = x + 1 >= x + 1 = no(f(x)) f(mark(x)) = x + 1 >= x + 1 = 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: active#(f(x)) -> f#(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: dimension: 1 interpretation: [f#](x0) = 0, [active#](x0) = 1, [tp](x0) = 0, [c] = 0, [y] = 0, [mat](x0, x1) = 0, [X] = 0, [chk](x0) = 0, [no](x0) = 0, [mark](x0) = 0, [active](x0) = 0, [f](x0) = 0 orientation: active#(f(x)) = 1 >= 0 = f#(f(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()) = 0 >= 0 = no(c()) f(active(x)) = 0 >= 0 = active(f(x)) f(no(x)) = 0 >= 0 = 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