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, r14, r15, r16, r17, r21 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: Term_sub#_A(x1,x2) = x1 + 3 Case_A(x1,x2,x3) = x1 + x3 + 10 Frozen#_A(x1,x2,x3,x4) = x1 + x2 + x3 Sum_sub_A(x1,x2) = 9 Sum_term_var_A(x1) = 3 Term_sub_A(x1,x2) = x1 + x2 + 5 Concat#_A(x1,x2) = x1 Cons_sum_A(x1,x2,x3) = x1 + x2 + x3 + 7 Cons_usual_A(x1,x2,x3) = x1 + x2 + x3 + 10 Concat_A(x1,x2) = x1 + x2 + 11 Term_inr_A(x1) = x1 + 6 Term_inl_A(x1) = x1 + 6 Term_pair_A(x1,x2) = x1 + x2 + 6 Term_app_A(x1,x2) = x1 + x2 + 4 Sum_constant_A(x1) = 8 Right_A() = 4 Left_A() = 1 Term_var_A(x1) = 1 Id_A() = 2 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: Term_sub#_A(x1,x2) = 0 Case_A(x1,x2,x3) = 1 Frozen#_A(x1,x2,x3,x4) = 0 Sum_sub_A(x1,x2) = 1 Sum_term_var_A(x1) = 1 Term_sub_A(x1,x2) = x1 + x2 + 2 Concat#_A(x1,x2) = 0 Cons_sum_A(x1,x2,x3) = x1 + x2 Cons_usual_A(x1,x2,x3) = x1 + x2 Concat_A(x1,x2) = x2 Term_inr_A(x1) = 1 Term_inl_A(x1) = 1 Term_pair_A(x1,x2) = 1 Term_app_A(x1,x2) = x1 + x2 + 1 Sum_constant_A(x1) = 1 Right_A() = 0 Left_A() = 1 Term_var_A(x1) = x1 + 1 Id_A() = 1 Term_sub#!_A(x1,x2) = 2 Case!_A(x1,x2,x3) = x1 + x3 + 3 Frozen#!_A(x1,x2,x3,x4) = 2 Sum_sub!_A(x1,x2) = 4 Sum_term_var!_A(x1) = 1 Term_sub!_A(x1,x2) = 6 Concat#!_A(x1,x2) = 2 Cons_sum!_A(x1,x2,x3) = 1 Cons_usual!_A(x1,x2,x3) = x3 + 4 Concat!_A(x1,x2) = 6 Term_inr!_A(x1) = x1 + 5 Term_inl!_A(x1) = x1 + 5 Term_pair!_A(x1,x2) = x1 + x2 + 7 Term_app!_A(x1,x2) = x1 + x2 + 3 Sum_constant!_A(x1) = 4 Right!_A() = 0 Left!_A() = 7 Term_var!_A(x1) = 5 Id!_A() = 0 partial status: pi(Term_sub#) = [] pi(Case) = [] pi(Frozen#) = [] pi(Sum_sub) = [] pi(Sum_term_var) = [] pi(Term_sub) = [1] pi(Concat#) = [1] pi(Cons_sum) = [1, 2, 3] pi(Cons_usual) = [] pi(Concat) = [1, 2] pi(Term_inr) = [1] pi(Term_inl) = [1] pi(Term_pair) = [1, 2] pi(Term_app) = [] pi(Sum_constant) = [] pi(Right) = [] pi(Left) = [] pi(Term_var) = [] pi(Id) = [] The following rules are removed: p1, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p17, p18 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) p2: Frozen#(m,Sum_term_var(xi),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: (no SCCs) -- 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 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: Sum_sub#_A(x1,x2) = x1 + x2 + 5 Cons_sum_A(x1,x2,x3) = x1 + x2 + x3 + 4 Cons_usual_A(x1,x2,x3) = x1 + x3 + 4 Term_sub_A(x1,x2) = 2 Term_var_A(x1) = 1 Id_A() = 4 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: Sum_sub#_A(x1,x2) = x2 Cons_sum_A(x1,x2,x3) = x3 + 1 Cons_usual_A(x1,x2,x3) = x3 + 3 Term_sub_A(x1,x2) = x1 + x2 + 1 Term_var_A(x1) = x1 + 5 Id_A() = 3 Sum_sub#!_A(x1,x2) = x1 + x2 + 9 Cons_sum!_A(x1,x2,x3) = x3 + 12 Cons_usual!_A(x1,x2,x3) = x3 + 8 Term_sub!_A(x1,x2) = x1 + x2 + 4 Term_var!_A(x1) = 11 Id!_A() = 12 partial status: pi(Sum_sub#) = [1] pi(Cons_sum) = [1, 2] pi(Cons_usual) = [1] pi(Term_sub) = [] pi(Term_var) = [] 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: 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 r7, r9, r21 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: Term_sub#_A(x1,x2) = 3 Term_var_A(x1) = 1 Cons_usual_A(x1,x2,x3) = 2 Cons_sum_A(x1,x2,x3) = x2 + x3 + 4 Term_sub_A(x1,x2) = 3 Term_inl_A(x1) = 0 Id_A() = 2 Concat_A(x1,x2) = x2 + 5 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: Term_sub#_A(x1,x2) = 0 Term_var_A(x1) = x1 + 1 Cons_usual_A(x1,x2,x3) = x3 + 3 Cons_sum_A(x1,x2,x3) = x3 + 5 Term_sub_A(x1,x2) = x1 + x2 + 2 Term_inl_A(x1) = 1 Id_A() = 1 Concat_A(x1,x2) = x2 + 3 Term_sub#!_A(x1,x2) = x2 Term_var!_A(x1) = 4 Cons_usual!_A(x1,x2,x3) = 6 Cons_sum!_A(x1,x2,x3) = 10 Term_sub!_A(x1,x2) = 5 Term_inl!_A(x1) = 5 Id!_A() = 6 Concat!_A(x1,x2) = x1 + x2 + 4 partial status: pi(Term_sub#) = [] pi(Term_var) = [] pi(Cons_usual) = [] pi(Cons_sum) = [2, 3] pi(Term_sub) = [] pi(Term_inl) = [] pi(Id) = [] pi(Concat) = [] The following rules are removed: p1, p2 Then no dependency pair remains.