R
↳Dependency Pair Analysis
APP(f, app(s, x)) -> APP(f, x)
APP(g, app(app(cons, 0), y)) -> APP(g, y)
APP(h, app(app(cons, x), y)) -> APP(h, app(g, app(app(cons, x), y)))
APP(h, app(app(cons, x), y)) -> APP(g, app(app(cons, x), y))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
APP(f, app(s, x)) -> APP(f, x)
app(f, app(s, x)) -> app(f, x)
app(g, app(app(cons, 0), y)) -> app(g, y)
app(g, app(app(cons, app(s, x)), y)) -> app(s, x)
app(h, app(app(cons, x), y)) -> app(h, app(g, app(app(cons, x), y)))
innermost
APP(f, app(s, x)) -> APP(f, x)
POL(s) = 0 POL(APP(x1, x2)) = x1 + x2 POL(f) = 0 POL(app(x1, x2)) = 1 + x1 + x2
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> app(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
app(f, app(s, x)) -> app(f, x)
app(g, app(app(cons, 0), y)) -> app(g, y)
app(g, app(app(cons, app(s, x)), y)) -> app(s, x)
app(h, app(app(cons, x), y)) -> app(h, app(g, app(app(cons, x), y)))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳AFS
APP(g, app(app(cons, 0), y)) -> APP(g, y)
app(f, app(s, x)) -> app(f, x)
app(g, app(app(cons, 0), y)) -> app(g, y)
app(g, app(app(cons, app(s, x)), y)) -> app(s, x)
app(h, app(app(cons, x), y)) -> app(h, app(g, app(app(cons, x), y)))
innermost
APP(g, app(app(cons, 0), y)) -> APP(g, y)
POL(0) = 0 POL(g) = 0 POL(cons) = 1 POL(APP(x1, x2)) = 1 + x1 + x2 POL(app(x1, x2)) = x1 + x2
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> app(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳AFS
app(f, app(s, x)) -> app(f, x)
app(g, app(app(cons, 0), y)) -> app(g, y)
app(g, app(app(cons, app(s, x)), y)) -> app(s, x)
app(h, app(app(cons, x), y)) -> app(h, app(g, app(app(cons, x), y)))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
APP(h, app(app(cons, x), y)) -> APP(h, app(g, app(app(cons, x), y)))
app(f, app(s, x)) -> app(f, x)
app(g, app(app(cons, 0), y)) -> app(g, y)
app(g, app(app(cons, app(s, x)), y)) -> app(s, x)
app(h, app(app(cons, x), y)) -> app(h, app(g, app(app(cons, x), y)))
innermost
APP(h, app(app(cons, x), y)) -> APP(h, app(g, app(app(cons, x), y)))
app(f, app(s, x)) -> app(f, x)
app(g, app(app(cons, 0), y)) -> app(g, y)
app(g, app(app(cons, app(s, x)), y)) -> app(s, x)
app(h, app(app(cons, x), y)) -> app(h, app(g, app(app(cons, x), y)))
POL(g) = 0 POL(cons) = 1 POL(h) = 0 POL(s) = 0 POL(APP(x1, x2)) = x1 + x2 POL(f) = 0
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 6
↳Dependency Graph
app(f, app(s, x)) -> app(f, x)
app(g, app(app(cons, 0), y)) -> app(g, y)
app(g, app(app(cons, app(s, x)), y)) -> app(s, x)
app(h, app(app(cons, x), y)) -> app(h, app(g, app(app(cons, x), y)))
innermost