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

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Remaining

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

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 using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 4

             ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Remaining

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

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 using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 4

             ↳Polo

...

               →DP Problem 5

                 ↳Dependency Graph

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Remaining

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

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Remaining

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

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 using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(Term_var(x₁)) = 0

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 6

             ↳Polynomial Ordering

       →DP Problem 3

         ↳Remaining

Dependency Pair:

TERM_SUB(Term_var(x), Cons_sum(xi, k, 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

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 using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(Term_var(x₁)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 6

             ↳Polo

...

               →DP Problem 7

                 ↳Dependency Graph

       →DP Problem 3

         ↳Remaining

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

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Remaining Obligation(s)

The following remains to be proven:
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

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

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