YES We show the termination of the TRS R: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_var(x),Id()) -> Term_var(x) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Id(),s) -> s -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) p2: Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) p3: Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) p4: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) p5: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) p6: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) p7: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) p8: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) p9: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) p10: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) p11: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) p12: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) p13: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) p14: Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) p15: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) p16: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) p17: Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s) p18: Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s) p19: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) p20: Concat#(Concat(s,t),u) -> Concat#(t,u) p21: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) p22: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) p23: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The estimated dependency graph contains the following SCCs: {p1, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p15, p16, p19, p20, p21, p22, p23} {p17, p18} {p13, p14} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) p2: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) p3: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) p4: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) p5: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) p6: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) p7: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) p8: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) p9: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) p10: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) p11: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) p12: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) p13: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) p14: Concat#(Concat(s,t),u) -> Concat#(t,u) p15: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) p16: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) p17: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) p18: Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The set of usable rules consists of r9, r10, r14, r15, r16, r17, r21 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: Term_sub#_A(x1,x2) = 1 Case_A(x1,x2,x3) = max{53, x1 + 36, x2 + 19, x3 + 21} Frozen#_A(x1,x2,x3,x4) = max{1, x2 - 17} Sum_sub_A(x1,x2) = 16 Sum_term_var_A(x1) = 11 Term_sub_A(x1,x2) = max{40, x1 + 2, x2 + 31} Concat#_A(x1,x2) = 1 Cons_sum_A(x1,x2,x3) = x3 + 14 Cons_usual_A(x1,x2,x3) = max{x2 - 3, x3 + 12} Concat_A(x1,x2) = max{12, x1, x2} Term_inr_A(x1) = max{18, x1 + 1} Term_inl_A(x1) = x1 + 48 Term_pair_A(x1,x2) = max{x1 + 20, x2 + 1} Term_app_A(x1,x2) = max{x1 + 10, x2 + 47} Sum_constant_A(x1) = 14 Right_A = 0 Left_A = 0 Term_var_A(x1) = max{48, x1 - 3} Id_A = 15 Term_sub#!_A(x1,x2) = max{29, x1 - 19} Case!_A(x1,x2,x3) = max{36, x1 + 15, x2 + 15, x3 + 15} Frozen#!_A(x1,x2,x3,x4) = max{x1 - 19, x2 + 18, x3 + 1} Sum_sub!_A(x1,x2) = max{35, x1 - 1, x2 + 1} Sum_term_var!_A(x1) = max{30, x1 - 2} Term_sub!_A(x1,x2) = max{33, x2 - 15} Concat#!_A(x1,x2) = max{29, x1 - 13} Cons_sum!_A(x1,x2,x3) = max{0, x1 - 17, x3 - 28} Cons_usual!_A(x1,x2,x3) = max{36, x2 - 3, x3} Concat!_A(x1,x2) = max{33, x2 - 15} Term_inr!_A(x1) = 34 Term_inl!_A(x1) = 32 Term_pair!_A(x1,x2) = x2 Term_app!_A(x1,x2) = max{34, x2 - 41} Sum_constant!_A(x1) = 34 Right!_A = 34 Left!_A = 30 Term_var!_A(x1) = 32 Id!_A = 31 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: Term_sub#_A(x1,x2) = 2 Case_A(x1,x2,x3) = max{41, x1 + 5, x2 + 19, x3 + 7} Frozen#_A(x1,x2,x3,x4) = 2 Sum_sub_A(x1,x2) = max{33, x1} Sum_term_var_A(x1) = max{33, x1} Term_sub_A(x1,x2) = max{x1 + 44, x2 - 4} Concat#_A(x1,x2) = 2 Cons_sum_A(x1,x2,x3) = max{22, x3} Cons_usual_A(x1,x2,x3) = max{22, x2 + 4, x3} Concat_A(x1,x2) = max{45, x1 + 22, x2} Term_inr_A(x1) = max{52, x1 + 7} Term_inl_A(x1) = max{5, x1} Term_pair_A(x1,x2) = max{53, x1 + 6, x2} Term_app_A(x1,x2) = max{x1 + 7, x2 + 3} Sum_constant_A(x1) = 1 Right_A = 0 Left_A = 1 Term_var_A(x1) = 43 Id_A = 0 Term_sub#!_A(x1,x2) = max{34, x1 - 18} Case!_A(x1,x2,x3) = max{x1 + 35, x2 + 36, x3 - 1} Frozen#!_A(x1,x2,x3,x4) = max{34, x1 - 17, x2 + 1, x3 - 18} Sum_sub!_A(x1,x2) = x1 + 79 Sum_term_var!_A(x1) = max{78, x1 + 36} Term_sub!_A(x1,x2) = 35 Concat#!_A(x1,x2) = max{34, x1 - 22} Cons_sum!_A(x1,x2,x3) = max{1, x3 - 46} Cons_usual!_A(x1,x2,x3) = max{0, x1 - 1, x2 - 1, x3 - 23} Concat!_A(x1,x2) = 35 Term_inr!_A(x1) = 36 Term_inl!_A(x1) = max{0, x1 - 7} Term_pair!_A(x1,x2) = max{47, x1 + 5, x2 - 43} Term_app!_A(x1,x2) = max{0, x1 - 45, x2 - 47} Sum_constant!_A(x1) = 36 Right!_A = 36 Left!_A = 36 Term_var!_A(x1) = x1 + 35 Id!_A = 1 partial status: pi(Term_sub#) = [] pi(Case) = [2] pi(Frozen#) = [] pi(Sum_sub) = [] pi(Sum_term_var) = [] pi(Term_sub) = [2] pi(Concat#) = [] pi(Cons_sum) = [1, 2, 3] pi(Cons_usual) = [1, 2, 3] pi(Concat) = [1, 2] pi(Term_inr) = [] pi(Term_inl) = [1] pi(Term_pair) = [2] pi(Term_app) = [2] pi(Sum_constant) = [] pi(Right) = [] pi(Left) = [] pi(Term_var) = [] pi(Id) = [] The following rules are removed: p11, p17 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) p2: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) p3: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) p4: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) p5: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) p6: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) p7: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) p8: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) p9: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) p10: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) p11: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) p12: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) p13: Concat#(Concat(s,t),u) -> Concat#(t,u) p14: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) p15: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) p16: Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) p2: Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) p3: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) p4: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) p5: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) p6: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) p7: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) p8: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) p9: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) p10: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) p11: Concat#(Concat(s,t),u) -> Concat#(t,u) p12: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) p13: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) p14: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) p15: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) p16: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The set of usable rules consists of r9, r10, r14, r15, r16, r17 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: Term_sub#_A(x1,x2) = 43 Case_A(x1,x2,x3) = max{x1 + 8, x2 + 54, x3 + 54} Frozen#_A(x1,x2,x3,x4) = 43 Sum_sub_A(x1,x2) = max{71, x1 + 1} Sum_constant_A(x1) = 1 Left_A = 1 Term_app_A(x1,x2) = max{62, x1 + 54, x2 + 54} Term_pair_A(x1,x2) = max{62, x1 - 9, x2 + 54} Term_inl_A(x1) = max{62, x1 + 54} Term_inr_A(x1) = max{61, x1 + 54} Term_sub_A(x1,x2) = max{x1 + 6, x2 + 8} Concat_A(x1,x2) = max{39, x1 - 2} Concat#_A(x1,x2) = 43 Cons_usual_A(x1,x2,x3) = max{44, x1 - 7, x2 - 7, x3 + 3} Cons_sum_A(x1,x2,x3) = max{44, x1 - 7, x2 - 39} Sum_term_var_A(x1) = max{1, x1 - 40} Term_var_A(x1) = max{55, x1 - 7} Id_A = 2 Term_sub#!_A(x1,x2) = max{71, x1 + 10} Case!_A(x1,x2,x3) = max{x1 + 73, x2 + 73, x3 + 73} Frozen#!_A(x1,x2,x3,x4) = max{x1 + 72, x2 - 1, x3 + 72} Sum_sub!_A(x1,x2) = 0 Sum_constant!_A(x1) = 0 Left!_A = 0 Term_app!_A(x1,x2) = max{72, x1 + 9, x2 + 9} Term_pair!_A(x1,x2) = max{1, x1 - 9, x2 - 9} Term_inl!_A(x1) = max{1, x1 - 5} Term_inr!_A(x1) = max{0, x1 - 9} Term_sub!_A(x1,x2) = 0 Concat!_A(x1,x2) = max{73, x1 - 45, x2 + 35} Concat#!_A(x1,x2) = 0 Cons_usual!_A(x1,x2,x3) = max{72, x1 - 53, x2 + 70} Cons_sum!_A(x1,x2,x3) = x1 + 1 Sum_term_var!_A(x1) = 0 Term_var!_A(x1) = 0 Id!_A = 1 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: Term_sub#_A(x1,x2) = max{194, x1 - 20} Case_A(x1,x2,x3) = max{211, x1 + 169, x2 + 171, x3 + 20} Frozen#_A(x1,x2,x3,x4) = max{194, x1 - 20, x2 - 2, x3 - 20} Sum_sub_A(x1,x2) = max{194, x1 - 1} Sum_constant_A(x1) = 1 Left_A = 0 Term_app_A(x1,x2) = max{169, x1 + 69, x2 + 110} Term_pair_A(x1,x2) = max{51, x1 - 59, x2 + 28} Term_inl_A(x1) = x1 + 28 Term_inr_A(x1) = max{20, x1} Term_sub_A(x1,x2) = max{x1 + 58, x2 + 41} Concat_A(x1,x2) = max{59, x1, x2} Concat#_A(x1,x2) = max{194, x1 + 21} Cons_usual_A(x1,x2,x3) = max{60, x1 - 20, x2 - 20, x3} Cons_sum_A(x1,x2,x3) = max{60, x1 - 20, x2, x3 + 1} Sum_term_var_A(x1) = max{1, x1 - 1} Term_var_A(x1) = 51 Id_A = 1 Term_sub#!_A(x1,x2) = max{119, x1 + 92} Case!_A(x1,x2,x3) = max{305, x1 + 115, x2 + 1, x3 + 113} Frozen#!_A(x1,x2,x3,x4) = max{304, x1 + 93, x3 + 112} Sum_sub!_A(x1,x2) = 118 Sum_constant!_A(x1) = 1 Left!_A = 120 Term_app!_A(x1,x2) = max{118, x2 - 1} Term_pair!_A(x1,x2) = max{x1 - 131, x2 + 4} Term_inl!_A(x1) = max{6, x1 - 42} Term_inr!_A(x1) = x1 + 4 Term_sub!_A(x1,x2) = max{5, x1 - 52} Concat!_A(x1,x2) = max{0, x1 - 61, x2 - 142} Concat#!_A(x1,x2) = 4 Cons_usual!_A(x1,x2,x3) = max{139, x2 + 120, x3 - 141} Cons_sum!_A(x1,x2,x3) = max{x1 + 6, x2 + 3} Sum_term_var!_A(x1) = max{133, x1 + 2} Term_var!_A(x1) = 4 Id!_A = 134 partial status: pi(Term_sub#) = [1] pi(Case) = [1, 2, 3] pi(Frozen#) = [1, 3] pi(Sum_sub) = [1, 2] pi(Sum_constant) = [] pi(Left) = [] pi(Term_app) = [1, 2] pi(Term_pair) = [2] pi(Term_inl) = [1] pi(Term_inr) = [1] pi(Term_sub) = [1, 2] pi(Concat) = [1, 2] pi(Concat#) = [1] pi(Cons_usual) = [2, 3] pi(Cons_sum) = [1, 2, 3] pi(Sum_term_var) = [] pi(Term_var) = [] pi(Id) = [] The following rules are removed: p1, p2, p3, p4, p5, p6, p8, p9, p11, p12, p14, p15, p16 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) p2: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) p3: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s 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: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The set of usable rules consists of (no rules) 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: Term_sub#_A(x1,x2) = max{0, x1 - 35} Term_inr_A(x1) = max{37, x1 + 34} Term_sub#!_A(x1,x2) = max{5, x1 - 38, x2 - 1} Term_inr!_A(x1) = 4 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: Term_sub#_A(x1,x2) = max{0, x1 - 2} Term_inr_A(x1) = max{26, x1 + 1} Term_sub#!_A(x1,x2) = max{6, x1 - 65, x2 - 1} Term_inr!_A(x1) = max{5, x1 - 64} partial status: pi(Term_sub#) = [1] pi(Term_inr) = [1] 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: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) p2: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The set of usable rules consists of r18, r19, r20, r21 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: Concat#_A(x1,x2) = max{0, x1 - 15, x2 - 21} Concat_A(x1,x2) = max{14, x1 + 6, x2} Cons_usual_A(x1,x2,x3) = max{7, x1 - 24, x3} Term_sub_A(x1,x2) = max{9, x1 + 6, x2 + 6} Cons_sum_A(x1,x2,x3) = max{15, x1 - 12, x2 - 8, x3 - 15} Id_A = 7 Concat#!_A(x1,x2) = max{x1 + 6, x2 - 21} Concat!_A(x1,x2) = max{24, x1 + 9, x2 - 15} Cons_usual!_A(x1,x2,x3) = max{0, x1 - 17, x3 - 30} Term_sub!_A(x1,x2) = 25 Cons_sum!_A(x1,x2,x3) = max{0, x3 - 16} Id!_A = 2 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: Concat#_A(x1,x2) = max{0, x1 - 9, x2 - 11} Concat_A(x1,x2) = max{8, x1 + 2, x2} Cons_usual_A(x1,x2,x3) = max{x1 - 3, x3} Term_sub_A(x1,x2) = max{5, x1 + 2, x2 + 3} Cons_sum_A(x1,x2,x3) = max{x1, x2 - 4, x3 - 4} Id_A = 0 Concat#!_A(x1,x2) = max{2, x1 - 9, x2 - 16} Concat!_A(x1,x2) = max{1, x1 - 10, x2 - 12} Cons_usual!_A(x1,x2,x3) = max{0, x1 - 4, x3 - 11} Term_sub!_A(x1,x2) = 3 Cons_sum!_A(x1,x2,x3) = max{0, x1 - 11, x2 - 15, x3 - 17} Id!_A = 1 partial status: pi(Concat#) = [1] pi(Concat) = [1, 2] pi(Cons_usual) = [3] pi(Term_sub) = [] pi(Cons_sum) = [2] pi(Id) = [] The following rules are removed: p1, p2 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s) p2: Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The set of usable rules consists of (no rules) 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: Sum_sub#_A(x1,x2) = max{0, x2 - 14} Cons_sum_A(x1,x2,x3) = max{14, x1 - 30, x2 - 30, x3 + 13} Cons_usual_A(x1,x2,x3) = max{3, x1 - 30, x2 - 30, x3 + 1} Sum_sub#!_A(x1,x2) = max{1, x2 - 12} Cons_sum!_A(x1,x2,x3) = max{2, x1 - 11, x2 - 47, x3 - 11} Cons_usual!_A(x1,x2,x3) = max{0, x1 - 51, x2 - 54, x3 - 51} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: Sum_sub#_A(x1,x2) = max{0, x2 - 17} Cons_sum_A(x1,x2,x3) = max{x1 - 1, x2 - 6, x3 + 16} Cons_usual_A(x1,x2,x3) = max{32, x1 - 19, x2 - 6, x3 + 1} Sum_sub#!_A(x1,x2) = max{2, x1 - 1, x2 - 37} Cons_sum!_A(x1,x2,x3) = max{1, x1 - 19, x2 - 38, x3 - 38} Cons_usual!_A(x1,x2,x3) = max{1, x1 - 51, x2 - 55, x3 - 51} partial status: pi(Sum_sub#) = [] pi(Cons_sum) = [1] pi(Cons_usual) = [3] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The set of usable rules consists of (no rules) 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: Sum_sub#_A(x1,x2) = max{0, x2 - 27} Cons_usual_A(x1,x2,x3) = max{x1 - 29, x2 - 5, x3 + 26} Sum_sub#!_A(x1,x2) = max{1, x2 - 24} Cons_usual!_A(x1,x2,x3) = max{2, x1 - 6, x2 - 4, x3 - 5} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: Sum_sub#_A(x1,x2) = max{0, x2 - 2} Cons_usual_A(x1,x2,x3) = max{3, x1 - 8, x2 - 8, x3 + 1} Sum_sub#!_A(x1,x2) = max{1, x1 - 1, x2 - 4} Cons_usual!_A(x1,x2,x3) = 0 partial status: pi(Sum_sub#) = [2] pi(Cons_usual) = [2, 3] 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: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) p2: Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) and R consists of: r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) r9: Term_sub(Term_var(x),Id()) -> Term_var(x) r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) r14: Sum_sub(xi,Id()) -> Sum_term_var(xi) r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) r21: Concat(Id(),s) -> s The set of usable rules consists of (no rules) 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: Term_sub#_A(x1,x2) = max{0, x2 - 10} Term_var_A(x1) = max{15, x1 - 1} Cons_usual_A(x1,x2,x3) = max{12, x1 - 62, x2 - 62, x3 + 1} Cons_sum_A(x1,x2,x3) = max{10, x1 - 62, x2 - 62, x3 + 9} Term_sub#!_A(x1,x2) = max{2, x1 - 20, x2 - 13} Term_var!_A(x1) = max{3, x1 - 24} Cons_usual!_A(x1,x2,x3) = max{0, x2 - 23, x3 - 33} Cons_sum!_A(x1,x2,x3) = max{1, x1 - 6, x2 - 6, x3 - 14} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: Term_sub#_A(x1,x2) = max{0, x2 - 3} Term_var_A(x1) = max{4, x1 - 1} Cons_usual_A(x1,x2,x3) = max{2, x1 - 28, x2 - 4, x3 + 1} Cons_sum_A(x1,x2,x3) = max{x1 - 1, x2 - 4, x3 + 2} Term_sub#!_A(x1,x2) = max{4, x1 - 79, x2 - 70} Term_var!_A(x1) = max{2, x1 - 55} Cons_usual!_A(x1,x2,x3) = max{3, x1 - 93, x2 - 91, x3 - 93} Cons_sum!_A(x1,x2,x3) = max{0, x2 - 69, x3 - 69} partial status: pi(Term_sub#) = [2] pi(Term_var) = [1] pi(Cons_usual) = [3] pi(Cons_sum) = [3] The following rules are removed: p1, p2 Then no dependency pair remains.