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
↳Nar
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)))
APP(f, app(s, x)) -> APP(f, x)
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
↳Nar
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)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳Nar
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)))
APP(g, app(app(cons, 0), y)) -> APP(g, y)
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
↳Nar
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)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Narrowing Transformation
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)))
two new Dependency Pairs are created:
APP(h, app(app(cons, x), y)) -> APP(h, app(g, app(app(cons, x), y)))
APP(h, app(app(cons, 0), y'')) -> APP(h, app(g, y''))
APP(h, app(app(cons, app(s, x'')), y'')) -> APP(h, app(s, x''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Narrowing Transformation
APP(h, app(app(cons, app(s, x'')), y'')) -> APP(h, app(s, x''))
APP(h, app(app(cons, 0), y'')) -> APP(h, 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)))
two new Dependency Pairs are created:
APP(h, app(app(cons, 0), y'')) -> APP(h, app(g, y''))
APP(h, app(app(cons, 0), app(app(cons, 0), y'))) -> APP(h, app(g, y'))
APP(h, app(app(cons, 0), app(app(cons, app(s, x')), y'))) -> APP(h, app(s, x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
APP(h, app(app(cons, 0), app(app(cons, app(s, x')), y'))) -> APP(h, app(s, x'))
APP(h, app(app(cons, 0), app(app(cons, 0), y'))) -> APP(h, app(g, y'))
APP(h, app(app(cons, app(s, x'')), y'')) -> APP(h, app(s, 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)))
no new Dependency Pairs are created.
APP(h, app(app(cons, app(s, x'')), y'')) -> APP(h, app(s, x''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
APP(h, app(app(cons, 0), app(app(cons, 0), y'))) -> APP(h, app(g, y'))
APP(h, app(app(cons, 0), app(app(cons, app(s, x')), y'))) -> APP(h, app(s, 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)))
no new Dependency Pairs are created.
APP(h, app(app(cons, 0), app(app(cons, app(s, x')), y'))) -> APP(h, app(s, x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 9
↳Narrowing Transformation
APP(h, app(app(cons, 0), app(app(cons, 0), y'))) -> APP(h, 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)))
two new Dependency Pairs are created:
APP(h, app(app(cons, 0), app(app(cons, 0), y'))) -> APP(h, app(g, y'))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'')))) -> APP(h, app(g, y''))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'')))) -> APP(h, app(s, x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 10
↳Narrowing Transformation
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'')))) -> APP(h, app(s, x'))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'')))) -> APP(h, 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)))
two new Dependency Pairs are created:
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'')))) -> APP(h, app(g, y''))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'))))) -> APP(h, app(g, y'))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'))))) -> APP(h, app(s, x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 11
↳Narrowing Transformation
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'))))) -> APP(h, app(s, x'))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'))))) -> APP(h, app(g, y'))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'')))) -> APP(h, app(s, 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)))
no new Dependency Pairs are created.
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'')))) -> APP(h, app(s, x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 12
↳Narrowing Transformation
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'))))) -> APP(h, app(g, y'))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'))))) -> APP(h, app(s, 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)))
two new Dependency Pairs are created:
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'))))) -> APP(h, app(g, y'))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'')))))) -> APP(h, app(g, y''))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'')))))) -> APP(h, app(s, x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 13
↳Narrowing Transformation
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'')))))) -> APP(h, app(s, x'))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'')))))) -> APP(h, app(g, y''))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'))))) -> APP(h, app(s, 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)))
no new Dependency Pairs are created.
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'))))) -> APP(h, app(s, x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 14
↳Narrowing Transformation
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'')))))) -> APP(h, app(g, y''))
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'')))))) -> APP(h, app(s, 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)))
no new Dependency Pairs are created.
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, app(s, x')), y'')))))) -> APP(h, app(s, x'))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 15
↳Remaining Obligation(s)
APP(h, app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), app(app(cons, 0), y'')))))) -> APP(h, 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)))