YES
We show the termination of the TRS R:

  Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
  Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
  Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
  Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
  Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
  Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
  Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
  Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
  Term_sub(Term_var(x),Id()) -> Term_var(x)
  Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
  Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
  Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
  Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
  Sum_sub(xi,Id()) -> Sum_term_var(xi)
  Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
  Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
  Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
  Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
  Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
  Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
  Concat(Id(),s) -> s


-- SCC decomposition.

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

p1: Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
p2: Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
p3: Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s)
p4: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
p5: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
p6: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
p7: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p9: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p10: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p11: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p12: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p13: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
p14: Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
p15: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p16: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p17: Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s)
p18: Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s)
p19: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
p20: Concat#(Concat(s,t),u) -> Concat#(t,u)
p21: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p22: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p23: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)

and R consists of:

r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
r9: Term_sub(Term_var(x),Id()) -> Term_var(x)
r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
r14: Sum_sub(xi,Id()) -> Sum_term_var(xi)
r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
r21: Concat(Id(),s) -> s

The estimated dependency graph contains the following SCCs:

  {p1, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p15, p16, p19, p20, p21, p22, p23}
  {p17, p18}
  {p13, p14}


-- Reduction pair.

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

p1: Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
p2: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
p3: Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
p4: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
p5: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p6: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p7: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p8: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p9: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p10: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p11: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p12: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p13: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
p14: Concat#(Concat(s,t),u) -> Concat#(t,u)
p15: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
p16: Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
p17: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
p18: Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s)

and R consists of:

r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
r9: Term_sub(Term_var(x),Id()) -> Term_var(x)
r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
r14: Sum_sub(xi,Id()) -> Sum_term_var(xi)
r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
r21: Concat(Id(),s) -> s

