Term Rewriting System R:
[x, y, z]
*(x, *(y, z)) -> *(otimes(x, y), z)
*(1, y) -> y
*(+(x, y), z) -> oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
*'(x, *(y, z)) -> *'(otimes(x, y), z)
*'(+(x, y), z) -> *'(x, z)
*'(+(x, y), z) -> *'(y, z)
*'(x, oplus(y, z)) -> *'(x, y)
*'(x, oplus(y, z)) -> *'(x, z)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
Dependency Pairs:
*'(x, oplus(y, z)) -> *'(x, z)
*'(x, oplus(y, z)) -> *'(x, y)
*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
Rules:
*(x, *(y, z)) -> *(otimes(x, y), z)
*(1, y) -> y
*(+(x, y), z) -> oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))
Strategy:
innermost
As we are in the innermost case, we can delete all 4 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Size-Change Principle
Dependency Pairs:
*'(x, oplus(y, z)) -> *'(x, z)
*'(x, oplus(y, z)) -> *'(x, y)
*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
Rule:
none
Strategy:
innermost
We number the DPs as follows:
- *'(x, oplus(y, z)) -> *'(x, z)
- *'(x, oplus(y, z)) -> *'(x, y)
- *'(+(x, y), z) -> *'(y, z)
- *'(+(x, y), z) -> *'(x, z)
and get the following Size-Change Graph(s): | {1, 2, 3, 4} | , | {1, 2, 3, 4} |
|---|
| 1 | = | 1 |
| 2 | > | 2 |
|
| {1, 2, 3, 4} | , | {1, 2, 3, 4} |
|---|
| 1 | > | 1 |
| 2 | = | 2 |
|
which lead(s) to this/these maximal multigraph(s): | {1, 2, 3, 4} | , | {1, 2, 3, 4} |
|---|
| 1 | > | 1 |
| 2 | = | 2 |
|
| {1, 2, 3, 4} | , | {1, 2, 3, 4} |
|---|
| 1 | = | 1 |
| 2 | > | 2 |
|
| {1, 2, 3, 4} | , | {1, 2, 3, 4} |
|---|
| 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:
oplus(x1, x2) -> oplus(x1, x2)
+(x1, x2) -> +(x1, x2)
We obtain no new DP problems.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes