R
↳Dependency Pair Analysis
*'(x, *(y, z)) -> *'(otimes(x, y), z)
*'(+(x, y), z) -> *'(x, z)
*'(+(x, y), z) -> *'(y, z)
*'(x, oplus(y, z)) -> *'(x, y)
*'(x, oplus(y, z)) -> *'(x, z)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
*'(x, oplus(y, z)) -> *'(x, z)
*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
*'(x, oplus(y, z)) -> *'(x, y)
*'(x, *(y, z)) -> *'(otimes(x, y), z)
*(x, *(y, z)) -> *(otimes(x, y), z)
*(1, y) -> y
*(+(x, y), z) -> oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))
*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
POL(*'(x1, x2)) = x1 POL(otimes(x1, x2)) = 0 POL(*(x1, x2)) = 0 POL(oplus(x1, x2)) = 0 POL(+(x1, x2)) = 1 + x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
*'(x, oplus(y, z)) -> *'(x, z)
*'(x, oplus(y, z)) -> *'(x, y)
*'(x, *(y, z)) -> *'(otimes(x, y), z)
*(x, *(y, z)) -> *(otimes(x, y), z)
*(1, y) -> y
*(+(x, y), z) -> oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))
*'(x, oplus(y, z)) -> *'(x, z)
*'(x, oplus(y, z)) -> *'(x, y)
POL(*'(x1, x2)) = x2 POL(otimes(x1, x2)) = 0 POL(*(x1, x2)) = x2 POL(oplus(x1, x2)) = 1 + x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
...
→DP Problem 3
↳Instantiation Transformation
*'(x, *(y, z)) -> *'(otimes(x, y), z)
*(x, *(y, z)) -> *(otimes(x, y), z)
*(1, y) -> y
*(+(x, y), z) -> oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))
one new Dependency Pair is created:
*'(x, *(y, z)) -> *'(otimes(x, y), z)
*'(otimes(x'', y''), *(y0, z'')) -> *'(otimes(otimes(x'', y''), y0), z'')
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
...
→DP Problem 4
↳Instantiation Transformation
*'(otimes(x'', y''), *(y0, z'')) -> *'(otimes(otimes(x'', y''), y0), z'')
*(x, *(y, z)) -> *(otimes(x, y), z)
*(1, y) -> y
*(+(x, y), z) -> oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))
one new Dependency Pair is created:
*'(otimes(x'', y''), *(y0, z'')) -> *'(otimes(otimes(x'', y''), y0), z'')
*'(otimes(otimes(x'''', y''''), y''0), *(y0'', z'''')) -> *'(otimes(otimes(otimes(x'''', y''''), y''0), y0''), z'''')
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
...
→DP Problem 5
↳Polynomial Ordering
*'(otimes(otimes(x'''', y''''), y''0), *(y0'', z'''')) -> *'(otimes(otimes(otimes(x'''', y''''), y''0), y0''), z'''')
*(x, *(y, z)) -> *(otimes(x, y), z)
*(1, y) -> y
*(+(x, y), z) -> oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))
*'(otimes(otimes(x'''', y''''), y''0), *(y0'', z'''')) -> *'(otimes(otimes(otimes(x'''', y''''), y''0), y0''), z'''')
POL(*'(x1, x2)) = x2 POL(otimes(x1, x2)) = 0 POL(*(x1, x2)) = 1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
...
→DP Problem 6
↳Dependency Graph
*(x, *(y, z)) -> *(otimes(x, y), z)
*(1, y) -> y
*(+(x, y), z) -> oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))