Term Rewriting System R:
[a, x, k, d]
f(a, empty) -> g(a, empty)
f(a, cons(x, k)) -> f(cons(x, a), k)
g(empty, d) -> d
g(cons(x, k), d) -> g(k, cons(x, d))

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

F(a, empty) -> G(a, empty)
F(a, cons(x, k)) -> F(cons(x, a), k)
G(cons(x, k), d) -> G(k, cons(x, d))

Furthermore, R contains two SCCs.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)




The following remains to be proven:

Termination of R could not be shown.
Duration:
0:01 minutes