Term Rewriting System R:
[y, x]
ack(0, y) -> succ(y)
ack(succ(x), y) -> ack(x, succ(0))
ack(succ(x), succ(y)) -> ack(x, ack(succ(x), y))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
ACK(succ(x), y) -> ACK(x, succ(0))
ACK(succ(x), succ(y)) -> ACK(x, ack(succ(x), y))
ACK(succ(x), succ(y)) -> ACK(succ(x), y)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Size-Change Principle
Dependency Pairs:
ACK(succ(x), succ(y)) -> ACK(succ(x), y)
ACK(succ(x), succ(y)) -> ACK(x, ack(succ(x), y))
ACK(succ(x), y) -> ACK(x, succ(0))
Rules:
ack(0, y) -> succ(y)
ack(succ(x), y) -> ack(x, succ(0))
ack(succ(x), succ(y)) -> ack(x, ack(succ(x), y))
We number the DPs as follows:
- ACK(succ(x), succ(y)) -> ACK(succ(x), y)
- ACK(succ(x), succ(y)) -> ACK(x, ack(succ(x), y))
- ACK(succ(x), y) -> ACK(x, succ(0))
and get the following Size-Change Graph(s): {3, 2, 1} | , | {3, 2, 1} |
---|
1 | = | 1 |
2 | > | 2 |
|
|
which lead(s) to this/these maximal multigraph(s): {3, 2, 1} | , | {3, 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:
succ(x1) -> succ(x1)
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes