Term Rewriting System R:
[x, y, z]
app(app(:, app(app(:, x), y)), z) -> app(app(:, x), app(app(:, y), z))
app(app(:, app(app(+, x), y)), z) -> app(app(+, app(app(:, x), z)), app(app(:, y), z))
app(app(:, z), app(app(+, x), app(f, y))) -> app(app(:, app(app(g, z), y)), app(app(+, x), a))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
APP(app(:, app(app(:, x), y)), z) -> APP(app(:, x), app(app(:, y), z))
APP(app(:, app(app(:, x), y)), z) -> APP(app(:, y), z)
APP(app(:, app(app(:, x), y)), z) -> APP(:, y)
APP(app(:, app(app(+, x), y)), z) -> APP(app(+, app(app(:, x), z)), app(app(:, y), z))
APP(app(:, app(app(+, x), y)), z) -> APP(+, app(app(:, x), z))
APP(app(:, app(app(+, x), y)), z) -> APP(app(:, x), z)
APP(app(:, app(app(+, x), y)), z) -> APP(:, x)
APP(app(:, app(app(+, x), y)), z) -> APP(app(:, y), z)
APP(app(:, app(app(+, x), y)), z) -> APP(:, y)
APP(app(:, z), app(app(+, x), app(f, y))) -> APP(app(:, app(app(g, z), y)), app(app(+, x), a))
APP(app(:, z), app(app(+, x), app(f, y))) -> APP(:, app(app(g, z), y))
APP(app(:, z), app(app(+, x), app(f, y))) -> APP(app(g, z), y)
APP(app(:, z), app(app(+, x), app(f, y))) -> APP(g, z)
APP(app(:, z), app(app(+, x), app(f, y))) -> APP(app(+, x), a)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Size-Change Principle
Dependency Pairs:
APP(app(:, app(app(+, x), y)), z) -> APP(app(:, y), z)
APP(app(:, app(app(+, x), y)), z) -> APP(app(:, x), z)
APP(app(:, app(app(:, x), y)), z) -> APP(app(:, y), z)
APP(app(:, app(app(:, x), y)), z) -> APP(app(:, x), app(app(:, y), z))
Rules:
app(app(:, app(app(:, x), y)), z) -> app(app(:, x), app(app(:, y), z))
app(app(:, app(app(+, x), y)), z) -> app(app(+, app(app(:, x), z)), app(app(:, y), z))
app(app(:, z), app(app(+, x), app(f, y))) -> app(app(:, app(app(g, z), y)), app(app(+, x), a))
The original DP problem is in applicative form. Its DPs and usable rules are the following.
APP(app(:, app(app(+, x), y)), z) -> APP(app(:, y), z)
APP(app(:, app(app(+, x), y)), z) -> APP(app(:, x), z)
APP(app(:, app(app(:, x), y)), z) -> APP(app(:, y), z)
APP(app(:, app(app(:, x), y)), z) -> APP(app(:, x), app(app(:, y), z))
app(app(:, app(app(:, x), y)), z) -> app(app(:, x), app(app(:, y), z))
app(app(:, app(app(+, x), y)), z) -> app(app(+, app(app(:, x), z)), app(app(:, y), z))
app(app(:, z), app(app(+, x), app(f, y))) -> app(app(:, app(app(g, z), y)), app(app(+, x), a))
It is proper and hence, it can be A-transformed which results in the DP problem
:'(+(x, y), z) -> :'(y, z)
:'(+(x, y), z) -> :'(x, z)
:'(:(x, y), z) -> :'(y, z)
:'(:(x, y), z) -> :'(x, :(y, z))
:(:(x, y), z) -> :(x, :(y, z))
:(+(x, y), z) -> +(:(x, z), :(y, z))
:(z, +(x, f(y))) -> :(g(z, y), +(x, a))
We number the DPs as follows:
- :'(+(x, y), z) -> :'(y, z)
- :'(+(x, y), z) -> :'(x, z)
- :'(:(x, y), z) -> :'(y, z)
- :'(:(x, y), z) -> :'(x, :(y, 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 |
|
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 |
|
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
+(x1, x2) -> +(x1, x2)
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes