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
↳Polynomial 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
POL(if(x1, x2, x3)) = 0 POL(0) = 0 POL(-'(x1, x2)) = x2 POL(greater(x1, x2)) = 0 POL(s(x1)) = 1 + x1 POL(-(x1, x2)) = x1 POL(p(x1)) = x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Polo
...
→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