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.


R contains the following Dependency Pairs: 


   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_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_pair(m, n), s) -> TERM_SUB(m, s)
   TERM_SUB(Term_pair(m, n), s) -> TERM_SUB(n, s)
   TERM_SUB(Term_sub(m, s), t) -> TERM_SUB(m, Concat(s, t))
   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)
   TERM_SUB(Case(m, xi, n), s) -> SUM_SUB(xi, s)
   TERM_SUB(Term_inr(m), s) -> TERM_SUB(m, s)
   TERM_SUB(Term_inl(m), s) -> TERM_SUB(m, s)
   SUM_SUB(xi, Cons_usual(y, m, s)) -> SUM_SUB(xi, s)
   SUM_SUB(xi, Cons_sum(psi, k, s)) -> SUM_SUB(xi, s)
   CONCAT(Cons_sum(xi, k, s), t) -> CONCAT(s, t)
   CONCAT(Cons_usual(x, m, s), t) -> TERM_SUB(m, t)
   CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)
   CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
   CONCAT(Concat(s, t), u) -> CONCAT(t, u)
   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)

Furthermore, R contains three SCCs.


SCC1:

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

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(SUM_SUB(x_1, x_2)) = 1 + x_1 + x_2
POL(Cons_usual(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3
POL(Cons_sum(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.


SCC2:

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)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(Term_var(x_1)) = 1 + x_1
POL(Cons_usual(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3
POL(Cons_sum(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3
POL(TERM_SUB(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   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)



 This transformation is resulting in no new subcycles.


SCC3:

CONCAT(Concat(s, t), u) -> CONCAT(t, u)
CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)
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)
TERM_SUB(Term_inl(m), s) -> TERM_SUB(m, s)
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)
CONCAT(Cons_usual(x, m, s), t) -> TERM_SUB(m, t)
CONCAT(Cons_sum(xi, k, s), t) -> CONCAT(s, t)
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_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)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(Term_sub(x_1, x_2)) = x_1 + x_2
POL(Term_app(x_1, x_2)) = x_1 + x_2
POL(Term_var(x_1)) = 0
POL(Term_inr(x_1)) = x_1
POL(Term_pair(x_1, x_2)) = x_1 + x_2
POL(Case(x_1, x_2, x_3)) = x_1 + x_3
POL(FROZEN(x_1, x_2, x_3, x_4)) = x_1 + x_3
POL(Frozen(x_1, x_2, x_3, x_4)) = 0
POL(CONCAT(x_1, x_2)) = x_1
POL(Cons_sum(x_1, x_2, x_3)) = x_3
POL(TERM_SUB(x_1, x_2)) = x_1
POL(Right) = 0
POL(Sum_term_var(x_1)) = 0
POL(Term_inl(x_1)) = x_1
POL(Left) = 0
POL(Id) = 0
POL(Sum_constant(x_1)) = 0
POL(Cons_usual(x_1, x_2, x_3)) = x_2 + x_3
POL(Concat(x_1, x_2)) = 1 + x_1 + x_2
POL(Sum_sub(x_1, x_2)) = 0

 resulting in one subcycle.


SCC3.Polo1:

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)
TERM_SUB(Term_inl(m), s) -> TERM_SUB(m, s)
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)
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_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(Cons_sum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(Term_sub(x_1, x_2)) = x_1 + x_2
POL(Term_app(x_1, x_2)) = x_1 + x_2
POL(Term_var(x_1)) = 0
POL(Term_inr(x_1)) = x_1
POL(Term_pair(x_1, x_2)) = x_1 + x_2
POL(Case(x_1, x_2, x_3)) = 1 + x_1 + x_3
POL(FROZEN(x_1, x_2, x_3, x_4)) = 1 + x_1 + x_3
POL(Frozen(x_1, x_2, x_3, x_4)) = 0
POL(CONCAT(x_1, x_2)) = x_1
POL(Cons_sum(x_1, x_2, x_3)) = x_3
POL(TERM_SUB(x_1, x_2)) = x_1
POL(Right) = 0
POL(Sum_term_var(x_1)) = 0
POL(Term_inl(x_1)) = x_1
POL(Left) = 0
POL(Id) = 0
POL(Cons_usual(x_1, x_2, x_3)) = x_2 + x_3
POL(Sum_constant(x_1)) = 0
POL(Concat(x_1, x_2)) = 0
POL(Sum_sub(x_1, x_2)) = 0

 resulting in one subcycle.


SCC3.Polo1.Polo1:

CONCAT(Cons_usual(x, m, s), t) -> CONCAT(s, t)
TERM_SUB(Term_inr(m), s) -> TERM_SUB(m, s)
CONCAT(Cons_usual(x, m, s), t) -> TERM_SUB(m, t)
CONCAT(Cons_sum(xi, k, s), t) -> CONCAT(s, t)
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_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_inl(m), s) -> TERM_SUB(m, s)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(Term_sub(x_1, x_2)) = 1 + x_1 + x_2
POL(Term_app(x_1, x_2)) = 1 + x_1 + x_2
POL(Term_var(x_1)) = 0
POL(Term_pair(x_1, x_2)) = 1 + x_1 + x_2
POL(Case(x_1, x_2, x_3)) = 0
POL(Term_inr(x_1)) = 1 + x_1
POL(Frozen(x_1, x_2, x_3, x_4)) = 0
POL(CONCAT(x_1, x_2)) = x_1
POL(Cons_sum(x_1, x_2, x_3)) = 1 + x_3
POL(TERM_SUB(x_1, x_2)) = x_1
POL(Right) = 0
POL(Sum_term_var(x_1)) = 0
POL(Term_inl(x_1)) = 1 + x_1
POL(Left) = 0
POL(Id) = 0
POL(Cons_usual(x_1, x_2, x_3)) = 1 + x_2 + x_3
POL(Sum_constant(x_1)) = 0
POL(Concat(x_1, x_2)) = 0
POL(Sum_sub(x_1, x_2)) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 2.90 seconds.