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

  r10, r14, r15, r16, r17, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1
          Case_A(x1,x2,x3) = x1 + x3 + 3
          Frozen#_A(x1,x2,x3,x4) = x1 + x3 + 1
          Sum_sub_A(x1,x2) = 2
          Sum_term_var_A(x1) = 1
          Term_sub_A(x1,x2) = x1 + x2
          Concat#_A(x1,x2) = x1
          Cons_sum_A(x1,x2,x3) = x3 + 4
          Cons_usual_A(x1,x2,x3) = x2 + x3
          Concat_A(x1,x2) = x1 + x2 + 1
          Term_inr_A(x1) = x1
          Term_inl_A(x1) = x1
          Term_pair_A(x1,x2) = x1 + x2 + 1
          Term_app_A(x1,x2) = x1 + x2
          Sum_constant_A(x1) = 1
          Right_A() = 1
          Left_A() = 1
          Term_var_A(x1) = x1 + 3
          Id_A() = 2
  
    base order 2:
  
      precedence:
      
        Term_sub = Term_pair = Term_app = Term_var > Case = Id > Frozen# = Sum_term_var = Cons_sum = Cons_usual = Term_inl = Right = Left > Term_sub# = Concat# > Sum_sub = Concat = Term_inr > Sum_constant
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Case) = [3]
      pi(Frozen#) = [3]
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Term_sub) = []
      pi(Concat#) = []
      pi(Cons_sum) = []
      pi(Cons_usual) = [2]
      pi(Concat) = []
      pi(Term_inr) = [1]
      pi(Term_inl) = [1]
      pi(Term_pair) = []
      pi(Term_app) = []
      pi(Sum_constant) = []
      pi(Right) = []
      pi(Left) = []
      pi(Term_var) = []
      pi(Id) = []

The following rules are removed:

  p14



-- 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_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#(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) -> Term_sub#(m,Concat(s,t))
p10: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p11: Concat#(Concat(s,t),u) -> Concat#(s,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

  r9, r10, r11, r12, r14, r15, r16, r17, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1 + 2
          Case_A(x1,x2,x3) = x1 + x2 + x3 + 4
          Frozen#_A(x1,x2,x3,x4) = x1 + x3 + 3
          Sum_sub_A(x1,x2) = 2
          Sum_constant_A(x1) = 1
          Left_A() = 1
          Term_app_A(x1,x2) = x1 + x2 + 3
          Term_pair_A(x1,x2) = x1 + x2 + 3
          Term_inl_A(x1) = x1 + 3
          Term_inr_A(x1) = x1 + 3
          Term_sub_A(x1,x2) = x1 + x2 + 7
          Concat_A(x1,x2) = x1 + x2 + 6
          Concat#_A(x1,x2) = x1 + 1
          Cons_usual_A(x1,x2,x3) = x1 + x2 + x3 + 5
          Cons_sum_A(x1,x2,x3) = x1 + x2 + x3 + 3
          Right_A() = 1
          Sum_term_var_A(x1) = 1
          Term_var_A(x1) = x1 + 4
          Id_A() = 2
  
    base order 2:
  
      precedence:
      
        Term_var > Frozen# = Cons_sum > Term_sub# = Term_app = Term_pair = Term_sub = Concat = Cons_usual > Case = Sum_sub = Left = Term_inl = Term_inr = Concat# = Right = Id > Sum_constant = Sum_term_var
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Case) = [3]
      pi(Frozen#) = [3]
      pi(Sum_sub) = []
      pi(Sum_constant) = []
      pi(Left) = []
      pi(Term_app) = [2]
      pi(Term_pair) = [2]
      pi(Term_inl) = [1]
      pi(Term_inr) = [1]
      pi(Term_sub) = [1]
      pi(Concat) = [1, 2]
      pi(Concat#) = []
      pi(Cons_usual) = [2]
      pi(Cons_sum) = [2, 3]
      pi(Right) = []
      pi(Sum_term_var) = []
      pi(Term_var) = []
      pi(Id) = []

The following rules are removed:

  p1



-- SCC decomposition.

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

p1: Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s)
p2: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p3: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p4: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,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#(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:

  {p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13}


-- Reduction pair.

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

p1: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p2: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p3: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
p4: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p5: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p6: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,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: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))

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, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1
          Term_app_A(x1,x2) = x1 + x2 + 1
          Term_sub_A(x1,x2) = x1 + x2 + 4
          Concat#_A(x1,x2) = x1 + 1
          Cons_sum_A(x1,x2,x3) = x1 + x3 + 3
          Cons_usual_A(x1,x2,x3) = x2 + x3 + 6
          Concat_A(x1,x2) = x1 + 5
          Term_inr_A(x1) = x1 + 1
          Term_inl_A(x1) = x1 + 1
          Term_pair_A(x1,x2) = x1 + x2 + 1
          Term_var_A(x1) = 0
          Id_A() = 0
          Sum_sub_A(x1,x2) = 2
          Sum_term_var_A(x1) = 1
          Sum_constant_A(x1) = 1
  
    base order 2:
  
      precedence:
      
        Cons_usual = Id > Term_var > Term_app = Term_sub > Term_inr = Term_inl = Term_pair > Term_sub# = Concat > Cons_sum > Concat# = Sum_sub > Sum_term_var = Sum_constant
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_app) = []
      pi(Term_sub) = []
      pi(Concat#) = [1]
      pi(Cons_sum) = [1, 3]
      pi(Cons_usual) = [2]
      pi(Concat) = [1]
      pi(Term_inr) = [1]
      pi(Term_inl) = [1]
      pi(Term_pair) = [2]
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Sum_constant) = []

