Term Rewriting System R:
[y, x]
-(0, y) -> 0
-(x, 0) -> x
-(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) -> 0
p(s(x)) -> x
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
-'(x, s(y)) -> -'(x, p(s(y)))
-'(x, s(y)) -> P(s(y))
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
Dependency Pair:
-'(x, s(y)) -> -'(x, p(s(y)))
Rules:
-(0, y) -> 0
-(x, 0) -> x
-(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) -> 0
p(s(x)) -> x
On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule
-'(x, s(y)) -> -'(x, p(s(y)))
one new Dependency Pair
is created:
-'(x, s(y')) -> -'(x, y')
The transformation is resulting in one new DP problem:
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Argument Filtering and Ordering
Dependency Pair:
-'(x, s(y')) -> -'(x, y')
Rules:
-(0, y) -> 0
-(x, 0) -> x
-(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) -> 0
p(s(x)) -> x
The following dependency pair can be strictly oriented:
-'(x, s(y')) -> -'(x, y')
There are no usable rules using the Ce-refinement that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System: -'(x1, x2) -> -'(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳AFS
...
→DP Problem 3
↳Dependency Graph
Dependency Pair:
Rules:
-(0, y) -> 0
-(x, 0) -> x
-(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) -> 0
p(s(x)) -> x
Using the Dependency Graph resulted in no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes