YES
TRS:
 {     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)),
                           Sum_sub(xi, Id()) -> Sum_term_var(xi),
            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_constant(k),
                 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_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),
                             Concat(Id(), s) -> s,
              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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
 DP:
  Strict:
   {     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#(m, s),
             Frozen#(m, Sum_term_var(xi), n, s) -> Term_sub#(n, 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_sub(m, s), t) -> Term_sub#(m, Concat(s, t)),
                   Term_sub#(Term_sub(m, s), t) -> Concat#(s, t),
                   Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), 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_app(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_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),
                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#(Concat(s, t), u) -> Concat#(s, Concat(t, u)),
                       Concat#(Concat(s, t), u) -> Concat#(t, u)}
  Weak:
  {     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)),
                            Sum_sub(xi, Id()) -> Sum_term_var(xi),
             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_constant(k),
                  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_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),
                              Concat(Id(), s) -> s,
               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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
  EDG:
   {
    (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))
    (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_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) -> Concat#(s, t))
    (Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, 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_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) -> Concat#(s, t))
    (Term_sub#(Term_sub(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#(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_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) -> Concat#(s, t))
    (Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, 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#(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_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#(Case(m, xi, n), s) -> Sum_sub#(xi, 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#(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)))
    (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#(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_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#(Case(m, xi, n), s) -> Sum_sub#(xi, 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#(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)))
    (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_usual(y, m, 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))
    (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#(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#(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_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#(Case(m, xi, n), s) -> Sum_sub#(xi, 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#(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_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#(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_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#(Case(m, xi, n), s) -> Sum_sub#(xi, 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#(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_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#(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_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#(Case(m, xi, n), s) -> Sum_sub#(xi, 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_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)))
    (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#(Cons_sum(xi, k, 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))
    (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#(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_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#(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_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_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#(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_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#(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_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_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#(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_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#(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_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))
    (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))
    (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#(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#(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#(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_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_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#(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(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#(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_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))
    (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#(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#(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) -> 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#(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))
    (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#(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_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))
    (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#(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#(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_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#(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#(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#(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_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))
   }
   SCCS:
    Scc:
     {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)}
    Scc:
     {Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s),
      Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)}
    Scc:
     { 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#(m, 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)),
                 Term_sub#(Term_sub(m, s), t) -> Concat#(s, t),
                 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_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_inr(m), s) -> Term_sub#(m, s),
              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#(Concat(s, t), u) -> Concat#(s, Concat(t, u)),
                     Concat#(Concat(s, t), u) -> Concat#(t, u)}
    SCC:
     Strict:
      {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)}
     Weak:
     {     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)),
                               Sum_sub(xi, Id()) -> Sum_term_var(xi),
                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_constant(k),
                     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_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),
                                 Concat(Id(), s) -> s,
                  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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
     SPSC:
      Simple Projection:
       pi(Term_sub#) = 1
      Strict:
       {Term_sub#(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub#(Term_var(x), s)}
      EDG:
       {(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))}
       SCCS:
        Scc:
         {Term_sub#(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub#(Term_var(x), s)}
        SCC:
         Strict:
          {Term_sub#(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub#(Term_var(x), s)}
         Weak:
         {     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)),
                                   Sum_sub(xi, Id()) -> Sum_term_var(xi),
                    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_constant(k),
                         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_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),
                                     Concat(Id(), s) -> s,
                      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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
         SPSC:
          Simple Projection:
           pi(Term_sub#) = 1
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s),
       Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)}
     Weak:
     {     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)),
                               Sum_sub(xi, Id()) -> Sum_term_var(xi),
                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_constant(k),
                     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_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),
                                 Concat(Id(), s) -> s,
                  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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
     SPSC:
      Simple Projection:
       pi(Sum_sub#) = 1
      Strict:
       {Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)}
      EDG:
       {(Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s))}
       SCCS:
        Scc:
         {Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)}
        SCC:
         Strict:
          {Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)}
         Weak:
         {     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)),
                                   Sum_sub(xi, Id()) -> Sum_term_var(xi),
                    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_constant(k),
                         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_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),
                                     Concat(Id(), s) -> s,
                      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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
         SPSC:
          Simple Projection:
           pi(Sum_sub#) = 1
          Strict:
           {}
          Qed
    SCC:
     Strict:
      { 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#(m, 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)),
                  Term_sub#(Term_sub(m, s), t) -> Concat#(s, t),
                  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_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_inr(m), s) -> Term_sub#(m, s),
               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#(Concat(s, t), u) -> Concat#(s, Concat(t, u)),
                      Concat#(Concat(s, t), u) -> Concat#(t, u)}
     Weak:
     {     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)),
                               Sum_sub(xi, Id()) -> Sum_term_var(xi),
                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_constant(k),
                     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_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),
                                 Concat(Id(), s) -> s,
                  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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
     POLY:
      Argument Filtering:
       pi(Concat#) = 0, pi(Concat) = [0,1], pi(Cons_sum) = 2, pi(Cons_usual) = [1,2], pi(Id) = [], pi(Term_var) = [], pi(Term_inr) = 0, pi(Term_inl) = 0, pi(Term_pair) = [0,1], pi(Term_app) = [0,1], pi(Sum_term_var) = [], pi(Right) = [], pi(Left) = [], pi(Sum_constant) = [], pi(Case) = [0,2], pi(Term_sub#) = 0, pi(Term_sub) = [0,1], pi(Sum_sub) = [], pi(Frozen#) = [0,2], pi(Frozen) = []
      Usable Rules:
       {}
      Interpretation:
       [Frozen#](x0, x1) = x0 + x1,
       [Cons_usual](x0, x1) = x0 + x1,
       [Case](x0, x1) = x0 + x1,
       [Concat](x0, x1) = x0 + x1 + 1,
       [Term_pair](x0, x1) = x0 + x1,
       [Term_app](x0, x1) = x0 + x1,
       [Term_sub](x0, x1) = x0 + x1
      Strict:
       { 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#(m, 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)),
                   Term_sub#(Term_sub(m, s), t) -> Concat#(s, t),
                   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_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_inr(m), s) -> Term_sub#(m, s),
                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)}
      Weak:
       {     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)),
                                 Sum_sub(xi, Id()) -> Sum_term_var(xi),
                  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_constant(k),
                       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_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),
                                   Concat(Id(), s) -> s,
                    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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
      EDG:
       {
        (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#(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_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#(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_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_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#(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_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#(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_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)))
        (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#(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_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#(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_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_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#(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_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#(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_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_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#(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_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#(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_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#(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))
        (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))
        (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#(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_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#(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_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)))
        (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) -> 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_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#(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#(Cons_sum(xi, k, 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#(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#(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#(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#(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_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_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#(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#(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#(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_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_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#(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#(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#(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_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_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#(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#(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#(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_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))
        (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#(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#(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#(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_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_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#(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#(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#(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_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))
       }
       SCCS:
        Scc:
         { 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#(m, 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)),
                     Term_sub#(Term_sub(m, s), t) -> Concat#(s, t),
                     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_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_inr(m), s) -> Term_sub#(m, s),
                  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)}
        SCC:
         Strict:
          { 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#(m, 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)),
                      Term_sub#(Term_sub(m, s), t) -> Concat#(s, t),
                      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_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_inr(m), s) -> Term_sub#(m, s),
                   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)}
         Weak:
         {     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)),
                                   Sum_sub(xi, Id()) -> Sum_term_var(xi),
                    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_constant(k),
                         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_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),
                                     Concat(Id(), s) -> s,
                      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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
         POLY:
          Argument Filtering:
           pi(Concat#) = 0, pi(Concat) = [], pi(Cons_sum) = 2, pi(Cons_usual) = [1,2], pi(Id) = [], pi(Term_var) = [], pi(Term_inr) = 0, pi(Term_inl) = 0, pi(Term_pair) = [0,1], pi(Term_app) = [0,1], pi(Sum_term_var) = [], pi(Right) = [], pi(Left) = [], pi(Sum_constant) = [], pi(Case) = [0,2], pi(Term_sub#) = 0, pi(Term_sub) = [0,1], pi(Sum_sub) = [], pi(Frozen#) = [0,2], pi(Frozen) = []
          Usable Rules:
           {}
          Interpretation:
           [Frozen#](x0, x1) = x0 + x1,
           [Cons_usual](x0, x1) = x0 + x1 + 1,
           [Case](x0, x1) = x0 + x1,
           [Term_pair](x0, x1) = x0 + x1,
           [Term_app](x0, x1) = x0 + x1,
           [Term_sub](x0, x1) = x0 + x1
          Strict:
           { 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#(m, 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)),
                       Term_sub#(Term_sub(m, s), t) -> Concat#(s, t),
                       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_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_inr(m), s) -> Term_sub#(m, s),
                     Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)}
          Weak:
           {     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)),
                                     Sum_sub(xi, Id()) -> Sum_term_var(xi),
                      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_constant(k),
                           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_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),
                                       Concat(Id(), s) -> s,
                        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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
          EDG:
           {
            (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#(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_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#(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_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)))
            (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#(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_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#(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_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)))
            (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#(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_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#(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_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_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#(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_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#(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_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_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#(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_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#(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_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_sub(m, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t))
            (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))
            (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))
            (Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, 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_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#(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#(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#(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_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_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#(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#(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#(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_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_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#(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#(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#(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_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))
            (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#(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#(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#(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_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_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#(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#(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#(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_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))
            (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#(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#(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#(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_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))
           }
           SCCS:
            Scc:
             {Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)}
            Scc:
             { 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#(m, 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)),
                         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_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_inr(m), s) -> Term_sub#(m, s)}
            SCC:
             Strict:
              {Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)}
             Weak:
             {     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)),
                                       Sum_sub(xi, Id()) -> Sum_term_var(xi),
                        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_constant(k),
                             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_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),
                                         Concat(Id(), s) -> s,
                          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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
             SPSC:
              Simple Projection:
               pi(Concat#) = 0
              Strict:
               {}
              Qed
            SCC:
             Strict:
              { 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#(m, 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)),
                          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_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_inr(m), s) -> Term_sub#(m, s)}
             Weak:
             {     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)),
                                       Sum_sub(xi, Id()) -> Sum_term_var(xi),
                        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_constant(k),
                             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_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),
                                         Concat(Id(), s) -> s,
                          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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
             POLY:
              Argument Filtering:
               pi(Concat) = [], pi(Cons_sum) = [], pi(Cons_usual) = [], pi(Id) = [], pi(Term_var) = [], pi(Term_inr) = [0], pi(Term_inl) = 0, pi(Term_pair) = [0,1], pi(Term_app) = [0,1], pi(Sum_term_var) = [], pi(Right) = [], pi(Left) = [], pi(Sum_constant) = [], pi(Case) = [0,2], pi(Term_sub#) = 0, pi(Term_sub) = 0, pi(Sum_sub) = [], pi(Frozen#) = [0,2], pi(Frozen) = []
              Usable Rules:
               {}
              Interpretation:
               [Frozen#](x0, x1) = x0 + x1,
               [Case](x0, x1) = x0 + x1,
               [Term_pair](x0, x1) = x0 + x1,
               [Term_app](x0, x1) = x0 + x1,
               [Term_inr](x0) = x0 + 1
              Strict:
               { 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#(m, 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)),
                           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_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)}
              Weak:
               {     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)),
                                         Sum_sub(xi, Id()) -> Sum_term_var(xi),
                          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_constant(k),
                               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_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),
                                           Concat(Id(), s) -> s,
                            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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
              EDG:
               {(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#(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_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#(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_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_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#(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_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#(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_sub(m, s), t) -> Term_sub#(m, Concat(s, t)))
                (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#(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_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#(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_sub(m, s), t) -> Term_sub#(m, Concat(s, t)))
                (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#(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_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#(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_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_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#(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_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#(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_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#(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#(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#(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#(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#(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_inl(m), s) -> Term_sub#(m, 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#(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#(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#(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_inl(m), s) -> Term_sub#(m, 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#(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#(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#(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_inl(m), s) -> Term_sub#(m, 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#(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#(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#(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_inl(m), s) -> Term_sub#(m, 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#(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#(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#(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_inl(m), s) -> Term_sub#(m, s))}
               SCCS:
                Scc:
                 { 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#(m, 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)),
                             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_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)}
                SCC:
                 Strict:
                  { 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#(m, 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)),
                              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_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)}
                 Weak:
                 {     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)),
                                           Sum_sub(xi, Id()) -> Sum_term_var(xi),
                            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_constant(k),
                                 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_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),
                                             Concat(Id(), s) -> s,
                              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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                 POLY:
                  Argument Filtering:
                   pi(Concat) = [], pi(Cons_sum) = [], pi(Cons_usual) = [], pi(Id) = [], pi(Term_var) = [], pi(Term_inr) = [], pi(Term_inl) = 0, pi(Term_pair) = [0,1], pi(Term_app) = [0,1], pi(Sum_term_var) = [], pi(Right) = [], pi(Left) = [], pi(Sum_constant) = [], pi(Case) = [0,2], pi(Term_sub#) = 0, pi(Term_sub) = 0, pi(Sum_sub) = [], pi(Frozen#) = [0,2], pi(Frozen) = []
                  Usable Rules:
                   {}
                  Interpretation:
                   [Frozen#](x0, x1) = x0 + x1,
                   [Case](x0, x1) = x0 + x1,
                   [Term_pair](x0, x1) = x0 + x1 + 1,
                   [Term_app](x0, x1) = x0 + x1
                  Strict:
                   { 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#(m, 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)),
                               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_inl(m), s) -> Term_sub#(m, s)}
                  Weak:
                   {     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)),
                                             Sum_sub(xi, Id()) -> Sum_term_var(xi),
                              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_constant(k),
                                   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_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),
                                               Concat(Id(), s) -> s,
                                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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                  EDG:
                   {(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_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#(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_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_inl(m), 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#(Term_app(m, n), s) -> Term_sub#(m, 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#(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_inl(m), 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#(Term_app(m, n), s) -> Term_sub#(m, 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#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)))
                    (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_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#(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_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) -> 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#(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#(Term_inl(m), s) -> Term_sub#(m, 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#(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#(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#(Term_inl(m), 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) -> 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#(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))
                    (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#(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#(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#(Term_inl(m), s) -> Term_sub#(m, 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#(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#(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#(Term_inl(m), s) -> Term_sub#(m, s))}
                   SCCS:
                    Scc:
                     { 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#(m, 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)),
                                 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_inl(m), s) -> Term_sub#(m, s)}
                    SCC:
                     Strict:
                      { 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#(m, 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)),
                                  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_inl(m), s) -> Term_sub#(m, s)}
                     Weak:
                     {     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)),
                                               Sum_sub(xi, Id()) -> Sum_term_var(xi),
                                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_constant(k),
                                     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_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),
                                                 Concat(Id(), s) -> s,
                                  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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                     POLY:
                      Argument Filtering:
                       pi(Concat) = [], pi(Cons_sum) = [], pi(Cons_usual) = [], pi(Id) = [], pi(Term_var) = [], pi(Term_inr) = [], pi(Term_inl) = [0], pi(Term_pair) = [], pi(Term_app) = [0,1], pi(Sum_term_var) = [], pi(Right) = [], pi(Left) = [], pi(Sum_constant) = [], pi(Case) = [0,2], pi(Term_sub#) = 0, pi(Term_sub) = 0, pi(Sum_sub) = [], pi(Frozen#) = [0,2], pi(Frozen) = []
                      Usable Rules:
                       {}
                      Interpretation:
                       [Frozen#](x0, x1) = x0 + x1,
                       [Case](x0, x1) = x0 + x1,
                       [Term_app](x0, x1) = x0 + x1,
                       [Term_inl](x0) = x0 + 1
                      Strict:
                       { 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#(m, 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)),
                                   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)}
                      Weak:
                       {     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)),
                                                 Sum_sub(xi, Id()) -> Sum_term_var(xi),
                                  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_constant(k),
                                       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_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),
                                                   Concat(Id(), s) -> s,
                                    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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                      EDG:
                       {(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#(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_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_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#(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_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_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))
                        (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#(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#(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_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#(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#(m, s))
                        (Term_sub#(Term_app(m, 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#(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#(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#(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_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#(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#(m, s))
                        (Frozen#(m, Sum_constant(Right()), n, s) -> Term_sub#(n, 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_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))
                        (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))}
                       SCCS:
                        Scc:
                         { 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#(m, 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)),
                                     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)}
                        SCC:
                         Strict:
                          { 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#(m, 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)),
                                      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)}
                         Weak:
                         {     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)),
                                                   Sum_sub(xi, Id()) -> Sum_term_var(xi),
                                    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_constant(k),
                                         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_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),
                                                     Concat(Id(), s) -> s,
                                      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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                         POLY:
                          Argument Filtering:
                           pi(Concat) = [], pi(Cons_sum) = [], pi(Cons_usual) = [], pi(Id) = [], pi(Term_var) = [], pi(Term_inr) = [], pi(Term_inl) = [], pi(Term_pair) = [], pi(Term_app) = [0,1], pi(Sum_term_var) = [], pi(Right) = [], pi(Left) = [], pi(Sum_constant) = [], pi(Case) = [0,2], pi(Term_sub#) = 0, pi(Term_sub) = 0, pi(Sum_sub) = [], pi(Frozen#) = [0,2], pi(Frozen) = []
                          Usable Rules:
                           {}
                          Interpretation:
                           [Frozen#](x0, x1) = x0 + x1,
                           [Case](x0, x1) = x0 + x1,
                           [Term_app](x0, x1) = x0 + x1 + 1
                          Strict:
                           { 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#(m, 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)),
                                       Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)}
                          Weak:
                           {     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)),
                                                     Sum_sub(xi, Id()) -> Sum_term_var(xi),
                                      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_constant(k),
                                           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_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),
                                                       Concat(Id(), s) -> s,
                                        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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                          EDG:
                           {(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_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_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_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))
                            (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))
                            (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#(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_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))
                            (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#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s))}
                           SCCS:
                            Scc:
                             { 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#(m, 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)),
                                         Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)}
                            SCC:
                             Strict:
                              { 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#(m, 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)),
                                          Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)}
                             Weak:
                             {     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)),
                                                       Sum_sub(xi, Id()) -> Sum_term_var(xi),
                                        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_constant(k),
                                             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_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),
                                                         Concat(Id(), s) -> s,
                                          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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                             POLY:
                              Argument Filtering:
                               pi(Concat) = [], pi(Cons_sum) = [], pi(Cons_usual) = [], pi(Id) = [], pi(Term_var) = [], pi(Term_inr) = [], pi(Term_inl) = [], pi(Term_pair) = [], pi(Term_app) = [], pi(Sum_term_var) = [], pi(Right) = [], pi(Left) = [], pi(Sum_constant) = [], pi(Case) = [0,2], pi(Term_sub#) = 0, pi(Term_sub) = 0, pi(Sum_sub) = [], pi(Frozen#) = [0,2], pi(Frozen) = []
                              Usable Rules:
                               {}
                              Interpretation:
                               [Frozen#](x0, x1) = x0 + x1,
                               [Case](x0, x1) = x0 + x1 + 1
                              Strict:
                               { 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#(m, 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))}
                              Weak:
                               {     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)),
                                                         Sum_sub(xi, Id()) -> Sum_term_var(xi),
                                          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_constant(k),
                                               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_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),
                                                           Concat(Id(), s) -> s,
                                            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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                              EDG:
                               {(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_term_var(xi), n, s) -> Term_sub#(n, s), 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)))
                                (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(Left()), n, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)))}
                               SCCS:
                                Scc:
                                 {Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))}
                                SCC:
                                 Strict:
                                  {Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))}
                                 Weak:
                                 {     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)),
                                                           Sum_sub(xi, Id()) -> Sum_term_var(xi),
                                            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_constant(k),
                                                 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_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),
                                                             Concat(Id(), s) -> s,
                                              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(Concat(s, t), u) -> Concat(s, Concat(t, u))}
                                 SPSC:
                                  Simple Projection:
                                   pi(Term_sub#) = 0
                                  Strict:
                                   {}
                                  Qed