The set of usable rules consists of

  r9, r10, r14, r15, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = max{118, x1 + 60}
        Case_A(x1,x2,x3) = max{x1 + 120, x2 + 394, x3 + 120}
        Frozen#_A(x1,x2,x3,x4) = max{174, x1 + 119, x3 + 119}
        Sum_sub_A(x1,x2) = max{x1 + 569, x2 - 80}
        Sum_term_var_A(x1) = x1 + 568
        Term_sub_A(x1,x2) = max{447, x1 + 62, x2 + 59}
        Concat#_A(x1,x2) = max{80, x1 + 40}
        Cons_sum_A(x1,x2,x3) = max{x1 + 105, x2 + 105, x3 + 41}
        Cons_usual_A(x1,x2,x3) = max{384, x1 + 79, x2 + 321, x3 + 197}
        Concat_A(x1,x2) = max{123, x1 + 62, x2 + 62}
        Term_inr_A(x1) = x1 + 119
        Term_inl_A(x1) = x1 + 119
        Term_pair_A(x1,x2) = max{385, x1 + 119, x2 + 322}
        Term_app_A(x1,x2) = max{385, x1 + 62, x2 + 62}
        Sum_constant_A(x1) = 106
        Right_A = 117
        Left_A = 117
        Term_var_A(x1) = max{101, x1 - 63}
        Id_A = 198
  
    base order 2:
  
      precedence:
      
        Case = Sum_constant = Right > Term_sub = Cons_usual = Concat = Term_inr = Term_var > Cons_sum = Term_inl = Term_pair = Term_app > Frozen# = Concat# = Left > Term_sub# > Sum_term_var > Sum_sub = Id
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Case) = [1]
      pi(Frozen#) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Term_sub) = [2]
      pi(Concat#) = [1]
      pi(Cons_sum) = [3]
      pi(Cons_usual) = [1, 2]
      pi(Concat) = [1, 2]
      pi(Term_inr) = []
      pi(Term_inl) = []
      pi(Term_pair) = []
      pi(Term_app) = []
      pi(Sum_constant) = []
      pi(Right) = []
      pi(Left) = []
      pi(Term_var) = []
      pi(Id) = []

The following rules are removed:

  p16



-- 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#(t,u)
p15: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
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#(Concat(s,t),u) -> Concat#(t,u)
p13: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p14: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p15: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
p16: Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,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, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = max{82, x1 + 42}
        Case_A(x1,x2,x3) = max{260, x1 + 86, x2 + 18, x3 + 84}
        Frozen#_A(x1,x2,x3,x4) = max{x1 + 83, x3 + 83}
        Sum_sub_A(x1,x2) = max{73, x1 + 59, x2 + 6}
        Sum_constant_A(x1) = max{81, x1 - 2}
        Left_A = 83
        Term_app_A(x1,x2) = max{x1 + 43, x2 + 173}
        Term_pair_A(x1,x2) = max{175, x1 + 45, x2 + 45}
        Term_inl_A(x1) = max{129, x1 + 83}
        Term_inr_A(x1) = max{91, x1 + 45}
        Term_sub_A(x1,x2) = max{174, x1 + 45, x2 + 41}
        Concat_A(x1,x2) = max{x1 + 46, x2 + 53}
        Concat#_A(x1,x2) = max{6, x1 + 3}
        Cons_usual_A(x1,x2,x3) = max{255, x1 + 80, x2 + 80, x3 + 80}
        Cons_sum_A(x1,x2,x3) = max{x1 + 75, x2 + 74, x3 + 5}
        Right_A = 85
        Sum_term_var_A(x1) = x1 + 58
        Term_var_A(x1) = max{122, x1 - 46}
        Id_A = 1
  
    base order 2:
  
      precedence:
      
        Concat > Term_sub = Term_var > Left = Term_app = Term_pair = Term_inl = Term_inr = Cons_usual = Cons_sum = Right > Concat# > Term_sub# > Sum_constant > Sum_sub > Case > Frozen# = Sum_term_var > Id
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Case) = []
      pi(Frozen#) = []
      pi(Sum_sub) = [1]
      pi(Sum_constant) = []
      pi(Left) = []
      pi(Term_app) = []
      pi(Term_pair) = []
      pi(Term_inl) = []
      pi(Term_inr) = [1]
      pi(Term_sub) = []
      pi(Concat) = [1, 2]
      pi(Concat#) = []
      pi(Cons_usual) = []
      pi(Cons_sum) = [3]
      pi(Right) = []
      pi(Sum_term_var) = []
      pi(Term_var) = []
      pi(Id) = []

The following rules are removed:

  p2



-- 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#(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#(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#(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_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_constant(Right()),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, r21

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = max{53, x1 + 27}
        Case_A(x1,x2,x3) = max{97, x1 + 55, x3 + 55}
        Frozen#_A(x1,x2,x3,x4) = max{83, x1 + 54, x3 + 54}
        Sum_sub_A(x1,x2) = max{50, x1 + 43, x2 - 50}
        Sum_term_var_A(x1) = x1 + 12
        Term_sub_A(x1,x2) = max{82, x1 + 40, x2 + 39}
        Concat#_A(x1,x2) = max{54, x1 + 38}
        Cons_sum_A(x1,x2,x3) = max{x1 + 100, x2 + 58, x3 + 55}
        Cons_usual_A(x1,x2,x3) = max{225, x1 + 184, x2 + 101, x3 + 51}
        Concat_A(x1,x2) = max{x1 + 40, x2 + 94}
        Term_inr_A(x1) = max{53, x1 + 43}
        Term_inl_A(x1) = max{68, x1 + 27}
        Term_pair_A(x1,x2) = max{81, x1 + 40, x2 + 40}
        Term_app_A(x1,x2) = max{x1 + 54, x2 + 40}
        Sum_constant_A(x1) = max{52, x1 + 9}
        Right_A = 0
        Term_var_A(x1) = max{10, x1 - 41}
        Id_A = 62
  
    base order 2:
  
      precedence:
      
        Case = Sum_constant = Term_var > Cons_sum = Concat > Term_sub > Frozen# = Cons_usual = Term_inr = Term_inl = Term_pair = Term_app = Right > Term_sub# = Concat# > Sum_term_var > Sum_sub = Id
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Case) = []
      pi(Frozen#) = [3]
      pi(Sum_sub) = []
      pi(Sum_term_var) = [1]
      pi(Term_sub) = []
      pi(Concat#) = [1]
      pi(Cons_sum) = [2, 3]
      pi(Cons_usual) = [1, 2, 3]
      pi(Concat) = [1, 2]
      pi(Term_inr) = []
      pi(Term_inl) = []
      pi(Term_pair) = [1, 2]
      pi(Term_app) = [2]
      pi(Sum_constant) = []
      pi(Right) = []
      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_term_var(xi),n,s) -> Term_sub#(n,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: 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_constant(Right()),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, p14}


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

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

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = max{51, x1 + 25}
        Term_sub_A(x1,x2) = max{67, x1 + 50, x2 - 19}
        Concat#_A(x1,x2) = max{76, x1 + 5}
        Concat_A(x1,x2) = max{68, x1 + 3, x2 + 4}
        Cons_usual_A(x1,x2,x3) = max{x1 + 50, x2 + 47, x3 + 72}
        Term_app_A(x1,x2) = max{65, x1 + 47, x2 + 49}
        Term_pair_A(x1,x2) = max{67, x1 + 43, x2 + 27}
        Term_inl_A(x1) = x1 + 26
        Term_inr_A(x1) = x1 + 26
        Cons_sum_A(x1,x2,x3) = max{x1 + 77, x2 + 55, x3 + 66}
        Term_var_A(x1) = max{8, x1 - 49}
        Id_A = 61
        Sum_sub_A(x1,x2) = max{x1 + 78, x2 - 60}
        Sum_term_var_A(x1) = x1 + 78
        Sum_constant_A(x1) = max{78, x1 - 6}
  
    base order 2:
  
      precedence:
      
        Id = Sum_sub > Term_var = Sum_constant > Concat = Cons_usual = Cons_sum > Concat# > Term_sub = Sum_term_var > Term_app = Term_pair = Term_inr > Term_sub# = Term_inl
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = []
      pi(Concat#) = [1]
      pi(Concat) = [1, 2]
      pi(Cons_usual) = [1]
      pi(Term_app) = []
      pi(Term_pair) = []
      pi(Term_inl) = [1]
      pi(Term_inr) = [1]
      pi(Cons_sum) = [1, 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_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_app(m,n),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p6: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p7: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p8: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p9: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p10: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p11: Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
p12: 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, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12}


-- 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#(Cons_sum(xi,k,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: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,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, r11, r12

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 1
        Term_sub_A(x1,x2) = max{51, x1 + 24, x2 + 48}
        Concat#_A(x1,x2) = x1 + 4
        Cons_sum_A(x1,x2,x3) = max{x1 + 5, x2 + 5, x3 + 209}
        Cons_usual_A(x1,x2,x3) = max{209, x1 - 2, x2 + 18, x3 + 5}
        Concat_A(x1,x2) = max{12, x1 + 6}
        Term_inr_A(x1) = max{27, x1 + 2}
        Term_inl_A(x1) = max{54, x1 + 2}
        Term_pair_A(x1,x2) = max{27, x1 + 1, x2 + 2}
        Term_app_A(x1,x2) = max{49, x1 + 23, x2 + 23}
        Term_var_A(x1) = max{28, x1 - 25}
        Id_A = 5
  
    base order 2:
  
      precedence:
      
        Term_sub > Term_pair > Term_sub# > Concat# = Term_inr = Term_inl = Term_app = Term_var > Cons_sum = Concat > Cons_usual > Id
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = []
      pi(Concat#) = [1]
      pi(Cons_sum) = [1, 2, 3]
      pi(Cons_usual) = []
      pi(Concat) = [1]
      pi(Term_inr) = []
      pi(Term_inl) = [1]
      pi(Term_pair) = []
      pi(Term_app) = []
      pi(Term_var) = []
      pi(Id) = []

The following rules are removed:

  p3



-- 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_sum(xi,k,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: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p10: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,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_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_app(m,n),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p6: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p7: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p8: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p9: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p10: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p11: 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

  r9, r10, r11, r12, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 8
        Term_sub_A(x1,x2) = max{44, x1 + 17, x2 - 2}
        Concat#_A(x1,x2) = max{52, x1}
        Concat_A(x1,x2) = max{52, x1 + 5}
        Cons_usual_A(x1,x2,x3) = max{x1 + 137, x2 + 38, x3 + 84}
        Term_app_A(x1,x2) = max{27, x1 + 9, x2 + 9}
        Term_pair_A(x1,x2) = max{27, x1 + 8, x2 + 9}
        Term_inl_A(x1) = max{27, x1 + 9}
        Term_inr_A(x1) = max{27, x1 + 9}
        Cons_sum_A(x1,x2,x3) = max{137, x1 + 53, x2 + 53, x3 + 7}
        Term_var_A(x1) = 37
        Id_A = 1
        Sum_sub_A(x1,x2) = max{24, x1 - 138, x2 - 138}
        Sum_term_var_A(x1) = max{24, x1 - 138}
        Sum_constant_A(x1) = max{24, x1 - 139}
  
    base order 2:
  
      precedence:
      
        Concat = Term_var > Cons_usual = Cons_sum > Term_sub > Term_app = Term_pair = Term_inl = Sum_sub > Term_sub# = Sum_term_var = Sum_constant > Concat# = Term_inr = Id
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = [1]
      pi(Concat#) = [1]
      pi(Concat) = [1]
      pi(Cons_usual) = [1, 2, 3]
      pi(Term_app) = []
      pi(Term_pair) = []
      pi(Term_inl) = []
      pi(Term_inr) = []
      pi(Cons_sum) = [1, 2, 3]
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Sum_constant) = []

The following rules are removed:

  p2



-- 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) -> Term_sub#(m,t)
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: 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, 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_sub(m,s),t) -> Concat#(s,t)
p2: Concat#(Cons_sum(xi,k,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: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p10: Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)

and R consists of:

r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
r9: Term_sub(Term_var(x),Id()) -> Term_var(x)
r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
r14: Sum_sub(xi,Id()) -> Sum_term_var(xi)
r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
r21: Concat(Id(),s) -> s

The set of usable rules consists of

  r9, r10, r11, r12, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 4
        Term_sub_A(x1,x2) = max{20, x1 + 7, x2}
        Concat#_A(x1,x2) = max{3, x1 - 1}
        Cons_sum_A(x1,x2,x3) = max{x1 + 15, x2 + 15, x3 + 21}
        Cons_usual_A(x1,x2,x3) = max{x1 + 27, x2 + 6, x3}
        Concat_A(x1,x2) = 0
        Term_inr_A(x1) = max{12, x1 + 4}
        Term_inl_A(x1) = max{13, x1 + 5}
        Term_pair_A(x1,x2) = max{19, x1 + 5, x2 + 4}
        Term_app_A(x1,x2) = max{13, x1 + 5, x2 + 1}
        Term_var_A(x1) = 7
        Id_A = 0
        Sum_sub_A(x1,x2) = max{28, x1 - 1, x2 - 28}
        Sum_term_var_A(x1) = max{1, x1 - 9}
        Sum_constant_A(x1) = max{14, x1 - 14}
  
    base order 2:
  
      precedence:
      
        Term_var = Sum_sub > Cons_usual = Sum_constant > Cons_sum = Concat > Term_sub = Term_pair > Term_inr = Term_inl = Term_app = Sum_term_var > Term_sub# = Id > Concat#
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Term_sub) = [1, 2]
      pi(Concat#) = []
      pi(Cons_sum) = [1, 2]
      pi(Cons_usual) = [1, 3]
      pi(Concat) = []
      pi(Term_inr) = []
      pi(Term_inl) = []
      pi(Term_pair) = []
      pi(Term_app) = []
      pi(Term_var) = []
      pi(Id) = []
      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: Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
p2: Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
p3: Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p4: Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
p5: Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
p6: Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
p7: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
p8: Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
p9: Term_sub#(Term_app(m,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}
  {p3, p4, p5, p6, p7, p8, p9}


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

  r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Concat#_A(x1,x2) = max{9, x1 + 2, x2 + 1}
        Cons_sum_A(x1,x2,x3) = max{7, x1 - 1, x2 - 1, x3}
        Sum_sub_A(x1,x2) = max{8, x1 - 1, x2 - 8}
        Id_A = 1
        Sum_term_var_A(x1) = max{2, x1 - 2}
        Sum_constant_A(x1) = max{5, x1 - 10}
  
    base order 2:
  
      precedence:
      
        Concat# = Sum_sub > Cons_sum > Sum_constant > Sum_term_var > Id
      
  
    partial status:
  
      pi(Concat#) = [1]
      pi(Cons_sum) = [3]
      pi(Sum_sub) = []
      pi(Id) = []
      pi(Sum_term_var) = []
      pi(Sum_constant) = []

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_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
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)

and R consists of:

r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
r9: Term_sub(Term_var(x),Id()) -> Term_var(x)
r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
r14: Sum_sub(xi,Id()) -> Sum_term_var(xi)
r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
r21: Concat(Id(),s) -> s

The set of usable rules consists of

  r9, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 29
        Term_sub_A(x1,x2) = max{x1 + 36, x2 - 26}
        Concat_A(x1,x2) = max{11, x1 - 13, x2 - 13}
        Term_app_A(x1,x2) = max{x1 + 30, x2 + 33}
        Term_pair_A(x1,x2) = max{x1 + 30, x2 + 33}
        Term_inl_A(x1) = x1 + 30
        Term_inr_A(x1) = x1 + 30
        Term_var_A(x1) = max{26, x1 - 37}
        Id_A = 1
        Sum_sub_A(x1,x2) = max{75, x1 - 1, x2 - 27}
        Sum_term_var_A(x1) = max{2, x1 - 5}
        Cons_sum_A(x1,x2,x3) = max{x1 + 25, x2 - 2, x3 - 12}
        Sum_constant_A(x1) = max{24, x1 - 30}
  
    base order 2:
  
      precedence:
      
        Term_var > Concat = Cons_sum > Sum_sub > Term_sub = Term_app = Term_pair = Term_inl = Term_inr > Term_sub# = Sum_constant > Sum_term_var > Id
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = [1]
      pi(Concat) = []
      pi(Term_app) = [2]
      pi(Term_pair) = [2]
      pi(Term_inl) = [1]
      pi(Term_inr) = [1]
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Cons_sum) = []
      pi(Sum_constant) = []

The following rules are removed:

  p7



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

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

and R consists of:

r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
r9: Term_sub(Term_var(x),Id()) -> Term_var(x)
r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
r14: Sum_sub(xi,Id()) -> Sum_term_var(xi)
r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
r21: Concat(Id(),s) -> s

The set of usable rules consists of

  r9, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 8
        Term_sub_A(x1,x2) = x1 + 8
        Concat_A(x1,x2) = max{17, x1 + 8, x2 + 8}
        Term_inl_A(x1) = x1 + 8
        Term_pair_A(x1,x2) = max{15, x1 + 8, x2 + 8}
        Term_app_A(x1,x2) = max{x1 + 9, x2 + 9}
        Term_var_A(x1) = max{10, x1 - 9}
        Id_A = 9
        Sum_sub_A(x1,x2) = max{20, x1 - 1, x2 - 10}
        Sum_term_var_A(x1) = max{10, x1 - 5}
        Cons_sum_A(x1,x2,x3) = max{9, x1 - 9, x2 - 9, x3 - 27}
        Sum_constant_A(x1) = max{0, x1 - 20}
  
    base order 2:
  
      precedence:
      
        Term_var = Sum_sub > Concat = Term_inl = Term_app = Cons_sum > Term_sub > Term_pair = Sum_constant > Term_sub# = Sum_term_var > Id
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = []
      pi(Concat) = []
      pi(Term_inl) = [1]
      pi(Term_pair) = []
      pi(Term_app) = [2]
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Cons_sum) = []
      pi(Sum_constant) = []

The following rules are removed:

  p6



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


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

and R consists of:

r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
r9: Term_sub(Term_var(x),Id()) -> Term_var(x)
r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
r14: Sum_sub(xi,Id()) -> Sum_term_var(xi)
r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
r21: Concat(Id(),s) -> s

The set of usable rules consists of

  r9, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = max{3, x1}
        Term_sub_A(x1,x2) = max{17, x1 + 9, x2 + 4}
        Concat_A(x1,x2) = max{19, x1 - 21, x2 - 21}
        Term_app_A(x1,x2) = max{28, x1 + 18, x2 + 12}
        Term_pair_A(x1,x2) = max{x1 + 2, x2 + 3}
        Term_inl_A(x1) = x1 + 6
        Term_var_A(x1) = max{8, x1 - 10}
        Id_A = 1
        Sum_sub_A(x1,x2) = max{5, x1 - 3, x2 - 3}
        Sum_term_var_A(x1) = max{2, x1 - 4}
        Cons_sum_A(x1,x2,x3) = max{2, x1 - 5, x2 - 5, x3 - 25}
        Sum_constant_A(x1) = max{1, x1 - 9}
  
    base order 2:
  
      precedence:
      
        Term_sub = Term_app = Term_pair = Term_inl = Sum_sub > Term_var = Sum_term_var > Concat = Id = Cons_sum > Term_sub# = Sum_constant
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = [2]
      pi(Concat) = []
      pi(Term_app) = [2]
      pi(Term_pair) = [2]
      pi(Term_inl) = [1]
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Cons_sum) = []
      pi(Sum_constant) = []

The following rules are removed:

  p5



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

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

  r9

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 9
        Term_sub_A(x1,x2) = x1 + 10
        Concat_A(x1,x2) = max{5, x1 - 11, x2 - 11}
        Term_pair_A(x1,x2) = max{x1 + 17, x2 + 12}
        Term_app_A(x1,x2) = max{22, x1 - 7, x2 + 11}
        Term_var_A(x1) = max{13, x1 - 11}
        Id_A = 14
  
    base order 2:
  
      precedence:
      
        Term_pair > Term_sub = Concat = Term_var > Term_app = Id > Term_sub#
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = [1]
      pi(Concat) = []
      pi(Term_pair) = [1]
      pi(Term_app) = []
      pi(Term_var) = []
      pi(Id) = []

The following rules are removed:

  p4



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


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

  r9, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 27
        Term_sub_A(x1,x2) = max{40, x1 + 35, x2 - 25}
        Concat_A(x1,x2) = max{24, x1 - 22, x2 - 22}
        Term_pair_A(x1,x2) = max{38, x1 + 34, x2 + 28}
        Term_var_A(x1) = max{5, x1 - 36}
        Id_A = 1
        Sum_sub_A(x1,x2) = max{24, x1 - 11, x2 - 26}
        Sum_term_var_A(x1) = max{2, x1 - 12}
        Cons_sum_A(x1,x2,x3) = max{2, x1 - 1, x2 - 1, x3 - 27}
        Sum_constant_A(x1) = max{1, x1 - 28}
  
    base order 2:
  
      precedence:
      
        Term_var > Concat = Sum_sub = Cons_sum > Term_sub > Term_pair = Sum_constant > Term_sub# > Sum_term_var > Id
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = []
      pi(Concat) = []
      pi(Term_pair) = [2]
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Cons_sum) = []
      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_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p2: Term_sub#(Term_pair(m,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#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
