MAYBE

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

Proof:
 DP Processor:
  DPs:
   Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
   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) -> Term_sub#(n,s)
   Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
   Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
   Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
   Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
   Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
   Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
   Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
   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) -> Concat#(s,t)
   Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
   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#(t,u)
   Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
   Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
   Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
   Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
  TRS:
   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
  TDG Processor:
   DPs:
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    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) -> Term_sub#(n,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    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) -> Concat#(s,t)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    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#(t,u)
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
   TRS:
    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
   graph:
    Concat#(Concat(s,t),u) -> Concat#(t,u) ->
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
    Concat#(Concat(s,t),u) -> Concat#(t,u) ->
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
    Concat#(Concat(s,t),u) -> Concat#(t,u) ->
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
    Concat#(Concat(s,t),u) -> Concat#(t,u) ->
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
    Concat#(Concat(s,t),u) -> Concat#(t,u) ->
    Concat#(Concat(s,t),u) -> Concat#(t,u)
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
    Concat#(Concat(s,t),u) -> Concat#(t,u)
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
    Concat#(Concat(s,t),u) -> Concat#(t,u)
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
    Concat#(Concat(s,t),u) -> Concat#(t,u)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
    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) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s) ->
    Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s)
    Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s) ->
    Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s)
    Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s) ->
    Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s)
    Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s) ->
    Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,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))
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Term_sub#(Term_var(x),Cons_sum(xi,k,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_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    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_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    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_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
    Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
    Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
    Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
    Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
    Concat#(Concat(s,t),u) -> Concat#(t,u)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    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)) ->
    Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
    Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s)
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) ->
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) ->
    Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
    Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) ->
    Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
    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)
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) ->
    Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s)
    Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) -> Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s)
   SCC Processor:
    #sccs: 2
    #rules: 22
    #arcs: 203/529
    DPs:
     Concat#(Concat(s,t),u) -> Concat#(t,u)
     Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
     Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
     Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
     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)
     Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
     Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
     Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
     Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
     Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
     Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
     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) -> Concat#(s,t)
     Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
     Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
     Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
     Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
     Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
    TRS:
     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
    EDG Processor:
     DPs:
      Concat#(Concat(s,t),u) -> Concat#(t,u)
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
      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)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      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) -> Concat#(s,t)
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
     TRS:
      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
     graph:
      Concat#(Concat(s,t),u) -> Concat#(t,u) ->
      Concat#(Concat(s,t),u) -> Concat#(t,u)
      Concat#(Concat(s,t),u) -> Concat#(t,u) ->
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
      Concat#(Concat(s,t),u) -> Concat#(t,u) ->
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
      Concat#(Concat(s,t),u) -> Concat#(t,u) ->
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
      Concat#(Concat(s,t),u) -> Concat#(t,u) ->
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
      Concat#(Concat(s,t),u) -> Concat#(t,u)
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) ->
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
      Concat#(Concat(s,t),u) -> Concat#(t,u)
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) ->
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
      Concat#(Concat(s,t),u) -> Concat#(t,u)
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) ->
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      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) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) ->
      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_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      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_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
      Concat#(Concat(s,t),u) -> Concat#(t,u)
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
      Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
      Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
      Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) ->
      Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      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)) ->
      Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) ->
      Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
      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)
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) ->
      Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) ->
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
      Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) ->
      Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
     SCC Processor:
      #sccs: 2
      #rules: 20
      #arcs: 165/400
      DPs:
       Concat#(Concat(s,t),u) -> Concat#(t,u)
       Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
       Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
       Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
       Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
       Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
       Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u))
       Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
       Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
       Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
       Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
       Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
       Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
       Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
       Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
       Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
       Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
       Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s)
      TRS:
       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
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [Concat#](x0, x1) = x0 + 0,
        
        [Frozen#](x0, x1, x2, x3) = x0 + x2 + 3,
        
        [Term_sub#](x0, x1) = x0 + 0,
        
        [Concat](x0, x1) = 2x0 + x1 + 2,
        
        [Cons_sum](x0, x1, x2) = 4x0 + 3x1 + x2 + 0,
        
        [Cons_usual](x0, x1, x2) = 1x0 + x1 + x2 + 0,
        
        [Id] = 0,
        
        [Term_var](x0) = x0,
        
        [Term_inr](x0) = x0,
        
        [Term_inl](x0) = x0 + 5,
        
        [Term_pair](x0, x1) = x0 + x1,
        
        [Term_app](x0, x1) = x0 + x1 + 2,
        
        [Sum_term_var](x0) = 0,
        
        [Right] = 2,
        
        [Sum_constant](x0) = x0,
        
        [Left] = 0,
        
        [Frozen](x0, x1, x2, x3) = 2x0 + 2x2 + x3 + 5,
        
        [Sum_sub](x0, x1) = x0 + x1 + 0,
        
        [Term_sub](x0, x1) = 2x0 + x1 + 0,
        
        [Case](x0, x1, x2) = x0 + x2 + 3
       orientation:
        Concat#(Concat(s,t),u) = 2s + t + 2 >= t + 0 = Concat#(t,u)
        
        Concat#(Cons_sum(xi,k,s),t) = 3k + s + 4xi + 0 >= s + 0 = Concat#(s,t)
        
        Concat#(Cons_usual(x,m,s),t) = m + s + 1x + 0 >= m + 0 = Term_sub#(m,t)
        
        Term_sub#(Term_sub(m,s),t) = 2m + s + 0 >= m + 0 = Term_sub#(m,Concat(s,t))
        
        Term_sub#(Term_sub(m,s),t) = 2m + s + 0 >= s + 0 = Concat#(s,t)
        
        Concat#(Cons_usual(x,m,s),t) = m + s + 1x + 0 >= s + 0 = Concat#(s,t)
        
        Concat#(Concat(s,t),u) = 2s + t + 2 >= s + 0 = Concat#(s,Concat(t,u))
        
        Term_sub#(Term_inr(m),s) = m + 0 >= m + 0 = Term_sub#(m,s)
        
        Term_sub#(Term_inl(m),s) = m + 5 >= m + 0 = Term_sub#(m,s)
        
        Term_sub#(Term_pair(m,n),s) = m + n + 0 >= m + 0 = Term_sub#(m,s)
        
        Term_sub#(Term_pair(m,n),s) = m + n + 0 >= n + 0 = Term_sub#(n,s)
        
        Term_sub#(Term_app(m,n),s) = m + n + 2 >= m + 0 = Term_sub#(m,s)
        
        Term_sub#(Term_app(m,n),s) = m + n + 2 >= n + 0 = Term_sub#(n,s)
        
        Term_sub#(Case(m,xi,n),s) = m + n + 3 >= m + n + 3 = Frozen#(m,Sum_sub(xi,s),n,s)
        
        Frozen#(m,Sum_term_var(xi),n,s) = m + n + 3 >= m + 0 = Term_sub#(m,s)
        
        Frozen#(m,Sum_term_var(xi),n,s) = m + n + 3 >= n + 0 = Term_sub#(n,s)
        
        Frozen#(m,Sum_constant(Right()),n,s) = m + n + 3 >= n + 0 = Term_sub#(n,s)
        
        Frozen#(m,Sum_constant(Left()),n,s) = m + n + 3 >= m + 0 = Term_sub#(m,s)
        
        Term_sub(Case(m,xi,n),s) = 2m + 2n + s + 5 >= 2m + 2n + s + 5 = Frozen(m,Sum_sub(xi,s),n,s)
        
        Frozen(m,Sum_constant(Left()),n,s) = 2m + 2n + s + 5 >= 2m + s + 0 = Term_sub(m,s)
        
        Frozen(m,Sum_constant(Right()),n,s) = 2m + 2n + s + 5 >= 2n + s + 0 = Term_sub(n,s)
        
        Frozen(m,Sum_term_var(xi),n,s) = 2m + 2n + s + 5 >= 2m + 2n + s + 3 = Case(Term_sub(m,s),xi,Term_sub(n,s))
        
        Term_sub(Term_app(m,n),s) = 2m + 2n + s + 4 >= 2m + 2n + s + 2 = Term_app(Term_sub(m,s),Term_sub(n,s))
        
        Term_sub(Term_pair(m,n),s) = 2m + 2n + s + 0 >= 2m + 2n + s + 0 = Term_pair(Term_sub(m,s),Term_sub(n,s))
        
        Term_sub(Term_inl(m),s) = 2m + s + 7 >= 2m + s + 5 = Term_inl(Term_sub(m,s))
        
        Term_sub(Term_inr(m),s) = 2m + s + 0 >= 2m + s + 0 = Term_inr(Term_sub(m,s))
        
        Term_sub(Term_var(x),Id()) = 2x + 0 >= x = Term_var(x)
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) = m + s + 2x + 1y + 0 >= m = m
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) = m + s + 2x + 1y + 0 >= s + 2x + 0 = Term_sub(Term_var(x),s)
        
        Term_sub(Term_var(x),Cons_sum(xi,k,s)) = 3k + s + 2x + 4xi + 0 >= s + 2x + 0 = Term_sub(Term_var(x),s)
        
        Term_sub(Term_sub(m,s),t) = 4m + 2s + t + 2 >= 2m + 2s + t + 2 = Term_sub(m,Concat(s,t))
        
        Sum_sub(xi,Id()) = xi + 0 >= 0 = Sum_term_var(xi)
        
        Sum_sub(xi,Cons_sum(psi,k,s)) = 3k + 4psi + s + xi + 0 >= k = Sum_constant(k)
        
        Sum_sub(xi,Cons_sum(psi,k,s)) = 3k + 4psi + s + xi + 0 >= s + xi + 0 = Sum_sub(xi,s)
        
        Sum_sub(xi,Cons_usual(y,m,s)) = m + s + xi + 1y + 0 >= s + xi + 0 = Sum_sub(xi,s)
        
        Concat(Concat(s,t),u) = 4s + 2t + u + 4 >= 2s + 2t + u + 2 = Concat(s,Concat(t,u))
        
        Concat(Cons_usual(x,m,s),t) = 2m + 2s + t + 3x + 2 >= 2m + 2s + t + 1x + 2 = Cons_usual(x,Term_sub(m,t),Concat(s,t))
        
        Concat(Cons_sum(xi,k,s),t) = 5k + 2s + t + 6xi + 2 >= 3k + 2s + t + 4xi + 2 = Cons_sum(xi,k,Concat(s,t))
        
        Concat(Id(),s) = s + 2 >= s = s
       problem:
        DPs:
         Concat#(Concat(s,t),u) -> Concat#(t,u)
         Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
         Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
         Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t))
         Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
         Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
         Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
         Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
         Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
         Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
         Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
         Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
         Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
         Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
         Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
         Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
         Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s)
        TRS:
         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
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [Concat#](x0, x1) = x0,
         
         [Frozen#](x0, x1, x2, x3) = x0 + x1 + x2 + 0,
         
         [Term_sub#](x0, x1) = x0,
         
         [Concat](x0, x1) = 1x0 + x1 + 0,
         
         [Cons_sum](x0, x1, x2) = x1 + x2 + 0,
         
         [Cons_usual](x0, x1, x2) = 5x0 + x1 + x2,
         
         [Id] = 2,
         
         [Term_var](x0) = 3,
         
         [Term_inr](x0) = x0 + 0,
         
         [Term_inl](x0) = x0 + 0,
         
         [Term_pair](x0, x1) = x0 + x1 + 5,
         
         [Term_app](x0, x1) = x0 + x1 + 0,
         
         [Sum_term_var](x0) = x0 + 0,
         
         [Right] = 6,
         
         [Sum_constant](x0) = 0,
         
         [Left] = 0,
         
         [Frozen](x0, x1, x2, x3) = 1x0 + x1 + 1x2 + x3 + 0,
         
         [Sum_sub](x0, x1) = x0 + 0,
         
         [Term_sub](x0, x1) = 1x0 + x1 + 0,
         
         [Case](x0, x1, x2) = x0 + x1 + x2 + 0
        orientation:
         Concat#(Concat(s,t),u) = 1s + t + 0 >= t = Concat#(t,u)
         
         Concat#(Cons_sum(xi,k,s),t) = k + s + 0 >= s = Concat#(s,t)
         
         Concat#(Cons_usual(x,m,s),t) = m + s + 5x >= m = Term_sub#(m,t)
         
         Term_sub#(Term_sub(m,s),t) = 1m + s + 0 >= m = Term_sub#(m,Concat(s,t))
         
         Term_sub#(Term_sub(m,s),t) = 1m + s + 0 >= s = Concat#(s,t)
         
         Concat#(Cons_usual(x,m,s),t) = m + s + 5x >= s = Concat#(s,t)
         
         Term_sub#(Term_inr(m),s) = m + 0 >= m = Term_sub#(m,s)
         
         Term_sub#(Term_inl(m),s) = m + 0 >= m = Term_sub#(m,s)
         
         Term_sub#(Term_pair(m,n),s) = m + n + 5 >= m = Term_sub#(m,s)
         
         Term_sub#(Term_pair(m,n),s) = m + n + 5 >= n = Term_sub#(n,s)
         
         Term_sub#(Term_app(m,n),s) = m + n + 0 >= m = Term_sub#(m,s)
         
         Term_sub#(Term_app(m,n),s) = m + n + 0 >= n = Term_sub#(n,s)
         
         Term_sub#(Case(m,xi,n),s) = m + n + xi + 0 >= m + n + xi + 0 = Frozen#(m,Sum_sub(xi,s),n,s)
         
         Frozen#(m,Sum_term_var(xi),n,s) = m + n + xi + 0 >= m = Term_sub#(m,s)
         
         Frozen#(m,Sum_term_var(xi),n,s) = m + n + xi + 0 >= n = Term_sub#(n,s)
         
         Frozen#(m,Sum_constant(Right()),n,s) = m + n + 0 >= n = Term_sub#(n,s)
         
         Frozen#(m,Sum_constant(Left()),n,s) = m + n + 0 >= m = Term_sub#(m,s)
         
         Term_sub(Case(m,xi,n),s) = 1m + 1n + s + 1xi + 1 >= 1m + 1n + s + xi + 0 = Frozen(m,Sum_sub(xi,s),n,s)
         
         Frozen(m,Sum_constant(Left()),n,s) = 1m + 1n + s + 0 >= 1m + s + 0 = Term_sub(m,s)
         
         Frozen(m,Sum_constant(Right()),n,s) = 1m + 1n + s + 0 >= 1n + s + 0 = Term_sub(n,s)
         
         Frozen(m,Sum_term_var(xi),n,s) = 1m + 1n + s + xi + 0 >= 1m + 1n + s + xi + 0 = Case(Term_sub(m,s),xi,Term_sub(n,s))
         
         Term_sub(Term_app(m,n),s) = 1m + 1n + s + 1 >= 1m + 1n + s + 0 = Term_app(Term_sub(m,s),Term_sub(n,s))
         
         Term_sub(Term_pair(m,n),s) = 1m + 1n + s + 6 >= 1m + 1n + s + 5 = Term_pair(Term_sub(m,s),Term_sub(n,s))
         
         Term_sub(Term_inl(m),s) = 1m + s + 1 >= 1m + s + 0 = Term_inl(Term_sub(m,s))
         
         Term_sub(Term_inr(m),s) = 1m + s + 1 >= 1m + s + 0 = Term_inr(Term_sub(m,s))
         
         Term_sub(Term_var(x),Id()) = 4 >= 3 = Term_var(x)
         
         Term_sub(Term_var(x),Cons_usual(y,m,s)) = m + s + 5y + 4 >= m = m
         
         Term_sub(Term_var(x),Cons_usual(y,m,s)) = m + s + 5y + 4 >= s + 4 = Term_sub(Term_var(x),s)
         
         Term_sub(Term_var(x),Cons_sum(xi,k,s)) = k + s + 4 >= s + 4 = Term_sub(Term_var(x),s)
         
         Term_sub(Term_sub(m,s),t) = 2m + 1s + t + 1 >= 1m + 1s + t + 0 = Term_sub(m,Concat(s,t))
         
         Sum_sub(xi,Id()) = xi + 0 >= xi + 0 = Sum_term_var(xi)
         
         Sum_sub(xi,Cons_sum(psi,k,s)) = xi + 0 >= 0 = Sum_constant(k)
         
         Sum_sub(xi,Cons_sum(psi,k,s)) = xi + 0 >= xi + 0 = Sum_sub(xi,s)
         
         Sum_sub(xi,Cons_usual(y,m,s)) = xi + 0 >= xi + 0 = Sum_sub(xi,s)
         
         Concat(Concat(s,t),u) = 2s + 1t + u + 1 >= 1s + 1t + u + 0 = Concat(s,Concat(t,u))
         
         Concat(Cons_usual(x,m,s),t) = 1m + 1s + t + 6x + 0 >= 1m + 1s + t + 5x + 0 = Cons_usual(x,Term_sub(m,t),Concat(s,t))
         
         Concat(Cons_sum(xi,k,s),t) = 1k + 1s + t + 1 >= k + 1s + t + 0 = Cons_sum(xi,k,Concat(s,t))
         
         Concat(Id(),s) = s + 3 >= s = s
        problem:
         DPs:
          Concat#(Concat(s,t),u) -> Concat#(t,u)
          Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t)
          Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t)
          Term_sub#(Term_sub(m,s),t) -> Concat#(s,t)
          Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t)
          Term_sub#(Term_inr(m),s) -> Term_sub#(m,s)
          Term_sub#(Term_inl(m),s) -> Term_sub#(m,s)
          Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s)
          Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s)
          Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s)
          Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s)
          Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s)
          Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s)
          Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s)
          Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s)
          Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s)
         TRS:
          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
        Open
      
      DPs:
       Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),s)
       Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s)
      TRS:
       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
      Subterm Criterion Processor:
       simple projection:
        pi(Term_sub#) = 1
       problem:
        DPs:
         
        TRS:
         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
       Qed
    
    DPs:
     Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s)
     Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s)
    TRS:
     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
    Subterm Criterion Processor:
     simple projection:
      pi(Sum_sub#) = 1
     problem:
      DPs:
       
      TRS:
       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
     Qed