R
↳Dependency Pair Analysis
APP(f, app(f, x)) -> APP(g, app(f, x))
APP(g, app(g, x)) -> APP(f, x)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
APP(g, app(g, x)) -> APP(f, x)
APP(f, app(f, x)) -> APP(g, app(f, x))
app(f, app(f, x)) -> app(g, app(f, x))
app(g, app(g, x)) -> app(f, x)
one new Dependency Pair is created:
APP(f, app(f, x)) -> APP(g, app(f, x))
APP(f, app(f, app(f, x''))) -> APP(g, app(g, app(f, x'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Argument Filtering and Ordering
APP(f, app(f, app(f, x''))) -> APP(g, app(g, app(f, x'')))
APP(g, app(g, x)) -> APP(f, x)
app(f, app(f, x)) -> app(g, app(f, x))
app(g, app(g, x)) -> app(f, x)
APP(g, app(g, x)) -> APP(f, x)
app(f, app(f, x)) -> app(g, app(f, x))
app(g, app(g, x)) -> app(f, x)
APP(x1, x2) -> x2
app(x1, x2) -> app(x2)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳AFS
...
→DP Problem 3
↳Dependency Graph
APP(f, app(f, app(f, x''))) -> APP(g, app(g, app(f, x'')))
app(f, app(f, x)) -> app(g, app(f, x))
app(g, app(g, x)) -> app(f, x)