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

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x1 + 2
    Case_A(x1,x2,x3) = max{7, x1, x3}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 2, x3 + 2}
    Sum_sub_A(x1,x2) = max{x1 + 1, x2 + 10}
    Sum_term_var_A(x1) = 1
    Term_sub_A(x1,x2) = max{x1 + 11, x2}
    Concat#_A(x1,x2) = max{13, x1 + 2}
    Cons_sum_A(x1,x2,x3) = max{2, x1 - 9, x2 - 9, x3}
    Cons_usual_A(x1,x2,x3) = max{11, x1, x2, x3}
    Concat_A(x1,x2) = max{x1 + 11, x2}
    Term_inr_A(x1) = max{11, x1}
    Term_inl_A(x1) = max{12, x1}
    Term_pair_A(x1,x2) = max{12, x1, x2}
    Term_app_A(x1,x2) = max{12, x1, x2}
    Sum_constant_A(x1) = 1
    Right_A = 0
    Left_A = 0
    Frozen_A(x1,x2,x3,x4) = max{x1 + 11, x3 + 11, x4}
    Term_var_A(x1) = max{12, x1 + 1}
    Id_A = 0

The next rules are strictly ordered:

  p7

We remove them from the problem.

-- 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_inr(m),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p9: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p10: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,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(Right()),n,s) -> Term_sub#(n,s)
p17: 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, p17}


-- 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#(m,s)
p6: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p7: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
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_constant(Right()),n,s) -> Term_sub#(n,s)
p16: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
p17: 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

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x1 + 11
    Case_A(x1,x2,x3) = max{6, x1, x3}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 11, x3 + 11}
    Sum_sub_A(x1,x2) = max{x1 + 3, x2 + 3}
    Sum_constant_A(x1) = 3
    Left_A = 0
    Term_app_A(x1,x2) = max{1, x1, x2}
    Term_pair_A(x1,x2) = max{1, x1, x2}
    Term_inl_A(x1) = max{1, x1}
    Term_inr_A(x1) = max{1, x1}
    Term_sub_A(x1,x2) = max{x1 + 6, x2 - 2}
    Concat#_A(x1,x2) = x1 + 9
    Concat_A(x1,x2) = max{x1 + 6, x2}
    Cons_usual_A(x1,x2,x3) = max{x1, x2 + 2, x3}
    Cons_sum_A(x1,x2,x3) = max{6, x1, x2, x3}
    Right_A = 0
    Sum_term_var_A(x1) = 1
    Frozen_A(x1,x2,x3,x4) = max{x1 + 6, x3 + 6, x4 - 2}
    Term_var_A(x1) = max{1, x1 - 5}
    Id_A = 0

The next rules are strictly ordered:

  p10

We remove them from the problem.

-- 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_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#(m,s)
p6: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p7: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p9: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p10: Concat#(Concat(s,t),u) -> Concat#(t,u)
p11: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p12: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p13: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
p14: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
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 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_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_inr(m),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p9: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p10: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,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: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
p15: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,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 set of usable rules consists of

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = max{4, x1 + 2}
    Case_A(x1,x2,x3) = max{x1 + 2, x2 + 4, x3 + 2}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 4, x3 + 3}
    Sum_sub_A(x1,x2) = max{x1 + 3, x2 + 3}
    Sum_term_var_A(x1) = 1
    Term_sub_A(x1,x2) = max{x1 + 4, x2 + 4}
    Concat#_A(x1,x2) = x1 + 5
    Cons_sum_A(x1,x2,x3) = max{x2, x3}
    Cons_usual_A(x1,x2,x3) = max{x1, x2, x3}
    Term_inr_A(x1) = x1 + 1
    Term_inl_A(x1) = x1
    Term_pair_A(x1,x2) = max{x1, x2}
    Term_app_A(x1,x2) = max{x1, x2}
    Concat_A(x1,x2) = max{x1 + 1, x2 + 1}
    Sum_constant_A(x1) = x1 + 3
    Right_A = 0
    Left_A = 0
    Id_A = 0

The next rules are strictly ordered:

  p3, p6, p13

We remove them from the problem.

-- 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: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
p4: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p5: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p6: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p7: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p8: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p9: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p10: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p11: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
p12: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
p13: 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, p5, p6, p7, p8, p9, p10, p11, p12, p13}
  {p3, p4}


