R
↳Dependency Pair Analysis
+'(s(x), y) -> +'(x, y)
-'(s(x), s(y)) -> -'(x, y)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
+'(s(x), y) -> +'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
-(0, y) -> 0
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
+'(s(x), y) -> +'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
-(0, y) -> 0
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
+ > s
+'(x1, x2) -> +'(x1, x2)
s(x1) -> s(x1)
+(x1, x2) -> +(x1, x2)
-(x1, x2) -> -(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳AFS
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
-(0, y) -> 0
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
-'(s(x), s(y)) -> -'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
-(0, y) -> 0
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
-'(s(x), s(y)) -> -'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
-(0, y) -> 0
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
+ > s
-'(x1, x2) -> -'(x1, x2)
s(x1) -> s(x1)
+(x1, x2) -> +(x1, x2)
-(x1, x2) -> -(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 4
↳Dependency Graph
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
-(0, y) -> 0
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)