MAYBE
MAYBE
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))
 }
 DUP: We consider a duplicating system.
  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))
   }
  Fail