Termination Proof using AProVE

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)))

Termination of R to be shown.

     ↳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 two SCCs.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(last, ap(ap(cons, y), ys))

Rules:

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)))
Dependency Pairs:
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, 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(ap(if2, f), xs) -> AP(dropLast, xs)
AP(ap(if2, f), xs) -> AP(ap(map, f), ap(dropLast, xs))
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)
AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(ap(if, null), f), xs) -> AP(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
AP(ap(map, f), xs) -> AP(ap(if, ap(isEmpty, xs)), f)
AP(ap(map, f), xs) -> AP(ap(ap(if, ap(isEmpty, xs)), f), xs)

Rules:

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)))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(last, ap(ap(cons, y), ys))

Rules:

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)))
Dependency Pairs:
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, 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(ap(if2, f), xs) -> AP(dropLast, xs)
AP(ap(if2, f), xs) -> AP(ap(map, f), ap(dropLast, xs))
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)
AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(ap(if, null), f), xs) -> AP(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
AP(ap(map, f), xs) -> AP(ap(if, ap(isEmpty, xs)), f)
AP(ap(map, f), xs) -> AP(ap(ap(if, ap(isEmpty, xs)), f), xs)

Rules:

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)))

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