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

Strategy:

innermost

• Dependency Pair:

AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, 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)))

Strategy:

innermost

• Dependency Pairs:

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

Strategy:

innermost

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

Strategy:

innermost

• Dependency Pair:

AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, 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)))

Strategy:

innermost

• Dependency Pairs:

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

Strategy:

innermost

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

Strategy:

innermost

• Dependency Pair:

AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, 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)))

Strategy:

innermost

• Dependency Pairs:

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

Strategy:

innermost

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