Termination Proof using AProVE

Term Rewriting System R:
[m, xi, n, s, x, y, k, t, psi, u]
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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

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)
TERM_SUB(Term_sub(m, s), t) -> TERM_SUB(m, Concat(s, t))
TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
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_sum(psi, k, s)) -> SUM_SUB(xi, s)
SUM_SUB(xi, Cons_usual(y, m, s)) -> SUM_SUB(xi, s)
CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
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)

Furthermore, R contains three SCCs.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
SUM_SUB(xi, Cons_usual(y, m, s)) -> SUM_SUB(xi, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) -> SUM_SUB(xi, s)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s
Dependency Pairs:
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)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s
Dependency Pairs:
FROZEN(m, Sum_{term_var}(xi), n, s) -> TERM_SUB(n, s)
FROZEN(m, Sum_{term_var}(xi), n, s) -> TERM_SUB(m, s)
FROZEN(m, Sum_constant(Right), n, s) -> TERM_SUB(n, s)
CONCAT(Cons_sum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) -> TERM_SUB(m, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
TERM_SUB(Term_sub(m, s), t) -> TERM_SUB(m, Concat(s, t))
TERM_SUB(Term_inr(m), s) -> TERM_SUB(m, s)
TERM_SUB(Term_inl(m), s) -> TERM_SUB(m, s)
TERM_SUB(Term_pair(m, n), s) -> TERM_SUB(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(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)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
SUM_SUB(xi, Cons_usual(y, m, s)) -> SUM_SUB(xi, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) -> SUM_SUB(xi, s)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s
Dependency Pairs:
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)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s
Dependency Pairs:
FROZEN(m, Sum_{term_var}(xi), n, s) -> TERM_SUB(n, s)
FROZEN(m, Sum_{term_var}(xi), n, s) -> TERM_SUB(m, s)
FROZEN(m, Sum_constant(Right), n, s) -> TERM_SUB(n, s)
CONCAT(Cons_sum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) -> TERM_SUB(m, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
TERM_SUB(Term_sub(m, s), t) -> TERM_SUB(m, Concat(s, t))
TERM_SUB(Term_inr(m), s) -> TERM_SUB(m, s)
TERM_SUB(Term_inl(m), s) -> TERM_SUB(m, s)
TERM_SUB(Term_pair(m, n), s) -> TERM_SUB(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(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)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
SUM_SUB(xi, Cons_usual(y, m, s)) -> SUM_SUB(xi, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) -> SUM_SUB(xi, s)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s
Dependency Pairs:
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)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s
Dependency Pairs:
FROZEN(m, Sum_{term_var}(xi), n, s) -> TERM_SUB(n, s)
FROZEN(m, Sum_{term_var}(xi), n, s) -> TERM_SUB(m, s)
FROZEN(m, Sum_constant(Right), n, s) -> TERM_SUB(n, s)
CONCAT(Cons_sum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) -> TERM_SUB(m, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
TERM_SUB(Term_sub(m, s), t) -> TERM_SUB(m, Concat(s, t))
TERM_SUB(Term_inr(m), s) -> TERM_SUB(m, s)
TERM_SUB(Term_inl(m), s) -> TERM_SUB(m, s)
TERM_SUB(Term_pair(m, n), s) -> TERM_SUB(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(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)

Rules:

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)
Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
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_sum(psi, k, s)) -> Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) -> s

Termination of R could not be shown.
Duration:
0:00 minutes