Term Rewriting System R:
[m, xi, n, s, x, y, k, t, psi, u]
Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)
TERMSUB(Case(m, xi, n), s) -> SUMSUB(xi, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
TERMSUB(Terminr(m), s) -> TERMSUB(m, s)
TERMSUB(Termvar(x), Consusual(y, m, s)) -> TERMSUB(Termvar(x), s)
TERMSUB(Termvar(x), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)
TERMSUB(Termsub(m, s), t) -> TERMSUB(m, Concat(s, t))
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
SUMSUB(xi, Conssum(psi, k, s)) -> SUMSUB(xi, s)
SUMSUB(xi, Consusual(y, m, s)) -> SUMSUB(xi, s)
CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)

Furthermore, R contains three SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Usable Rules (Innermost)
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules


Dependency Pairs:

SUMSUB(xi, Consusual(y, m, s)) -> SUMSUB(xi, s)
SUMSUB(xi, Conssum(psi, k, s)) -> SUMSUB(xi, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




As we are in the innermost case, we can delete all 21 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 4
             ↳Size-Change Principle
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules


Dependency Pairs:

SUMSUB(xi, Consusual(y, m, s)) -> SUMSUB(xi, s)
SUMSUB(xi, Conssum(psi, k, s)) -> SUMSUB(xi, s)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. SUMSUB(xi, Consusual(y, m, s)) -> SUMSUB(xi, s)
  2. SUMSUB(xi, Conssum(psi, k, s)) -> SUMSUB(xi, s)
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
1=1
2>2

which lead(s) to this/these maximal multigraph(s):
{1, 2} , {1, 2}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳Usable Rules (Innermost)
       →DP Problem 3
         ↳UsableRules


Dependency Pairs:

TERMSUB(Termvar(x), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)
TERMSUB(Termvar(x), Consusual(y, m, s)) -> TERMSUB(Termvar(x), s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




As we are in the innermost case, we can delete all 21 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 5
             ↳Size-Change Principle
       →DP Problem 3
         ↳UsableRules


Dependency Pairs:

TERMSUB(Termvar(x), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)
TERMSUB(Termvar(x), Consusual(y, m, s)) -> TERMSUB(Termvar(x), s)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. TERMSUB(Termvar(x), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)
  2. TERMSUB(Termvar(x), Consusual(y, m, s)) -> TERMSUB(Termvar(x), s)
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
1=1
2>2

which lead(s) to this/these maximal multigraph(s):
{1, 2} , {1, 2}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
Termvar(x1) -> Termvar(x1)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳Usable Rules (Innermost)


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
TERMSUB(Terminr(m), s) -> TERMSUB(m, s)
TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




As we are in the innermost case, we can delete all 17 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 6
             ↳Size-Change Principle


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
TERMSUB(Terminr(m), s) -> TERMSUB(m, s)
TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)


Strategy:

innermost




We number the DPs as follows:
  1. FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
  2. FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
  3. FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
  4. CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
  5. CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
  6. CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
  7. CONCAT(Concat(s, t), u) -> CONCAT(t, u)
  8. TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
  9. TERMSUB(Terminr(m), s) -> TERMSUB(m, s)
  10. TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
  11. TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
  12. TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
  13. TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
  14. TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
  15. FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
  16. TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)
and get the following Size-Change Graph(s):
{1, 2, 3, 15} , {1, 2, 3, 15}
3=1
4=2
{1, 2, 3, 15} , {1, 2, 3, 15}
1=1
4=2
{4, 5, 7} , {4, 5, 7}
1>1
2=2
{6} , {6}
1>1
2=2
{8} , {8}
1>1
2=2
{9, 10, 11, 12, 13, 14} , {9, 10, 11, 12, 13, 14}
1>1
2=2
{16} , {16}
1>1
1>3
2=4

which lead(s) to this/these maximal multigraph(s):
{4, 5, 7} , {4, 5, 7}
1>1
2=2
{9, 10, 11, 12, 13, 14} , {9, 10, 11, 12, 13, 14}
1>1
2=2
{8} , {6}
1>1
2=2
{1, 2, 3, 15} , {16}
3>1
3>3
4=4
{6} , {8}
1>1
2=2
{16} , {1, 2, 3, 15}
1>1
2=2
{1, 2, 3, 15} , {16}
1>1
1>3
4=4
{4, 5, 7} , {8}
1>1
2=2
{8} , {9, 10, 11, 12, 13, 14}
1>1
2=2
{9, 10, 11, 12, 13, 14} , {1, 2, 3, 15}
1>1
2=2
{6} , {4, 5, 7}
1>1
2=2
{9, 10, 11, 12, 13, 14} , {6}
1>1
2=2
{16} , {9, 10, 11, 12, 13, 14}
1>1
2=2
{8} , {1, 2, 3, 15}
1>1
2=2
{16} , {6}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
Terminl(x1) -> Terminl(x1)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Terminr(x1) -> Terminr(x1)
Termsub(x1, x2) -> Termsub(x1, x2)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
Termapp(x1, x2) -> Termapp(x1, x2)
Termpair(x1, x2) -> Termpair(x1, x2)
Sumtermvar(x1) -> Sumtermvar(x1)
Concat(x1, x2) -> Concat(x1, x2)
Case(x1, x2, x3) -> Case(x1, x2, x3)
Sumconstant(x1) -> Sumconstant(x1)

We obtain no new DP problems.

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