The following rules are removed:

  p3



-- SCC decomposition.

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

p1: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p2: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p3: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p4: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p5: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p6: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p7: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p9: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p10: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p11: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))

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}


-- Reduction pair.

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

p1: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p2: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p3: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p4: Term_sub#(Term_pair(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: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p8: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p9: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
p10: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p11: 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

  r9, r10, r11, r12, r14, r15, r16, r17, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1
          Term_app_A(x1,x2) = x1 + x2 + 1
          Term_pair_A(x1,x2) = x1 + x2 + 1
          Term_inl_A(x1) = x1 + 1
          Term_inr_A(x1) = x1 + 1
          Term_sub_A(x1,x2) = x1 + x2 + 5
          Concat_A(x1,x2) = x1 + x2 + 4
          Concat#_A(x1,x2) = x1 + 1
          Cons_usual_A(x1,x2,x3) = x1 + x2 + x3 + 3
          Term_var_A(x1) = x1 + 4
          Id_A() = 2
          Cons_sum_A(x1,x2,x3) = x1 + x2 + x3 + 3
          Sum_sub_A(x1,x2) = 2
          Sum_term_var_A(x1) = 1
          Sum_constant_A(x1) = 1
  
    base order 2:
  
      precedence:
      
        Concat = Term_var > Term_app = Term_pair = Term_sub > Term_inl = Term_inr = Cons_usual = Cons_sum > Concat# = Id = Sum_sub > Term_sub# = Sum_term_var = Sum_constant
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Term_app) = [2]
      pi(Term_pair) = [2]
      pi(Term_inl) = [1]
      pi(Term_inr) = [1]
      pi(Term_sub) = [1]
      pi(Concat) = []
      pi(Concat#) = []
      pi(Cons_usual) = []
      pi(Term_var) = [1]
      pi(Id) = []
      pi(Cons_sum) = [3]
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Sum_constant) = []

The following rules are removed:

  p1



-- SCC decomposition.

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

p1: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p2: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p3: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p4: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p6: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p7: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p8: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
p9: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p10: 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, p4, p5, p6, p7, p8, p9, p10}


-- Reduction pair.

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

p1: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p2: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p3: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p4: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p5: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p6: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p7: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p9: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p10: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))

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, r11, r12, r14, r15, r16, r17

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1 + 2
          Term_app_A(x1,x2) = x2 + 3
          Term_sub_A(x1,x2) = x1 + x2 + 4
          Concat#_A(x1,x2) = x1 + 1
          Cons_usual_A(x1,x2,x3) = x1 + x2 + x3 + 7
          Concat_A(x1,x2) = x1 + 2
          Term_inr_A(x1) = x1 + 1
          Term_inl_A(x1) = x1 + 3
          Term_pair_A(x1,x2) = x1 + x2 + 3
          Term_var_A(x1) = x1 + 8
          Id_A() = 2
          Cons_sum_A(x1,x2,x3) = x1 + x3 + 7
          Sum_sub_A(x1,x2) = 6
          Sum_term_var_A(x1) = 1
          Sum_constant_A(x1) = 5
  
    base order 2:
  
      precedence:
      
        Cons_usual = Term_var > Cons_sum > Sum_sub > Sum_constant > Term_sub = Concat# = Concat = Term_pair = Id > Term_app = Term_inr = Term_inl = Sum_term_var > Term_sub#
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_app) = [2]
      pi(Term_sub) = [1]
      pi(Concat#) = [1]
      pi(Cons_usual) = [2]
      pi(Concat) = [1]
      pi(Term_inr) = [1]
      pi(Term_inl) = [1]
      pi(Term_pair) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Cons_sum) = [3]
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Sum_constant) = []