p2: Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)

and R consists of:

r1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
r2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
r3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
r4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
r5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
r6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
r7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
r8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
r9: Term_sub(Term_var(x),Id()) -> Term_var(x)
r10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
r11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
r12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
r13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
r14: Sum_sub(xi,Id()) -> Sum_term_var(xi)
r15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
r16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
r17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
r18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
r19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
r20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
r21: Concat(Id(),s) -> s

The set of usable rules consists of

  r9, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 15
        Term_sub_A(x1,x2) = max{x1 + 16, x2 - 13}
        Concat_A(x1,x2) = max{6, x1 - 14, x2 - 14}
        Term_pair_A(x1,x2) = max{23, x1 + 17, x2 - 8}
        Term_var_A(x1) = max{3, x1 - 17}
        Id_A = 2
        Sum_sub_A(x1,x2) = max{13, x1 - 8, x2 - 13}
        Sum_term_var_A(x1) = max{8, x1 - 9}
        Cons_sum_A(x1,x2,x3) = max{2, x1 - 1, x2 - 1, x3 - 15}
        Sum_constant_A(x1) = max{1, x1 - 15}
  
    base order 2:
  
      precedence:
      
        Term_sub = Term_pair > Term_var = Sum_sub > Concat = Cons_sum > Term_sub# = Sum_term_var = Sum_constant > Id
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = [1]
      pi(Concat) = []
      pi(Term_pair) = [1]
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Cons_sum) = []
      pi(Sum_constant) = []

