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

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
         ↳Size-Change Principle
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP


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





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):
{2, 1} , {2, 1}
1=1
2>2

which lead(s) to this/these maximal multigraph(s):
{2, 1} , {2, 1}
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
         ↳SCP
       →DP Problem 2
         ↳Size-Change Principle
       →DP Problem 3
         ↳SCP


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





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):
{2, 1} , {2, 1}
1=1
2>2

which lead(s) to this/these maximal multigraph(s):
{2, 1} , {2, 1}
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
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳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)
CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
TERMSUB(Termsub(m, s), t) -> TERMSUB(m, 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





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. CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
  9. TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
  10. TERMSUB(Termsub(m, s), t) -> TERMSUB(m, Concat(s, t))
  11. TERMSUB(Terminr(m), s) -> TERMSUB(m, s)
  12. TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
  13. TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
  14. TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
  15. TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
  16. TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
  17. FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
  18. TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)
and get the following Size-Change Graph(s):
{17, 3, 2, 1} , {17, 3, 2, 1}
3=1
4=2
{17, 3, 2, 1} , {17, 3, 2, 1}
1=1
4=2
{8, 7, 5, 4} , {8, 7, 5, 4}
1>1
2=2
{6} , {6}
1>1
2=2
{8, 7, 5, 4} , {8, 7, 5, 4}
1>1
{9} , {9}
1>1
2=2
{16, 15, 14, 13, 12, 11, 10} , {16, 15, 14, 13, 12, 11, 10}
1>1
{16, 15, 14, 13, 12, 11, 10} , {16, 15, 14, 13, 12, 11, 10}
1>1
2=2
{18} , {18}
1>1
1>3
2=4

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

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)
Case(x1, x2, x3) -> Case(x1, x2, x3)
Sumconstant(x1) -> Sumconstant(x1)

We obtain no new DP problems.

Termination of R successfully shown.
Duration:
0:01 minutes