R
↳Dependency Pair Analysis
REV(ls) -> R1(ls, empty)
R1(cons(x, k), a) -> R1(k, cons(x, a))
R
↳DPs
→DP Problem 1
↳Instantiation Transformation
R1(cons(x, k), a) -> R1(k, cons(x, a))
rev(ls) -> r1(ls, empty)
r1(empty, a) -> a
r1(cons(x, k), a) -> r1(k, cons(x, a))
one new Dependency Pair is created:
R1(cons(x, k), a) -> R1(k, cons(x, a))
R1(cons(x0, k''), cons(x'', a'')) -> R1(k'', cons(x0, cons(x'', a'')))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Remaining Obligation(s)
R1(cons(x0, k''), cons(x'', a'')) -> R1(k'', cons(x0, cons(x'', a'')))
rev(ls) -> r1(ls, empty)
r1(empty, a) -> a
r1(cons(x, k), a) -> r1(k, cons(x, a))