The following rules are removed:

  p1



-- SCC decomposition.

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

p1: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p2: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p3: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p4: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,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: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))

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#(Term_sub(m,s),t) -> Concat#(s,t)
p2: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
p3: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p4: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,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: 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

  r4, r9, r10, r11, r12, r14, r15, r16, r17, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1
          Term_sub_A(x1,x2) = x1 + x2 + 2
          Concat#_A(x1,x2) = x1
          Concat_A(x1,x2) = x1 + x2 + 2
          Cons_usual_A(x1,x2,x3) = x2 + x3 + 5
          Term_pair_A(x1,x2) = x1 + x2 + 3
          Term_inl_A(x1) = x1 + 1
          Term_inr_A(x1) = x1 + 1
          Frozen_A(x1,x2,x3,x4) = x3 + x4 + 1
          Sum_term_var_A(x1) = 1
          Case_A(x1,x2,x3) = 0
          Term_var_A(x1) = 0
          Id_A() = 2
          Cons_sum_A(x1,x2,x3) = x3 + 5
          Sum_sub_A(x1,x2) = 4
          Sum_constant_A(x1) = 3
  
    base order 2:
  
      precedence:
      
        Concat# > Term_sub# = Term_pair = Id = Sum_constant > Term_sub = Concat = Term_inr = Frozen = Term_var > Cons_usual = Term_inl = Cons_sum > Sum_sub > Sum_term_var > Case
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Term_sub) = []
      pi(Concat#) = [1]
      pi(Concat) = [1]
      pi(Cons_usual) = [2, 3]
      pi(Term_pair) = []
      pi(Term_inl) = []
      pi(Term_inr) = []
      pi(Frozen) = []
      pi(Sum_term_var) = []
      pi(Case) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Cons_sum) = [3]
      pi(Sum_sub) = []
      pi(Sum_constant) = []

The following rules are removed:

  p1



-- SCC decomposition.

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


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

  r6, r7, r8, r9, r14, r15, r18, r19, r20, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Concat#_A(x1,x2) = x1 + x2 + 2
          Concat_A(x1,x2) = x1 + x2 + 4
          Cons_usual_A(x1,x2,x3) = x1 + x3 + 1
          Term_sub_A(x1,x2) = x1 + x2 + 3
          Term_pair_A(x1,x2) = 1
          Term_inl_A(x1) = 1
          Term_inr_A(x1) = 1
          Term_var_A(x1) = x1 + 3
          Id_A() = 1
          Sum_sub_A(x1,x2) = x1 + 3
          Sum_term_var_A(x1) = x1 + 2
          Cons_sum_A(x1,x2,x3) = x1 + x2 + x3 + 2
          Sum_constant_A(x1) = 1
  
    base order 2:
  
      precedence:
      
        Concat# = Term_sub = Sum_sub = Sum_term_var > Concat = Term_var > Cons_usual = Term_pair = Term_inl = Term_inr = Id = Cons_sum > Sum_constant
      
  
    partial status:
  
      pi(Concat#) = []
      pi(Concat) = []
      pi(Cons_usual) = [3]
      pi(Term_sub) = [1]
      pi(Term_pair) = []
      pi(Term_inl) = []
      pi(Term_inr) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = [1]
      pi(Sum_term_var) = [1]
      pi(Cons_sum) = [3]
      pi(Sum_constant) = []

The following rules are removed:

  p2



-- SCC decomposition.

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

p1: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))

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#(Concat(s,t),u) -> Concat#(s,Concat(t,u))

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, r15, r18, r19, r20, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Concat#_A(x1,x2) = x1 + x2 + 1
          Concat_A(x1,x2) = x1 + x2 + 5
          Term_sub_A(x1,x2) = 2
          Term_inl_A(x1) = 1
          Term_var_A(x1) = 1
          Id_A() = 2
          Sum_sub_A(x1,x2) = x1 + 5
          Cons_sum_A(x1,x2,x3) = x1 + x2 + x3 + 4
          Sum_constant_A(x1) = 3
          Cons_usual_A(x1,x2,x3) = x1 + x3 + 3
  
    base order 2:
  
      precedence:
      
        Sum_sub > Term_sub = Id > Concat# = Concat = Term_inl > Cons_sum = Cons_usual > Term_var = Sum_constant
      
  
    partial status:
  
      pi(Concat#) = [1]
      pi(Concat) = [1]
      pi(Term_sub) = []
      pi(Term_inl) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Cons_sum) = [3]
      pi(Sum_constant) = []
      pi(Cons_usual) = [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_pair(m,n),s) -> Term_sub#(m,s)
