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

Innermost 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

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

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

Strategy:

innermost

The following dependency pair can be strictly oriented:

SUM_SUB(xi, Cons_usual(y, m, s)) -> SUM_SUB(xi, s)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(SUM_SUB(x₁, x₂)) = x₁ + x₂

POL(Cons_sum(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Cons_usual(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

resulting in one new DP problem.
Used Argument Filtering System:

SUM_SUB(x₁, x₂) -> SUM_SUB(x₁, x₂)
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 4

             ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

Dependency Pair:

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

Strategy:

innermost

The following dependency pair can be strictly oriented:

SUM_SUB(xi, Cons_sum(psi, k, s)) -> SUM_SUB(xi, s)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(SUM_SUB(x₁, x₂)) = x₁ + x₂

POL(Cons_sum(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

resulting in one new DP problem.
Used Argument Filtering System:

SUM_SUB(x₁, x₂) -> SUM_SUB(x₁, x₂)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 4

             ↳AFS

...

               →DP Problem 5

                 ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

Dependency Pair:

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

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳AFS

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

Strategy:

innermost

The following dependency pair can be strictly oriented:

TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) -> TERM_SUB(Term_var(x), s)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(Term_var(x₁)) = x₁

POL(Cons_sum(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

POL(Cons_usual(x₁, x₂, x₃)) = x₁ + x₂ + x₃

resulting in one new DP problem.
Used Argument Filtering System:

TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Term_var(x₁) -> Term_var(x₁)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 6

             ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳AFS

Dependency Pair:

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

Strategy:

innermost

The following dependency pair can be strictly oriented:

TERM_SUB(Term_var(x), Cons_usual(y, m, s)) -> TERM_SUB(Term_var(x), s)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(Term_var(x₁)) = x₁

POL(Cons_usual(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

resulting in one new DP problem.
Used Argument Filtering System:

TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Term_var(x₁) -> Term_var(x₁)
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 6

             ↳AFS

...

               →DP Problem 7

                 ↳Dependency Graph

       →DP Problem 3

         ↳AFS

Dependency Pair:

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

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Argument Filtering and Ordering

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)
TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
TERM_SUB(Term_inr(m), s) -> TERM_SUB(m, s)
TERM_SUB(Term_inl(m), s) -> TERM_SUB(m, s)
TERM_SUB(Term_pair(m, n), s) -> TERM_SUB(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

Strategy:

innermost

The following dependency pair can be strictly oriented:

TERM_SUB(Term_inl(m), s) -> TERM_SUB(m, s)

The following usable rules for innermost can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(Term_inl(x₁)) = 1 + x₁

POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄

POL(Cons_sum(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Cons_usual(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Term_sub(x₁, x₂)) = x₁ + x₂

POL(Term_inr(x₁)) = x₁

POL(Term_app(x₁, x₂)) = x₁ + x₂

POL(Term_pair(x₁, x₂)) = x₁ + x₂

POL(CONCAT(x₁, x₂)) = x₁ + x₂

POL(Sum_term_var(x₁)) = x₁

POL(Concat(x₁, x₂)) = x₁ + x₂

POL(Case(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Sum_constant) = 0

resulting in one new DP problem.
Used Argument Filtering System:

TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Term_inl(x₁) -> Term_inl(x₁)
Term_app(x₁, x₂) -> Term_app(x₁, x₂)
Term_pair(x₁, x₂) -> Term_pair(x₁, x₂)
CONCAT(x₁, x₂) -> CONCAT(x₁, x₂)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)
FROZEN(x₁, x₂, x₃, x₄) -> FROZEN(x₁, x₂, x₃, x₄)
Sum_constant(x₁) -> Sum_constant
Term_sub(x₁, x₂) -> Term_sub(x₁, x₂)
Concat(x₁, x₂) -> Concat(x₁, x₂)
Sum_{term_var}(x₁) -> Sum_{term_var}(x₁)
Term_inr(x₁) -> Term_inr(x₁)
Case(x₁, x₂, x₃) -> Case(x₁, x₂, x₃)
Sum_sub(x₁, x₂) -> x₁

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳Argument Filtering and Ordering

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)
TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
TERM_SUB(Term_inr(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

Strategy:

innermost

The following dependency pairs can be strictly oriented:

TERM_SUB(Term_pair(m, n), s) -> TERM_SUB(n, s)
TERM_SUB(Term_pair(m, n), s) -> TERM_SUB(m, s)

The following usable rules for innermost can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄

POL(Cons_sum(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Cons_usual(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Term_sub(x₁, x₂)) = x₁ + x₂

POL(Term_inr(x₁)) = x₁

POL(Term_app(x₁, x₂)) = x₁ + x₂

POL(Term_pair(x₁, x₂)) = 1 + x₁ + x₂

POL(CONCAT(x₁, x₂)) = x₁ + x₂

POL(Sum_term_var(x₁)) = x₁

POL(Concat(x₁, x₂)) = x₁ + x₂

POL(Case(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Sum_constant) = 0

resulting in one new DP problem.
Used Argument Filtering System:

TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Term_pair(x₁, x₂) -> Term_pair(x₁, x₂)
Term_app(x₁, x₂) -> Term_app(x₁, x₂)
CONCAT(x₁, x₂) -> CONCAT(x₁, x₂)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)
FROZEN(x₁, x₂, x₃, x₄) -> FROZEN(x₁, x₂, x₃, x₄)
Sum_constant(x₁) -> Sum_constant
Term_sub(x₁, x₂) -> Term_sub(x₁, x₂)
Concat(x₁, x₂) -> Concat(x₁, x₂)
Sum_{term_var}(x₁) -> Sum_{term_var}(x₁)
Term_inr(x₁) -> Term_inr(x₁)
Case(x₁, x₂, x₃) -> Case(x₁, x₂, x₃)
Sum_sub(x₁, x₂) -> x₁

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 9

                 ↳Argument Filtering and Ordering

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)
TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
TERM_SUB(Term_inr(m), 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

Strategy:

innermost

The following dependency pairs can be strictly oriented:

TERM_SUB(Term_app(m, n), s) -> TERM_SUB(n, s)
TERM_SUB(Term_app(m, n), s) -> TERM_SUB(m, s)

The following usable rules for innermost can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(Sum_term_var(x₁)) = x₁

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(Concat(x₁, x₂)) = x₁ + x₂

POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄

POL(Case(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Cons_sum(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Cons_usual(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Term_sub(x₁, x₂)) = x₁ + x₂

POL(Term_inr(x₁)) = x₁

POL(Term_app(x₁, x₂)) = 1 + x₁ + x₂

POL(Sum_constant) = 0

POL(CONCAT(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Term_app(x₁, x₂) -> Term_app(x₁, x₂)
CONCAT(x₁, x₂) -> CONCAT(x₁, x₂)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)
FROZEN(x₁, x₂, x₃, x₄) -> FROZEN(x₁, x₂, x₃, x₄)
Sum_constant(x₁) -> Sum_constant
Term_sub(x₁, x₂) -> Term_sub(x₁, x₂)
Concat(x₁, x₂) -> Concat(x₁, x₂)
Sum_{term_var}(x₁) -> Sum_{term_var}(x₁)
Term_inr(x₁) -> Term_inr(x₁)
Case(x₁, x₂, x₃) -> Case(x₁, x₂, x₃)
Sum_sub(x₁, x₂) -> x₁

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 10

                 ↳Argument Filtering and Ordering

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)
TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
TERM_SUB(Term_inr(m), 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

Strategy:

innermost

The following dependency pair can be strictly oriented:

TERM_SUB(Term_inr(m), s) -> TERM_SUB(m, s)

The following usable rules for innermost can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(Sum_term_var(x₁)) = x₁

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(Concat(x₁, x₂)) = x₁ + x₂

POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄

POL(Case(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Cons_sum(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Term_inr(x₁)) = 1 + x₁

POL(Cons_usual(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Term_sub(x₁, x₂)) = x₁ + x₂

POL(Sum_constant) = 0

POL(CONCAT(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Term_inr(x₁) -> Term_inr(x₁)
FROZEN(x₁, x₂, x₃, x₄) -> FROZEN(x₁, x₂, x₃, x₄)
Sum_{term_var}(x₁) -> Sum_{term_var}(x₁)
CONCAT(x₁, x₂) -> CONCAT(x₁, x₂)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)
Case(x₁, x₂, x₃) -> Case(x₁, x₂, x₃)
Sum_sub(x₁, x₂) -> x₁
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)
Sum_constant(x₁) -> Sum_constant
Term_sub(x₁, x₂) -> Term_sub(x₁, x₂)
Concat(x₁, x₂) -> Concat(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 11

                 ↳Argument Filtering and Ordering

Dependency Pairs:

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

Strategy:

innermost

The following dependency pairs can be strictly oriented:

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)
FROZEN(m, Sum_constant(Left), n, s) -> TERM_SUB(m, s)

The following usable rules for innermost can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(Sum_term_var(x₁)) = x₁

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(Concat(x₁, x₂)) = x₁ + x₂

POL(FROZEN(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄

POL(Case(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

POL(Cons_sum(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Cons_usual(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Term_sub(x₁, x₂)) = x₁ + x₂

POL(Sum_constant) = 0

POL(CONCAT(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

FROZEN(x₁, x₂, x₃, x₄) -> FROZEN(x₁, x₂, x₃, x₄)
TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Sum_{term_var}(x₁) -> Sum_{term_var}(x₁)
CONCAT(x₁, x₂) -> CONCAT(x₁, x₂)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)
Case(x₁, x₂, x₃) -> Case(x₁, x₂, x₃)
Sum_sub(x₁, x₂) -> x₁
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)
Sum_constant(x₁) -> Sum_constant
Term_sub(x₁, x₂) -> Term_sub(x₁, x₂)
Concat(x₁, x₂) -> Concat(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 12

                 ↳Dependency Graph

Dependency Pairs:

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

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

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 13

                 ↳Argument Filtering and Ordering

Dependency Pairs:

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(Concat(s, t), u) -> CONCAT(t, u)
CONCAT(Cons_sum(xi, k, s), t) -> CONCAT(s, t)

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

Strategy:

innermost

The following dependency pair can be strictly oriented:

CONCAT(Cons_sum(xi, k, s), t) -> CONCAT(s, t)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(Concat(x₁, x₂)) = x₁ + x₂

POL(Cons_sum(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

POL(Cons_usual(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(Term_sub(x₁, x₂)) = x₁ + x₂

POL(CONCAT(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

CONCAT(x₁, x₂) -> CONCAT(x₁, x₂)
Cons_sum(x₁, x₂, x₃) -> Cons_sum(x₁, x₂, x₃)
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)
TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Term_sub(x₁, x₂) -> Term_sub(x₁, x₂)
Concat(x₁, x₂) -> Concat(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 14

                 ↳Argument Filtering and Ordering

Dependency Pairs:

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(Concat(s, t), u) -> CONCAT(t, u)

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

Strategy:

innermost

The following dependency pairs can be strictly oriented:

CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) -> TERM_SUB(m, t)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(TERM_SUB(x₁, x₂)) = x₁ + x₂

POL(Concat(x₁, x₂)) = x₁ + x₂

POL(Cons_usual(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

POL(Term_sub(x₁, x₂)) = x₁ + x₂

POL(CONCAT(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

CONCAT(x₁, x₂) -> CONCAT(x₁, x₂)
Cons_usual(x₁, x₂, x₃) -> Cons_usual(x₁, x₂, x₃)
TERM_SUB(x₁, x₂) -> TERM_SUB(x₁, x₂)
Term_sub(x₁, x₂) -> Term_sub(x₁, x₂)
Concat(x₁, x₂) -> Concat(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 15

                 ↳Dependency Graph

Dependency Pairs:

TERM_SUB(Term_sub(m, s), t) -> CONCAT(s, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)

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

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 16

                 ↳Argument Filtering and Ordering

Dependency Pair:

CONCAT(Concat(s, t), u) -> CONCAT(t, u)

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

Strategy:

innermost

The following dependency pair can be strictly oriented:

CONCAT(Concat(s, t), u) -> CONCAT(t, u)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(Concat(x₁, x₂)) = 1 + x₁ + x₂

POL(CONCAT(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

CONCAT(x₁, x₂) -> CONCAT(x₁, x₂)
Concat(x₁, x₂) -> Concat(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 8

             ↳AFS

...

               →DP Problem 17

                 ↳Dependency Graph

Dependency Pair:

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

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:22 minutes

POL(SUM_SUB(x₁, x₂))	= x₁ + x₂
POL(Cons_sum(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(Cons_usual(x₁, x₂, x₃))	= 1 + x₁ + x₂ + x₃

POL(TERM_SUB(x₁, x₂))	= x₁ + x₂
POL(Term_var(x₁))	= x₁
POL(Cons_sum(x₁, x₂, x₃))	= 1 + x₁ + x₂ + x₃
POL(Cons_usual(x₁, x₂, x₃))	= x₁ + x₂ + x₃

POL(TERM_SUB(x₁, x₂))	= x₁ + x₂
POL(Term_inl(x₁))	= 1 + x₁
POL(FROZEN(x₁, x₂, x₃, x₄))	= x₁ + x₂ + x₃ + x₄
POL(Cons_sum(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(Cons_usual(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(Term_sub(x₁, x₂))	= x₁ + x₂
POL(Term_inr(x₁))	= x₁
POL(Term_app(x₁, x₂))	= x₁ + x₂
POL(Term_pair(x₁, x₂))	= x₁ + x₂
POL(CONCAT(x₁, x₂))	= x₁ + x₂
POL(Sum_term_var(x₁))	= x₁
POL(Concat(x₁, x₂))	= x₁ + x₂
POL(Case(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(Sum_constant)	= 0

POL(Concat(x₁, x₂))	= 1 + x₁ + x₂
POL(CONCAT(x₁, x₂))	= x₁ + x₂