R
↳Dependency Pair Analysis
-'(x, s(y)) -> -'(x, p(s(y)))
-'(x, s(y)) -> P(s(y))
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
-'(x, s(y)) -> -'(x, p(s(y)))
-(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
one new Dependency Pair is created:
-'(x, s(y)) -> -'(x, p(s(y)))
-'(x, s(y')) -> -'(x, y')
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Argument Filtering and Ordering
-'(x, s(y')) -> -'(x, y')
-(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
-'(x, s(y')) -> -'(x, y')
-(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
- > greater
-'(x1, x2) -> -'(x1, x2)
s(x1) -> s(x1)
-(x1, x2) -> -(x1, x2)
if(x1, x2, x3) -> x1
greater(x1, x2) -> greater(x1, x2)
p(x1) -> p(x1)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳AFS
...
→DP Problem 3
↳Dependency Graph
-(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