p2: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
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)

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

  r4, r5, r9, r15, r19, r20

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1 + 2
          Term_pair_A(x1,x2) = x1 + x2 + 3
          Term_sub_A(x1,x2) = x1 + x2 + 4
          Concat_A(x1,x2) = 5
          Term_inr_A(x1) = x1 + 3
          Term_inl_A(x1) = x1 + 3
          Frozen_A(x1,x2,x3,x4) = 2
          Sum_term_var_A(x1) = 5
          Case_A(x1,x2,x3) = 1
          Term_app_A(x1,x2) = 1
          Term_var_A(x1) = x1 + 7
          Id_A() = 6
          Sum_sub_A(x1,x2) = x1 + 3
          Cons_sum_A(x1,x2,x3) = 2
          Sum_constant_A(x1) = 1
          Cons_usual_A(x1,x2,x3) = 1
  
    base order 2:
  
      precedence:
      
        Id > Sum_term_var > Term_sub = Term_var = Sum_constant > Term_inr = Term_inl = Frozen = Term_app = Sum_sub > Term_sub# = Term_pair = Case > Concat > Cons_sum = Cons_usual
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Term_pair) = [1]
      pi(Term_sub) = []
      pi(Concat) = []
      pi(Term_inr) = []
      pi(Term_inl) = [1]
      pi(Frozen) = []
      pi(Sum_term_var) = []
      pi(Case) = []
      pi(Term_app) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = [1]
      pi(Cons_sum) = []
      pi(Sum_constant) = []
      pi(Cons_usual) = []

The following rules are removed:

  p1



-- SCC decomposition.

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

p1: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p2: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p3: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p4: Term_sub#(Term_pair(m,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}


-- Reduction pair.

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

p1: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p2: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p3: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p4: 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

  r5, r9, r14, r15, r20

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1
          Term_sub_A(x1,x2) = x1 + x2 + 7
          Concat_A(x1,x2) = 5
          Term_pair_A(x1,x2) = x2 + 1
          Term_inl_A(x1) = x1 + 1
          Term_inr_A(x1) = x1 + 1
          Term_app_A(x1,x2) = 1
          Term_var_A(x1) = x1 + 3
          Id_A() = 2
          Sum_sub_A(x1,x2) = x1 + x2 + 9
          Sum_term_var_A(x1) = 1
          Cons_sum_A(x1,x2,x3) = 4
          Sum_constant_A(x1) = 1
  
    base order 2:
  
      precedence:
      
        Sum_sub > Term_sub > Term_pair = Term_inl = Term_inr = Term_app = Term_var > Term_sub# = Id > Concat = Sum_term_var > Cons_sum > Sum_constant
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = []
      pi(Concat) = []
      pi(Term_pair) = [2]
      pi(Term_inl) = []
      pi(Term_inr) = [1]
      pi(Term_app) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = [1, 2]
      pi(Sum_term_var) = []
      pi(Cons_sum) = []
      pi(Sum_constant) = []

The following rules are removed:

  p1



-- SCC decomposition.

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

