R
↳Dependency Pair Analysis
+'(+(x, y), z) -> +'(x, +(y, z))
+'(+(x, y), z) -> +'(y, z)
*'(x, +(y, z)) -> +'(*(x, y), *(x, z))
*'(x, +(y, z)) -> *'(x, y)
*'(x, +(y, z)) -> *'(x, z)
*'(+(x, y), z) -> +'(*(x, z), *(y, z))
*'(+(x, y), z) -> *'(x, z)
*'(+(x, y), z) -> *'(y, z)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
+'(+(x, y), z) -> +'(y, z)
+'(+(x, y), z) -> +'(x, +(y, z))
+(x, 0) -> x
+(x, i(x)) -> 0
+(+(x, y), z) -> +(x, +(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))
+'(+(x, y), z) -> +'(y, z)
+(x, 0) -> x
+(x, i(x)) -> 0
+(+(x, y), z) -> +(x, +(y, z))
POL(0) = 0 POL(i(x1)) = x1 POL(+(x1, x2)) = 1 + x1 + x2 POL(+'(x1, x2)) = 1 + x1 + x2
+'(x1, x2) -> +'(x1, x2)
+(x1, x2) -> +(x1, x2)
i(x1) -> i(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
+'(+(x, y), z) -> +'(x, +(y, z))
+(x, 0) -> x
+(x, i(x)) -> 0
+(+(x, y), z) -> +(x, +(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))
+'(+(x, y), z) -> +'(x, +(y, z))
POL(+(x1, x2)) = 1 + x1 + x2
+'(x1, x2) -> x1
+(x1, x2) -> +(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳AFS
...
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳AFS
+(x, 0) -> x
+(x, i(x)) -> 0
+(+(x, y), z) -> +(x, +(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, y)
+(x, 0) -> x
+(x, i(x)) -> 0
+(+(x, y), z) -> +(x, +(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))
*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, y)
POL(*'(x1, x2)) = x1 + x2 POL(+(x1, x2)) = 1 + x1 + x2
*'(x1, x2) -> *'(x1, x2)
+(x1, x2) -> +(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳Dependency Graph
+(x, 0) -> x
+(x, i(x)) -> 0
+(+(x, y), z) -> +(x, +(y, z))
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(x, y), z) -> +(*(x, z), *(y, z))