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