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, >G) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: tp#_A(x1) = 2 mark_A(x1) = 3 chk_A(x1) = 7 mat_A(x1,x2) = x2 + 4 f_A(x1) = 6 X_A() = 1 active_A(x1) = x1 no_A(x1) = 3 y_A() = 1 c_A() = 2 tp_A(x1) = 2 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: tp#_A(x1) = max{0, x1 - 244} mark_A(x1) = max{243, x1 - 13} chk_A(x1) = x1 + 144 mat_A(x1,x2) = max{93, x1 - 10, x2 - 158} f_A(x1) = x1 + 6 X_A = 43 active_A(x1) = x1 + 237 no_A(x1) = x1 + 93 y_A = 347 c_A = 0 tp_A(x1) = max{0, x1 - 244} tp#!_A(x1) = max{236, x1 - 2} mark!_A(x1) = 3 chk!_A(x1) = x1 + 92 mat!_A(x1,x2) = max{97, x1 - 7} f!_A(x1) = max{191, x1 + 2} X!_A = 0 active!_A(x1) = max{186, x1 - 7} no!_A(x1) = 0 y!_A = 96 c!_A = 0 tp!_A(x1) = 0 partial status: pi(tp#) = [] pi(mark) = [] pi(chk) = [] pi(mat) = [] pi(f) = [] pi(X) = [] pi(active) = [1] 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, >G) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: chk#_A(x1) = 8 no_A(x1) = 2 f_A(x1) = 7 mat_A(x1,x2) = x2 + 5 X_A() = 1 y_A() = 6 chk_A(x1) = 4 c_A() = 3 active_A(x1) = 1 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: chk#_A(x1) = max{0, x1 - 255} no_A(x1) = max{2, x1 + 1} f_A(x1) = max{253, x1 - 30} mat_A(x1,x2) = max{253, x1 - 255} X_A = 324 y_A = 0 chk_A(x1) = x1 + 244 c_A = 0 active_A(x1) = max{2, x1 - 280} chk#!_A(x1) = x1 + 127 no!_A(x1) = max{2, x1 - 554} f!_A(x1) = max{4, x1 - 14} mat!_A(x1,x2) = max{x1 + 279, x2 + 5} X!_A = 1 y!_A = 4 chk!_A(x1) = 279 c!_A = 3 active!_A(x1) = max{1, x1 - 553} partial status: pi(chk#) = [] pi(no) = [] pi(f) = [] pi(mat) = [2] 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, >G) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: active#_A(x1) = x1 f_A(x1) = x1 f#_A(x1) = x1 mark_A(x1) = x1 no_A(x1) = x1 + 4 active_A(x1) = x1 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: active#_A(x1) = max{0, x1 - 50} f_A(x1) = max{17, x1} f#_A(x1) = max{0, x1 - 50} mark_A(x1) = max{2, x1} no_A(x1) = max{16, x1} active_A(x1) = max{49, x1} active#!_A(x1) = max{20, x1 + 2} f!_A(x1) = 0 f#!_A(x1) = x1 + 2 mark!_A(x1) = 0 no!_A(x1) = max{23, x1 + 5} active!_A(x1) = max{20, x1 + 2} partial status: pi(active#) = [] pi(f) = [1] pi(f#) = [] pi(mark) = [] pi(no) = [] pi(active) = [] The following rules are removed: p3 -- SCC decomposition. 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#(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, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: f#(active(x)) -> active#(f(x)) p3: f#(active(x)) -> f#(x) p4: 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 r1, r5, r6, r7, r8 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: active#_A(x1) = 1 f_A(x1) = 0 f#_A(x1) = x1 + 1 active_A(x1) = x1 mark_A(x1) = x1 mat_A(x1,x2) = 4 c_A() = 1 no_A(x1) = 0 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: active#_A(x1) = max{0, x1 - 37} f_A(x1) = x1 + 36 f#_A(x1) = max{0, x1 - 48} active_A(x1) = x1 + 47 mark_A(x1) = max{33, x1 + 11} mat_A(x1,x2) = max{20, x1 - 393, x2 - 38} c_A = 18 no_A(x1) = max{19, x1 - 37} active#!_A(x1) = max{45, x1 + 4} f!_A(x1) = 41 f#!_A(x1) = max{39, x1 - 1} active!_A(x1) = 38 mark!_A(x1) = 2 mat!_A(x1,x2) = max{43, x1 - 358, x2 - 364} c!_A = 42 no!_A(x1) = 0 partial status: pi(active#) = [] pi(f) = [] pi(f#) = [] pi(active) = [] pi(mark) = [] pi(mat) = [] pi(c) = [] pi(no) = [] The following rules are removed: p1, p2, p3 -- 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 (no rules) Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: f#_A(x1) = x1 mark_A(x1) = x1 + 39 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: f#_A(x1) = max{0, x1 - 1272} mark_A(x1) = x1 + 1271 f#!_A(x1) = max{1, x1 - 1550} mark!_A(x1) = max{220, x1 - 1549} partial status: pi(f#) = [1] pi(mark) = [1] The following rules are removed: p1 Then no dependency pair remains.