Term Rewriting System R:
[ls, a, x, k]
rev(ls) -> r1(ls, empty)
r1(empty, a) -> a
r1(cons(x, k), a) -> r1(k, cons(x, a))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
REV(ls) -> R1(ls, empty)
R1(cons(x, k), a) -> R1(k, cons(x, a))
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
The following remains to be proven:
Dependency Pair:
R1(cons(x, k), a) -> R1(k, cons(x, a))
Rules:
rev(ls) -> r1(ls, empty)
r1(empty, a) -> a
r1(cons(x, k), a) -> r1(k, cons(x, a))
Termination of R could not be shown.
Duration:
0:00 minutes