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
↳Remaining Obligation(s)
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))