The following rules are removed:

  p2



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

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_sub(m,s),t) -> Term_sub#(m,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, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = x1 + 7
        Term_sub_A(x1,x2) = max{x1 + 8, x2 - 5}
        Concat_A(x1,x2) = max{4, x1 - 15, x2 - 15}
        Term_var_A(x1) = max{3, x1 - 9}
        Id_A = 1
        Sum_sub_A(x1,x2) = max{12, x1 - 1, x2 - 3}
        Sum_term_var_A(x1) = max{2, x1 - 11}
        Cons_sum_A(x1,x2,x3) = max{2, x1 - 1, x2 - 1, x3 - 16}
        Sum_constant_A(x1) = max{1, x1 - 8}
  
    base order 2:
  
      precedence:
      
        Term_var = Sum_sub > Concat = Cons_sum > Term_sub = Sum_constant > Term_sub# > Sum_term_var > Id
      
  
    partial status:
  
      pi(Term_sub#) = [1]
      pi(Term_sub) = []
      pi(Concat) = []
      pi(Term_var) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Cons_sum) = []
      pi(Sum_constant) = []

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

  r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Sum_sub#_A(x1,x2) = max{1, x2 - 1}
        Cons_sum_A(x1,x2,x3) = max{5, x1 + 3, x2 + 3, x3 + 3}
        Cons_usual_A(x1,x2,x3) = max{6, x1 + 3, x2 + 3, x3 + 3}
        Sum_sub_A(x1,x2) = max{7, x1 - 1, x2 - 7}
        Id_A = 4
        Sum_term_var_A(x1) = max{5, x1 - 11}
        Sum_constant_A(x1) = max{4, x1 - 5}
  
    base order 2:
  
      precedence:
      
        Sum_sub > Sum_sub# = Cons_sum = Cons_usual > Sum_term_var > Id = Sum_constant
      
  
    partial status:
  
      pi(Sum_sub#) = []
      pi(Cons_sum) = [3]
      pi(Cons_usual) = []
      pi(Sum_sub) = []
      pi(Id) = []
      pi(Sum_term_var) = []
      pi(Sum_constant) = []

The following rules are removed:

  p2



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

  r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Sum_sub#_A(x1,x2) = max{x1 + 4, x2 + 11}
        Cons_sum_A(x1,x2,x3) = max{2, x1 - 7, x2 - 7, x3}
        Sum_sub_A(x1,x2) = max{17, x1 - 3, x2 - 6}
        Id_A = 1
        Sum_term_var_A(x1) = max{2, x1 - 4}
        Sum_constant_A(x1) = max{1, x1 - 14}
  
    base order 2:
  
      precedence:
      
        Sum_sub > Sum_sub# > Cons_sum > Sum_term_var = Sum_constant > Id
      
  
    partial status:
  
      pi(Sum_sub#) = [2]
      pi(Cons_sum) = [3]
      pi(Sum_sub) = []
      pi(Id) = []
      pi(Sum_term_var) = []
      pi(Sum_constant) = []

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

  r9, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = max{x1 - 11, x2 + 9}
        Term_var_A(x1) = 5
        Cons_usual_A(x1,x2,x3) = max{24, x1 - 1, x2 - 7, x3 + 10}
        Cons_sum_A(x1,x2,x3) = max{12, x1 - 7, x2 - 5, x3 + 10}
        Term_sub_A(x1,x2) = max{5, x1 - 35, x2 - 84}
        Id_A = 6
        Sum_sub_A(x1,x2) = max{25, x1 - 3, x2 - 25}
        Sum_term_var_A(x1) = max{7, x1 - 4}
        Sum_constant_A(x1) = max{11, x1 - 31}
  
    base order 2:
  
      precedence:
      
        Term_sub# = Sum_sub > Cons_sum > Term_sub = Sum_term_var > Cons_usual = Id = Sum_constant > Term_var
      
  
    partial status:
  
      pi(Term_sub#) = []
      pi(Term_var) = []
      pi(Cons_usual) = [3]
      pi(Cons_sum) = [3]
      pi(Term_sub) = []
      pi(Id) = []
      pi(Sum_sub) = []
      pi(Sum_term_var) = []
      pi(Sum_constant) = []

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

  r7, r14, r15

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        Term_sub#_A(x1,x2) = max{x1 - 2, x2 + 22}
        Term_var_A(x1) = x1 + 9
        Cons_usual_A(x1,x2,x3) = max{x1 - 7, x2 - 15, x3 + 4}
        Term_sub_A(x1,x2) = max{0, x1 - 14, x2 - 7}
        Term_inl_A(x1) = 0
        Sum_sub_A(x1,x2) = max{3, x1 - 3, x2 - 17}
        Id_A = 16
        Sum_term_var_A(x1) = max{0, x1 - 4}
        Cons_sum_A(x1,x2,x3) = max{2, x1 - 7, x2 - 7, x3 - 21}
        Sum_constant_A(x1) = max{1, x1 - 25}
  
    base order 2:
  
      precedence:
      
        Term_sub# = Term_var = Sum_sub > Cons_sum > Term_sub > Cons_usual = Term_inl = Sum_term_var = Sum_constant > Id
      
  
    partial status:
  
      pi(Term_sub#) = [2]
      pi(Term_var) = []
      pi(Cons_usual) = [3]
      pi(Term_sub) = []
      pi(Term_inl) = []
      pi(Sum_sub) = []
      pi(Id) = []
      pi(Sum_term_var) = []
      pi(Cons_sum) = []
      pi(Sum_constant) = []

The following rules are removed:

  p1

Then no dependency pair remains.