R
↳Dependency Pair Analysis
+'(s(x), y) -> +'(x, y)
+'(s(x), y) -> +'(x, s(y))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
+'(s(x), y) -> +'(x, s(y))
+'(s(x), y) -> +'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(s(x), y) -> +(x, s(y))
+'(s(x), y) -> +'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(s(x), y) -> +(x, s(y))
POL(0) = 0 POL(s(x1)) = 1 + x1 POL(+(x1, x2)) = x1 + x2 POL(+'(x1, x2)) = 1 + x1 + x2
+'(x1, x2) -> +'(x1, x2)
s(x1) -> s(x1)
+(x1, x2) -> +(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Instantiation Transformation
+'(s(x), y) -> +'(x, s(y))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(s(x), y) -> +(x, s(y))
one new Dependency Pair is created:
+'(s(x), y) -> +'(x, s(y))
+'(s(x''), s(y'')) -> +'(x'', s(s(y'')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Inst
...
→DP Problem 3
↳Instantiation Transformation
+'(s(x''), s(y'')) -> +'(x'', s(s(y'')))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(s(x), y) -> +(x, s(y))
one new Dependency Pair is created:
+'(s(x''), s(y'')) -> +'(x'', s(s(y'')))
+'(s(x''''), s(s(y''''))) -> +'(x'''', s(s(s(y''''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Inst
...
→DP Problem 4
↳Argument Filtering and Ordering
+'(s(x''''), s(s(y''''))) -> +'(x'''', s(s(s(y''''))))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(s(x), y) -> +(x, s(y))
+'(s(x''''), s(s(y''''))) -> +'(x'''', s(s(s(y''''))))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(s(x), y) -> +(x, s(y))
POL(0) = 1 POL(s(x1)) = 1 + x1 POL(+(x1, x2)) = x1 + x2
+'(x1, x2) -> x1
s(x1) -> s(x1)
+(x1, x2) -> +(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Inst
...
→DP Problem 5
↳Dependency Graph
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(s(x), y) -> +(x, s(y))