Term Rewriting System R:
[x, y, z]
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
PLUS(s(x), y) -> PLUS(x, y)
TIMES(s(x), y) -> PLUS(y, times(x, y))
TIMES(s(x), y) -> TIMES(x, y)
DIV(x, y) -> QUOT(x, y, y)
DIV(div(x, y), z) -> DIV(x, times(y, z))
DIV(div(x, y), z) -> TIMES(y, z)
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
QUOT(x, 0, s(z)) -> DIV(x, s(z))
Furthermore, R contains three SCCs.
R
↳DPs
→DP Problem 1
↳Size-Change Principle
→DP Problem 2
↳SCP
→DP Problem 3
↳AFS
Dependency Pair:
PLUS(s(x), y) -> PLUS(x, y)
Rules:
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
We number the DPs as follows:
- PLUS(s(x), y) -> PLUS(x, y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s(x1) -> s(x1)
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Size-Change Principle
→DP Problem 3
↳AFS
Dependency Pair:
TIMES(s(x), y) -> TIMES(x, y)
Rules:
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
We number the DPs as follows:
- TIMES(s(x), y) -> TIMES(x, y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s(x1) -> s(x1)
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳Argument Filtering and Ordering
Dependency Pairs:
DIV(div(x, y), z) -> DIV(x, times(y, z))
QUOT(x, 0, s(z)) -> DIV(x, s(z))
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
DIV(x, y) -> QUOT(x, y, y)
Rules:
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
The following dependency pair can be strictly oriented:
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
There are no usable rules w.r.t. the AFS that need to be oriented.
Used ordering: Lexicographic Path Order with Precedence:
trivial
resulting in one new DP problem.
Used Argument Filtering System: DIV(x1, x2) -> x1
div(x1, x2) -> x1
QUOT(x1, x2, x3) -> x1
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳AFS
→DP Problem 4
↳Argument Filtering and Ordering
Dependency Pairs:
DIV(div(x, y), z) -> DIV(x, times(y, z))
QUOT(x, 0, s(z)) -> DIV(x, s(z))
DIV(x, y) -> QUOT(x, y, y)
Rules:
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
The following dependency pair can be strictly oriented:
DIV(div(x, y), z) -> DIV(x, times(y, z))
There are no usable rules w.r.t. the AFS that need to be oriented.
Used ordering: Lexicographic Path Order with Precedence:
trivial
resulting in one new DP problem.
Used Argument Filtering System: DIV(x1, x2) -> x1
div(x1, x2) -> div(x1, x2)
QUOT(x1, x2, x3) -> x1
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
...
→DP Problem 5
↳Instantiation Transformation
Dependency Pairs:
QUOT(x, 0, s(z)) -> DIV(x, s(z))
DIV(x, y) -> QUOT(x, y, y)
Rules:
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule
DIV(x, y) -> QUOT(x, y, y)
one new Dependency Pair
is created:
DIV(x'', s(z'')) -> QUOT(x'', s(z''), s(z''))
The transformation is resulting in no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes