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