-- 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#(m,s)
p6: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p7: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p9: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
p10: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
p11: 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

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x1 + 5
    Case_A(x1,x2,x3) = max{x1, x2, x3 + 1}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 5, x2, x3 + 6}
    Sum_sub_A(x1,x2) = x1 + 1
    Sum_constant_A(x1) = 1
    Left_A = 0
    Term_app_A(x1,x2) = max{x1, x2}
    Term_pair_A(x1,x2) = max{x1, x2}
    Term_inl_A(x1) = x1
    Term_inr_A(x1) = x1
    Right_A = 0
    Sum_term_var_A(x1) = 1
    Id_A = 0
    Cons_sum_A(x1,x2,x3) = max{x1 + 1, x2 - 1, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1, x2}

The next rules are strictly ordered:

  p9, p11

We remove them from the problem.

-- 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_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#(m,s)
p6: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p7: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p9: 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:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9}


-- 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#(m,s)
p3: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p4: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p6: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p7: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p8: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p9: 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

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = max{3, x1 + 1}
    Case_A(x1,x2,x3) = max{x1 + 2, x2 + 3, x3 + 2}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 1, x2, x3 + 3}
    Sum_sub_A(x1,x2) = x1 + 4
    Sum_term_var_A(x1) = 4
    Term_inr_A(x1) = x1
    Term_inl_A(x1) = x1
    Term_pair_A(x1,x2) = max{x1, x2 + 3}
    Term_app_A(x1,x2) = max{x1, x2}
    Sum_constant_A(x1) = 3
    Left_A = 2
    Id_A = 3
    Cons_sum_A(x1,x2,x3) = max{x1 + 3, x2 - 1, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1, x2}

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- 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#(m,s)
p3: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p4: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p6: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p7: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p8: 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}


-- 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#(m,s)
p6: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p7: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p8: 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 set of usable rules consists of

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = max{1, x1}
    Case_A(x1,x2,x3) = max{x1 + 3, x2 + 3, x3 + 3}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 1, x2, x3 + 1}
    Sum_sub_A(x1,x2) = x1 + 3
    Sum_constant_A(x1) = 1
    Left_A = 0
    Term_app_A(x1,x2) = max{x1, x2}
    Term_pair_A(x1,x2) = max{x1 + 2, x2 + 2}
    Term_inl_A(x1) = x1
    Term_inr_A(x1) = x1 + 1
    Sum_term_var_A(x1) = x1 + 1
    Id_A = 0
    Cons_sum_A(x1,x2,x3) = max{x1 + 1, x2 - 1, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1, x2}

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- 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_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_inl(m),s) -> Term_sub#(m,s)
p6: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p7: 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:

  {p1, p2, p3, p4, p5, p6, p7}


-- 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#(m,s)
p3: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p4: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p6: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p7: 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

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x1 + 1
    Case_A(x1,x2,x3) = max{x1 + 2, x2 + 2, x3 + 2}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 1, x2 + 1, x3 + 1}
    Sum_sub_A(x1,x2) = x1 + 2
    Sum_term_var_A(x1) = 2
    Term_inr_A(x1) = x1
    Term_inl_A(x1) = x1
    Term_app_A(x1,x2) = max{x1, x2 + 1}
    Sum_constant_A(x1) = 0
    Left_A = 0
    Id_A = 2
    Cons_sum_A(x1,x2,x3) = max{x1 + 1, x2 - 1, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1 + 1, x2 + 1}

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- 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#(m,s)
p3: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p4: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p6: 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}


-- 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_inl(m),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p6: 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 set of usable rules consists of

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x1 + 3
    Case_A(x1,x2,x3) = max{x1 + 1, x2 - 2, x3 + 1}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 3, x2, x3 + 3}
    Sum_sub_A(x1,x2) = x1 + 1
    Sum_constant_A(x1) = 1
    Left_A = 0
    Term_app_A(x1,x2) = x1
    Term_inl_A(x1) = x1
    Term_inr_A(x1) = x1 + 1
    Sum_term_var_A(x1) = 1
    Id_A = 0
    Cons_sum_A(x1,x2,x3) = max{x1 + 1, x2 - 1, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1, x2}

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- 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_constant(Left()),n,s) -> Term_sub#(m,s)
p3: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p4: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p5: 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:

  {p1, p2, p3, p4, p5}


