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 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: tp#_A(x1) = 0 mark_A(x1) = max{34, x1 - 41} chk_A(x1) = max{32, x1} mat_A(x1,x2) = max{26, x2 - 60} f_A(x1) = max{38, x1 - 39} X_A = 520 active_A(x1) = max{27, x1 - 4} no_A(x1) = max{21, x1} y_A = 137 c_A = 26 tp#!_A(x1) = max{85, x1 + 52} mark!_A(x1) = 13 chk!_A(x1) = x1 + 59 mat!_A(x1,x2) = max{10, x1 - 130, x2 - 27} f!_A(x1) = max{12, x1 - 8} X!_A = 9 active!_A(x1) = 13 no!_A(x1) = 10 y!_A = 70 c!_A = 9 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: tp#_A(x1) = max{0, x1 - 11} mark_A(x1) = max{0, x1 - 10} chk_A(x1) = 0 mat_A(x1,x2) = max{27, x2 - 8} f_A(x1) = x1 X_A = 2 active_A(x1) = max{0, x1 - 10} no_A(x1) = x1 + 18 y_A = 34 c_A = 9 tp#!_A(x1) = x1 + 19 mark!_A(x1) = 5 chk!_A(x1) = x1 + 3 mat!_A(x1,x2) = max{2, x2 - 1} f!_A(x1) = x1 + 5 X!_A = 22 active!_A(x1) = max{31, x1 + 5} no!_A(x1) = 1 y!_A = 40 c!_A = 32 partial status: pi(tp#) = [] pi(mark) = [] pi(chk) = [] pi(mat) = [] pi(f) = [] pi(X) = [] pi(active) = [] pi(no) = [1] pi(y) = [] pi(c) = [] 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, r5 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: chk#_A(x1) = max{0, x1 - 37} no_A(x1) = max{11, x1 - 444} f_A(x1) = max{10, x1 - 48} mat_A(x1,x2) = max{36, x1 - 11, x2 - 492} X_A = 5 y_A = 527 c_A = 0 chk#!_A(x1) = max{2, x1 - 33} no!_A(x1) = max{4, x1 - 1} f!_A(x1) = max{7, x1 - 626} mat!_A(x1,x2) = max{5, x1 - 541, x2 - 1057} X!_A = 6 y!_A = 8 c!_A = 6 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: chk#_A(x1) = max{0, x1 - 37} no_A(x1) = max{11, x1 - 213} f_A(x1) = max{10, x1 - 20} mat_A(x1,x2) = max{19, x1 - 12, x2 - 234} X_A = 248 y_A = 11 c_A = 0 chk#!_A(x1) = max{8, x1 - 221} no!_A(x1) = max{3, x1 - 1} f!_A(x1) = max{7, x1 - 523} mat!_A(x1,x2) = max{4, x1 - 570, x2 - 453} X!_A = 2 y!_A = 5 c!_A = 5 partial status: pi(chk#) = [1] pi(no) = [1] pi(f) = [] pi(mat) = [1] pi(X) = [] pi(y) = [] pi(c) = [] 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: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: active#_A(x1) = max{0, x1 - 8} f_A(x1) = max{7, x1 - 27} f#_A(x1) = max{0, x1 - 8} mark_A(x1) = x1 no_A(x1) = x1 active_A(x1) = max{2, x1} active#!_A(x1) = 8 f!_A(x1) = max{80, x1 - 128} f#!_A(x1) = max{80, x1 - 126} mark!_A(x1) = 7 no!_A(x1) = max{71, x1 - 127} active!_A(x1) = 8 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: active#_A(x1) = max{68, x1 - 3} f_A(x1) = x1 + 6 f#_A(x1) = max{68, x1 - 5} mark_A(x1) = x1 + 9 no_A(x1) = x1 + 79 active_A(x1) = x1 + 72 active#!_A(x1) = max{56, x1 - 2} f!_A(x1) = max{55, x1 - 8} f#!_A(x1) = max{5, x1 - 15} mark!_A(x1) = 68 no!_A(x1) = max{70, x1 - 170} active!_A(x1) = 69 partial status: pi(active#) = [1] pi(f) = [] pi(f#) = [] pi(mark) = [] pi(no) = [] pi(active) = [] The following rules are removed: p1, p3, p4, p5 -- 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 r5 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: f#_A(x1) = max{0, x1 - 3} mark_A(x1) = max{11, x1 + 2} mat_A(x1,x2) = max{11, x1 - 2, x2 - 204} f_A(x1) = max{0, x1 - 12} c_A = 2 no_A(x1) = max{1, x1 - 3} f#!_A(x1) = max{2, x1 - 221} mark!_A(x1) = max{2, x1 - 220} mat!_A(x1,x2) = max{2, x2 - 318} f!_A(x1) = max{2, x1 - 123} c!_A = 1 no!_A(x1) = max{2, x1 - 218} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: f#_A(x1) = max{0, x1 - 2} mark_A(x1) = x1 + 1 mat_A(x1,x2) = max{21, x1 - 2, x2 - 17} f_A(x1) = max{0, x1 - 22} c_A = 2 no_A(x1) = max{13, x1 - 3} f#!_A(x1) = max{3, x1 - 154} mark!_A(x1) = max{3, x1 - 153} mat!_A(x1,x2) = max{2, x2 - 226} f!_A(x1) = max{4, x1 - 199} c!_A = 1 no!_A(x1) = max{2, x1 - 203} partial status: pi(f#) = [1] pi(mark) = [1] pi(mat) = [] pi(f) = [] pi(c) = [] pi(no) = [] The following rules are removed: p1 Then no dependency pair remains.