YES We show the termination of the TRS R: 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 decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) p3: chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) p4: chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) p5: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) p6: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) p7: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) p8: chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) p9: chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) p10: chk#(no(f(x))) -> f#(f(f(f(f(X()))))) p11: chk#(no(f(x))) -> f#(f(f(f(X())))) p12: chk#(no(f(x))) -> f#(f(f(X()))) p13: chk#(no(f(x))) -> f#(f(X())) p14: chk#(no(f(x))) -> f#(X()) p15: mat#(f(x),f(y())) -> f#(mat(x,y())) p16: mat#(f(x),f(y())) -> mat#(x,y()) p17: chk#(no(c())) -> active#(c()) p18: f#(active(x)) -> active#(f(x)) p19: f#(active(x)) -> f#(x) p20: f#(no(x)) -> f#(x) p21: f#(mark(x)) -> f#(x) p22: tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) p23: tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) p24: tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) p25: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) p26: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) p27: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) p28: tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) p29: tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) p30: tp#(mark(x)) -> f#(f(f(f(f(X()))))) p31: tp#(mark(x)) -> f#(f(f(f(X())))) p32: tp#(mark(x)) -> f#(f(f(X()))) p33: tp#(mark(x)) -> f#(f(X())) p34: tp#(mark(x)) -> f#(X()) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The estimated dependency graph contains the following SCCs: {p22} {p3} {p1, p18, p19, p20, p21} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: tp#_A(x1) = x1 + 30 mark_A(x1) = max{52, x1 - 9} chk_A(x1) = max{22, x1 + 7} mat_A(x1,x2) = max{2, x1 - 89, x2 - 78} f_A(x1) = max{81, x1 - 82} X_A = 23 active_A(x1) = max{1, x1} no_A(x1) = max{1, x1 - 2} y_A = 242 c_A = 1 tp_A(x1) = max{24, x1 - 61} base order 2: precedence: mat > f > mark = y > tp# = tp > chk > c > no > X = active partial status: pi(tp#) = [1] pi(mark) = [] pi(chk) = [] pi(mat) = [] pi(f) = [] pi(X) = [] pi(active) = [] pi(no) = [] pi(y) = [] pi(c) = [] pi(tp) = [] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r3, r4, r5 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: chk#_A(x1) = x1 + 113 no_A(x1) = max{9, x1 - 94} f_A(x1) = max{419, x1 - 10} mat_A(x1,x2) = max{7, x1 - 208, x2 - 423} X_A = 97 y_A = 852 chk_A(x1) = max{1, x1 - 214} c_A = 93 active_A(x1) = max{1, x1 - 427} base order 2: precedence: c > no > chk# > mat = y > f > X > chk > active partial status: pi(chk#) = [1] pi(no) = [] pi(f) = [] pi(mat) = [] pi(X) = [] pi(y) = [] pi(chk) = [] pi(c) = [] pi(active) = [] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: f#(mark(x)) -> f#(x) p3: f#(no(x)) -> f#(x) p4: f#(active(x)) -> f#(x) p5: f#(active(x)) -> active#(f(x)) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r1, r6, r7, r8 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: active#_A(x1) = max{6, x1 + 2} f_A(x1) = max{3, x1} f#_A(x1) = max{6, x1 + 1} mark_A(x1) = x1 no_A(x1) = max{1, x1} active_A(x1) = max{11, x1 + 7} base order 2: precedence: f = no > mark > active > active# > f# partial status: pi(active#) = [] pi(f) = [] pi(f#) = [] pi(mark) = [] pi(no) = [] pi(active) = [1] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(mark(x)) -> f#(x) p2: f#(no(x)) -> f#(x) p3: f#(active(x)) -> f#(x) p4: f#(active(x)) -> active#(f(x)) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: f#(mark(x)) -> f#(x) p2: f#(active(x)) -> f#(x) p3: f#(no(x)) -> f#(x) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r3, r5 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: f#_A(x1) = max{6, x1 + 2} mark_A(x1) = x1 + 24 active_A(x1) = max{8, x1 + 5} no_A(x1) = max{19, x1 + 7} mat_A(x1,x2) = max{23, x1 - 19, x2 - 111} f_A(x1) = max{8, x1 - 33} y_A = 7 c_A = 15 base order 2: precedence: active > no > mark = mat = f = c > f# = y partial status: pi(f#) = [1] pi(mark) = [1] pi(active) = [] pi(no) = [] pi(mat) = [] pi(f) = [] pi(y) = [] pi(c) = [] The following rules are removed: p3 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(mark(x)) -> f#(x) p2: f#(active(x)) -> f#(x) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: f#(mark(x)) -> f#(x) p2: f#(active(x)) -> f#(x) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r4, r5 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: f#_A(x1) = max{1, x1 - 1} mark_A(x1) = x1 + 21 active_A(x1) = max{16, x1 + 3} chk_A(x1) = max{17, x1 - 36} no_A(x1) = max{10, x1 - 344} c_A = 11 mat_A(x1,x2) = max{18, x1 - 209, x2 - 27} f_A(x1) = max{12, x1 - 34} base order 2: precedence: mark = active > f# > mat > f > chk = c > no partial status: pi(f#) = [] pi(mark) = [1] pi(active) = [1] pi(chk) = [] pi(no) = [] pi(c) = [] pi(mat) = [] pi(f) = [] The following rules are removed: p2 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(mark(x)) -> f#(x) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: f#(mark(x)) -> f#(x) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r4, r5 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: f#_A(x1) = max{14, x1 - 1} mark_A(x1) = x1 + 19 chk_A(x1) = max{15, x1 - 37} no_A(x1) = max{1, x1 - 292} c_A = 2 active_A(x1) = max{4, x1 - 4} mat_A(x1,x2) = max{14, x1 - 14, x2 - 354} f_A(x1) = max{3, x1 - 24} base order 2: precedence: mark > f# > chk > active = mat > f > c > no partial status: pi(f#) = [] pi(mark) = [1] pi(chk) = [] pi(no) = [] pi(c) = [] pi(active) = [] pi(mat) = [] pi(f) = [] The following rules are removed: p1 Then no dependency pair remains.