R
↳Dependency Pair Analysis
AP(ap(ap(g, x), y), ap(s, z)) -> AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) -> AP(ap(x, y), 0)
AP(ap(ap(g, x), y), ap(s, z)) -> AP(x, y)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
AP(ap(ap(g, x), y), ap(s, z)) -> AP(x, y)
AP(ap(ap(g, x), y), ap(s, z)) -> AP(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x) -> x
ap(ap(ap(g, x), y), ap(s, z)) -> ap(ap(ap(g, x), y), ap(ap(x, y), 0))
innermost
two new Dependency Pairs are created:
AP(ap(ap(g, x), y), ap(s, z)) -> AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, f), y'), ap(s, z)) -> AP(ap(ap(g, f), y'), ap(y', 0))
AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(ap(ap(ap(g, x''), y''), ap(ap(x'', y''), 0)), 0))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Forward Instantiation Transformation
AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(ap(ap(ap(g, x''), y''), ap(ap(x'', y''), 0)), 0))
AP(ap(ap(g, f), y'), ap(s, z)) -> AP(ap(ap(g, f), y'), ap(y', 0))
AP(ap(ap(g, x), y), ap(s, z)) -> AP(x, y)
ap(f, x) -> x
ap(ap(ap(g, x), y), ap(s, z)) -> ap(ap(ap(g, x), y), ap(ap(x, y), 0))
innermost
three new Dependency Pairs are created:
AP(ap(ap(g, x), y), ap(s, z)) -> AP(x, y)
AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, x''), y''), ap(s, z''))
AP(ap(ap(g, ap(ap(g, f), y''')), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, f), y'''), ap(s, z''))
AP(ap(ap(g, ap(ap(g, ap(ap(g, x''''), y'''')), ap(s, z''''))), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, ap(ap(g, x''''), y'''')), ap(s, z'''')), ap(s, z''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳FwdInst
...
→DP Problem 4
↳Remaining Obligation(s)
AP(ap(ap(g, f), y'), ap(s, z)) -> AP(ap(ap(g, f), y'), ap(y', 0))
ap(f, x) -> x
ap(ap(ap(g, x), y), ap(s, z)) -> ap(ap(ap(g, x), y), ap(ap(x, y), 0))
innermost
AP(ap(ap(g, ap(ap(g, ap(ap(g, x''''), y'''')), ap(s, z''''))), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, ap(ap(g, x''''), y'''')), ap(s, z'''')), ap(s, z''))
AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, x''), y''), ap(s, z''))
AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(ap(ap(ap(g, x''), y''), ap(ap(x'', y''), 0)), 0))
ap(f, x) -> x
ap(ap(ap(g, x), y), ap(s, z)) -> ap(ap(ap(g, x), y), ap(ap(x, y), 0))
innermost
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳FwdInst
...
→DP Problem 4
↳Remaining Obligation(s)
AP(ap(ap(g, f), y'), ap(s, z)) -> AP(ap(ap(g, f), y'), ap(y', 0))
ap(f, x) -> x
ap(ap(ap(g, x), y), ap(s, z)) -> ap(ap(ap(g, x), y), ap(ap(x, y), 0))
innermost
AP(ap(ap(g, ap(ap(g, ap(ap(g, x''''), y'''')), ap(s, z''''))), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, ap(ap(g, x''''), y'''')), ap(s, z'''')), ap(s, z''))
AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, x''), y''), ap(s, z''))
AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(s, z)) -> AP(ap(ap(g, ap(ap(g, x''), y'')), ap(s, z'')), ap(ap(ap(ap(g, x''), y''), ap(ap(x'', y''), 0)), 0))
ap(f, x) -> x
ap(ap(ap(g, x), y), ap(s, z)) -> ap(ap(ap(g, x), y), ap(ap(x, y), 0))
innermost