Term Rewriting System R:
[f, xs, x, y, ys]
ap(ap(map, f), xs) -> ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) -> null
ap(ap(ap(if, null), f), xs) -> ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) -> ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) -> true
ap(isEmpty, ap(ap(cons, x), xs)) -> null
ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AP(ap(map, f), xs) -> AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(map, f), xs) -> AP(ap(if, ap(isEmpty, xs)), f)
AP(ap(map, f), xs) -> AP(if, ap(isEmpty, xs))
AP(ap(map, f), xs) -> AP(isEmpty, xs)
AP(ap(ap(if, null), f), xs) -> AP(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
AP(ap(ap(if, null), f), xs) -> AP(cons, ap(f, ap(last, xs)))
AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(ap(if, null), f), xs) -> AP(last, xs)
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)
AP(ap(ap(if, null), f), xs) -> AP(if2, f)
AP(ap(if2, f), xs) -> AP(ap(map, f), ap(dropLast, xs))
AP(ap(if2, f), xs) -> AP(map, f)
AP(ap(if2, f), xs) -> AP(dropLast, xs)
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(last, ap(ap(cons, y), ys))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, ap(ap(cons, y), ys))

Furthermore, R contains three SCCs.


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




The following remains to be proven:


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




The following remains to be proven:


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




The following remains to be proven:

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