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

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

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 w.r.t. to the implicit AFS 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

         ↳Polo

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 w.r.t. to the implicit AFS 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

         ↳Polo

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

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

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 w.r.t. to the implicit AFS 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₃

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 6

             ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

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 w.r.t. to the implicit AFS 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_usual(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

         ↳Polo

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

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

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

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(Term_inl(x₁)) = x₁

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

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

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

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

POL(Term_inr(x₁)) = x₁

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

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

POL(Sum_sub(x₁, x₂)) = 0

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

POL(Sum_term_var(x₁)) = 0

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

POL(Id) = 0

POL(Left) = 0

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

POL(Sum_constant(x₁)) = 0

POL(Right) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

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

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 9

                 ↳Polynomial Ordering

Dependency Pairs:

CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)
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)
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 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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(Term_inl(x₁)) = x₁

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

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

POL(Term_sub(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₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 10

                 ↳Dependency Graph

Dependency Pairs:

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

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

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 11

                 ↳Polynomial Ordering

Dependency Pairs:

CONCAT(Cons_sum(xi, k, 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

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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 13

                 ↳Polynomial 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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 15

                 ↳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.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 12

                 ↳Polynomial Ordering

Dependency Pairs:

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

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(Term_inr(x₁)) = x₁

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 14

                 ↳Polynomial Ordering

Dependency Pairs:

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

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(Term_inr(x₁)) = x₁

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 16

                 ↳Polynomial Ordering

Dependency Pairs:

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_inr(m), s) -> TERM_SUB(m, 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)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(Term_inr(x₁)) = x₁

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 17

                 ↳Polynomial Ordering

Dependency Pair:

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

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳DGraph

...

               →DP Problem 18

                 ↳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:07 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₃))	= 1 + x₃
POL(Cons_usual(x₁, x₂, x₃))	= x₃

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

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