The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

ap(ap(map, z0), z1) → ap(ap(ap(if, ap(isEmpty, z1)), z0), z1)
ap(ap(ap(if, true), z0), z1) → nil
ap(ap(ap(if, false), z0), z1) → ap(ap(cons, ap(z0, ap(last, z1))), ap(ap(map, z0), ap(dropLast, z1)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, z0), z1)) → false
ap(last, ap(ap(cons, z0), nil)) → z0
ap(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → ap(last, ap(ap(cons, z1), z2))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, z0), nil)) → nil
ap(dropLast, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → ap(ap(cons, z0), ap(dropLast, ap(ap(cons, z1), z2)))

Tuples:

AP(ap(map, z0), z1) → c(AP(ap(ap(if, ap(isEmpty, z1)), z0), z1), AP(ap(if, ap(isEmpty, z1)), z0), AP(if, ap(isEmpty, z1)), AP(isEmpty, z1))
AP(ap(ap(if, false), z0), z1) → c2(AP(ap(cons, ap(z0, ap(last, z1))), ap(ap(map, z0), ap(dropLast, z1))), AP(cons, ap(z0, ap(last, z1))), AP(z0, ap(last, z1)), AP(last, z1), AP(ap(map, z0), ap(dropLast, z1)), AP(map, z0), AP(dropLast, z1))
AP(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c6(AP(last, ap(ap(cons, z1), z2)), AP(ap(cons, z1), z2), AP(cons, z1))
AP(dropLast, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c9(AP(ap(cons, z0), ap(dropLast, ap(ap(cons, z1), z2))), AP(cons, z0), AP(dropLast, ap(ap(cons, z1), z2)), AP(ap(cons, z1), z2), AP(cons, z1))

S tuples:

AP(ap(map, z0), z1) → c(AP(ap(ap(if, ap(isEmpty, z1)), z0), z1), AP(ap(if, ap(isEmpty, z1)), z0), AP(if, ap(isEmpty, z1)), AP(isEmpty, z1))
AP(ap(ap(if, false), z0), z1) → c2(AP(ap(cons, ap(z0, ap(last, z1))), ap(ap(map, z0), ap(dropLast, z1))), AP(cons, ap(z0, ap(last, z1))), AP(z0, ap(last, z1)), AP(last, z1), AP(ap(map, z0), ap(dropLast, z1)), AP(map, z0), AP(dropLast, z1))
AP(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c6(AP(last, ap(ap(cons, z1), z2)), AP(ap(cons, z1), z2), AP(cons, z1))
AP(dropLast, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c9(AP(ap(cons, z0), ap(dropLast, ap(ap(cons, z1), z2))), AP(cons, z0), AP(dropLast, ap(ap(cons, z1), z2)), AP(ap(cons, z1), z2), AP(cons, z1))

K tuples:none
Defined Rule Symbols:

ap

Defined Pair Symbols:

AP

Compound Symbols:

c, c2, c6, c9

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

AP(ap(map, z0), z1) → c(AP(ap(ap(if, ap(isEmpty, z1)), z0), z1), AP(ap(if, ap(isEmpty, z1)), z0), AP(if, ap(isEmpty, z1)), AP(isEmpty, z1))
AP(ap(ap(if, false), z0), z1) → c2(AP(ap(cons, ap(z0, ap(last, z1))), ap(ap(map, z0), ap(dropLast, z1))), AP(cons, ap(z0, ap(last, z1))), AP(z0, ap(last, z1)), AP(last, z1), AP(ap(map, z0), ap(dropLast, z1)), AP(map, z0), AP(dropLast, z1))
AP(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c6(AP(last, ap(ap(cons, z1), z2)), AP(ap(cons, z1), z2), AP(cons, z1))
AP(dropLast, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c9(AP(ap(cons, z0), ap(dropLast, ap(ap(cons, z1), z2))), AP(cons, z0), AP(dropLast, ap(ap(cons, z1), z2)), AP(ap(cons, z1), z2), AP(cons, z1))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

ap(ap(map, z0), z1) → ap(ap(ap(if, ap(isEmpty, z1)), z0), z1)
ap(ap(ap(if, true), z0), z1) → nil
ap(ap(ap(if, false), z0), z1) → ap(ap(cons, ap(z0, ap(last, z1))), ap(ap(map, z0), ap(dropLast, z1)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, z0), z1)) → false
ap(last, ap(ap(cons, z0), nil)) → z0
ap(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → ap(last, ap(ap(cons, z1), z2))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, z0), nil)) → nil
ap(dropLast, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → ap(ap(cons, z0), ap(dropLast, ap(ap(cons, z1), z2)))

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

ap

Defined Pair Symbols:none

Compound Symbols:none

(5) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(6) BOUNDS(O(1), O(1))