R
↳Dependency Pair Analysis
AP(ap(ff, x), x) -> AP(ap(x, ap(ff, x)), ap(ap(cons, x), nil))
AP(ap(ff, x), x) -> AP(x, ap(ff, x))
AP(ap(ff, x), x) -> AP(ap(cons, x), nil)
AP(ap(ff, x), x) -> AP(cons, x)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
AP(ap(ff, x), x) -> AP(ap(cons, x), nil)
AP(ap(ff, x), x) -> AP(ap(x, ap(ff, x)), ap(ap(cons, x), nil))
ap(ap(ff, x), x) -> ap(ap(x, ap(ff, x)), ap(ap(cons, x), nil))
innermost
no new Dependency Pairs are created.
AP(ap(ff, x), x) -> AP(ap(x, ap(ff, x)), ap(ap(cons, x), nil))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
AP(ap(ff, x), x) -> AP(ap(cons, x), nil)
ap(ap(ff, x), x) -> ap(ap(x, ap(ff, x)), ap(ap(cons, x), nil))
innermost
no new Dependency Pairs are created.
AP(ap(ff, x), x) -> AP(ap(cons, x), nil)