R
↳Dependency Pair Analysis
APP(g, app(g, x)) -> APP(g, app(h, app(g, x)))
APP(g, app(g, x)) -> APP(h, app(g, x))
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
APP(h, app(h, x)) -> APP(app(f, app(h, x)), x)
APP(h, app(h, x)) -> APP(f, app(h, x))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
innermost
APP(h, app(h, x)) -> APP(h, app(app(f, app(h, x)), x))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
h > f
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳AFS
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
APP(g, app(g, x)) -> APP(g, app(h, app(g, x)))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
innermost
APP(g, app(g, x)) -> APP(g, app(h, app(g, x)))
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
g > h
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 4
↳Dependency Graph
app(g, app(h, app(g, x))) -> app(g, x)
app(g, app(g, x)) -> app(g, app(h, app(g, x)))
app(h, app(h, x)) -> app(h, app(app(f, app(h, x)), x))
innermost