p1: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p2: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p3: 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 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_pair(m,n),s) -> Term_sub#(n,s)
p2: Term_sub#(Term_inr(m),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

  r9, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1
          Term_pair_A(x1,x2) = x2 + 3
          Term_inr_A(x1) = x1 + 3
          Term_inl_A(x1) = x1 + 3
          Term_sub_A(x1,x2) = 2
          Term_var_A(x1) = 1
          Id_A() = 6
          Concat_A(x1,x2) = x2 + 7
  
    base order 2:
  
      precedence:
      
        Term_pair = Term_inl > Term_inr = Term_sub = Id = Concat > Term_sub# > Term_var
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_pair) = [2]
      pi(Term_inr) = [1]
      pi(Term_inl) = [1]
      pi(Term_sub) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Concat) = []

The following rules are removed:

  p1



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


-- Reduction pair.

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

p1: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p2: 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

  r4, r6, r9, r15, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1 + x2 + 7
          Term_inr_A(x1) = x1 + 6
          Term_inl_A(x1) = x1 + 8
          Frozen_A(x1,x2,x3,x4) = x2 + 4
          Sum_term_var_A(x1) = 4
          Case_A(x1,x2,x3) = 1
          Term_sub_A(x1,x2) = x1 + 5
          Term_pair_A(x1,x2) = 6
          Term_var_A(x1) = x1 + 6
          Id_A() = 5
          Sum_sub_A(x1,x2) = x1 + 3
          Cons_sum_A(x1,x2,x3) = x3 + 1
          Sum_constant_A(x1) = 2
          Concat_A(x1,x2) = x2 + 11
  
    base order 2:
  
      precedence:
      
        Term_var > Id > Sum_term_var > Sum_sub > Term_sub# = Sum_constant > Term_inr = Term_inl = Cons_sum = Concat > Frozen = Case = Term_sub > Term_pair
      
  
    partial status:
  
      pi(Term_sub#) = [1, 2]
      pi(Term_inr) = [1]
      pi(Term_inl) = [1]
      pi(Frozen) = []
      pi(Sum_term_var) = []
      pi(Case) = []
      pi(Term_sub) = []
      pi(Term_pair) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = [1]
      pi(Cons_sum) = [3]
      pi(Sum_constant) = []
      pi(Concat) = [2]

The following rules are removed:

  p1



-- SCC decomposition.

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

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


-- Reduction pair.

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

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

  r4, r6, r9, r14, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x1
          Term_inl_A(x1) = x1 + 3
          Frozen_A(x1,x2,x3,x4) = x1 + x4 + 3
          Sum_term_var_A(x1) = 3
          Case_A(x1,x2,x3) = 2
          Term_sub_A(x1,x2) = 2
          Term_pair_A(x1,x2) = 1
          Term_var_A(x1) = 1
          Id_A() = 2
          Sum_sub_A(x1,x2) = x1 + 4
          Concat_A(x1,x2) = x2 + 4
  
    base order 2:
  
      precedence:
      
        Term_inl = Frozen = Sum_sub > Term_sub# = Sum_term_var > Case = Term_sub = Id = Concat > Term_pair = Term_var
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_inl) = [1]
      pi(Frozen) = []
      pi(Sum_term_var) = []
      pi(Case) = []
      pi(Term_sub) = []
      pi(Term_pair) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = [1]
      pi(Concat) = [2]

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

  r4, r6, r7, r8, r9, r14, r15, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Sum_sub#_A(x1,x2) = x2 + 6
          Cons_sum_A(x1,x2,x3) = x3 + 7
          Cons_usual_A(x1,x2,x3) = x3 + 5
          Frozen_A(x1,x2,x3,x4) = x1 + x2 + 2
          Sum_term_var_A(x1) = 2
          Case_A(x1,x2,x3) = 1
          Term_sub_A(x1,x2) = x1 + 3
          Term_pair_A(x1,x2) = 1
          Term_inl_A(x1) = 1
          Term_inr_A(x1) = 1
          Term_var_A(x1) = 1
          Id_A() = 3
          Sum_sub_A(x1,x2) = x1 + 9
          Sum_constant_A(x1) = 8
          Concat_A(x1,x2) = x2 + 8
  
    base order 2:
  
      precedence:
      
        Frozen = Term_sub = Id = Concat > Sum_term_var = Term_pair = Term_inl = Term_inr = Sum_constant > Sum_sub > Cons_sum = Case > Sum_sub# > Cons_usual > Term_var
      
  
    partial status:
  
      pi(Sum_sub#) = [2]
      pi(Cons_sum) = [3]
      pi(Cons_usual) = [3]
      pi(Frozen) = []
      pi(Sum_term_var) = []
      pi(Case) = []
      pi(Term_sub) = []
      pi(Term_pair) = []
      pi(Term_inl) = []
      pi(Term_inr) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_constant) = []
      pi(Concat) = []

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

  r6, r7, r8, r9, r14, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Sum_sub#_A(x1,x2) = x2
          Cons_usual_A(x1,x2,x3) = x3 + 1
          Term_sub_A(x1,x2) = x1 + x2 + 3
          Term_pair_A(x1,x2) = 1
          Term_inl_A(x1) = 1
          Term_inr_A(x1) = 1
          Term_var_A(x1) = x1 + 8
          Id_A() = 2
          Sum_sub_A(x1,x2) = x1 + 5
          Sum_term_var_A(x1) = 1
          Concat_A(x1,x2) = x2 + 2
  
    base order 2:
  
      precedence:
      
        Term_sub = Concat > Term_pair = Term_var > Id > Sum_sub = Sum_term_var > Cons_usual = Term_inl = Term_inr > Sum_sub#
      
  
    partial status:
  
      pi(Sum_sub#) = []
      pi(Cons_usual) = [3]
      pi(Term_sub) = []
      pi(Term_pair) = []
      pi(Term_inl) = []
      pi(Term_inr) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Concat) = []

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

  r6, r7, r8, r14, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x2
          Term_var_A(x1) = x1 + 2
          Cons_usual_A(x1,x2,x3) = x3 + 1
          Cons_sum_A(x1,x2,x3) = x3 + 7
          Term_sub_A(x1,x2) = x2 + 3
          Term_pair_A(x1,x2) = 0
          Term_inl_A(x1) = 0
          Term_inr_A(x1) = 0
          Sum_sub_A(x1,x2) = x1 + 5
          Id_A() = 5
          Sum_term_var_A(x1) = 4
          Concat_A(x1,x2) = x2 + 8
  
    base order 2:
  
      precedence:
      
        Term_inr = Sum_sub = Id = Concat > Term_var = Term_sub = Sum_term_var > Cons_usual = Cons_sum = Term_pair = Term_inl > Term_sub#
      
  
    partial status:
  
      pi(Term_sub#) = [2]
      pi(Term_var) = [1]
      pi(Cons_usual) = [3]
      pi(Cons_sum) = [3]
      pi(Term_sub) = []
      pi(Term_pair) = []
      pi(Term_inl) = []
      pi(Term_inr) = []
      pi(Sum_sub) = []
      pi(Id) = []
      pi(Sum_term_var) = []
      pi(Concat) = []

The following rules are removed:

  p2



-- SCC decomposition.

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)

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_usual(y,m,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

  r5, r6, r7, r8, r9, r14, r15, r16, r17, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          Term_sub#_A(x1,x2) = x2 + 2
          Term_var_A(x1) = 1
          Cons_usual_A(x1,x2,x3) = x3 + 3
          Term_sub_A(x1,x2) = x2 + 2
          Term_app_A(x1,x2) = 1
          Term_pair_A(x1,x2) = 1
          Term_inl_A(x1) = 1
          Term_inr_A(x1) = 1
          Id_A() = 2
          Sum_sub_A(x1,x2) = x1 + 4
          Sum_term_var_A(x1) = 1
          Cons_sum_A(x1,x2,x3) = x3 + 3
          Sum_constant_A(x1) = 1
          Concat_A(x1,x2) = x2 + 1
  
    base order 2:
  
      precedence:
      
        Sum_sub > Term_sub = Term_app > Term_pair = Term_inl = Term_inr = Sum_term_var = Concat > Cons_usual = Id = Cons_sum > Term_sub# = Sum_constant > Term_var
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Term_var) = []
      pi(Cons_usual) = [3]
      pi(Term_sub) = []
      pi(Term_app) = []
      pi(Term_pair) = []
      pi(Term_inl) = []
      pi(Term_inr) = []
      pi(Id) = []
      pi(Sum_sub) = [1]
      pi(Sum_term_var) = []
      pi(Cons_sum) = [3]
      pi(Sum_constant) = []
      pi(Concat) = []

The following rules are removed:

  p1

Then no dependency pair remains.