-- 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#(m,s)
p3: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p4: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p5: 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

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x1
    Case_A(x1,x2,x3) = max{x1 + 2, x2 + 2, x3 + 2}
    Frozen#_A(x1,x2,x3,x4) = max{x1, x2 + 1, x3 + 2}
    Sum_sub_A(x1,x2) = x1 + 1
    Sum_term_var_A(x1) = max{1, x1}
    Term_inl_A(x1) = x1
    Term_app_A(x1,x2) = max{x1 + 1, x2 + 1}
    Sum_constant_A(x1) = 1
    Left_A = 0
    Id_A = 0
    Cons_sum_A(x1,x2,x3) = max{x1 + 1, x2 - 3, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1, x2}

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- 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#(m,s)
p3: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p4: 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}


-- 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_inl(m),s) -> Term_sub#(m,s)
p4: 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 set of usable rules consists of

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = max{3, x1}
    Case_A(x1,x2,x3) = max{x1 + 3, x2 + 4, x3 + 4}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 3, x2, x3 + 3}
    Sum_sub_A(x1,x2) = x1 + 4
    Sum_constant_A(x1) = 1
    Left_A = 0
    Term_inl_A(x1) = x1
    Sum_term_var_A(x1) = x1 + 4
    Id_A = 0
    Cons_sum_A(x1,x2,x3) = max{x1 + 1, x2, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1, x2}

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- 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_constant(Left()),n,s) -> Term_sub#(m,s)
p3: Term_sub#(Term_inl(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 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#(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_inl(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

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x1 + 1
    Case_A(x1,x2,x3) = max{x1 + 1, x2, x3 + 1}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 1, x2 - 2, x3 + 1}
    Sum_sub_A(x1,x2) = max{4, x1 + 3}
    Sum_constant_A(x1) = 2
    Left_A = 3
    Term_inl_A(x1) = x1 + 1
    Id_A = 3
    Sum_term_var_A(x1) = max{4, x1 + 3}
    Cons_sum_A(x1,x2,x3) = max{x1 + 2, x2, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1, x2}

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- 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_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}


-- 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)

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

  r14, r15, r16, r17

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x1 + 3
    Case_A(x1,x2,x3) = max{x1 + 1, x2 + 1, x3 + 1}
    Frozen#_A(x1,x2,x3,x4) = max{x1 + 4, x2 + 3, x3 + 4}
    Sum_sub_A(x1,x2) = x1 + 1
    Sum_constant_A(x1) = 1
    Left_A = 0
    Id_A = 0
    Sum_term_var_A(x1) = x1 + 1
    Cons_sum_A(x1,x2,x3) = max{x1 + 1, x2 - 5, x3 - 1}
    Cons_usual_A(x1,x2,x3) = max{x1, x2}

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- 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)

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: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
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

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Concat#_A(x1,x2) = x1 + 1
    Cons_sum_A(x1,x2,x3) = max{x1, x2, x3}
    Cons_usual_A(x1,x2,x3) = max{x1, x2, x3 + 1}

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: 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}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: 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 set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    Concat#_A(x1,x2) = x1
    Cons_sum_A(x1,x2,x3) = x3 + 1

The next rules are strictly ordered:

  p1

We remove them from the problem.  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:

  max/plus interpretations on natural numbers:
  
    Sum_sub#_A(x1,x2) = x2 + 1
    Cons_sum_A(x1,x2,x3) = max{x1, x2, x3}
    Cons_usual_A(x1,x2,x3) = max{x1, x2, x3 + 1}

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: Sum_sub#(xi,Cons_sum(psi,k,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_sum(psi,k,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:

  max/plus interpretations on natural numbers:
  
    Sum_sub#_A(x1,x2) = x2
    Cons_sum_A(x1,x2,x3) = max{x1, x2, x3 + 1}

The next rules are strictly ordered:

  p1

We remove them from the problem.  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:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = max{x1, x2}
    Term_var_A(x1) = 0
    Cons_usual_A(x1,x2,x3) = max{x1 + 1, x2 + 1, x3 + 1}
    Cons_sum_A(x1,x2,x3) = x3

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: 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 estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: 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:

  max/plus interpretations on natural numbers:
  
    Term_sub#_A(x1,x2) = x2 + 1
    Term_var_A(x1) = x1 + 2
    Cons_sum_A(x1,x2,x3) = max{x1 + 1, x2 + 1, x3 + 1}

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.