(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) → 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)))
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) → null
ap(ap(ap(if, null), z0), z1) → ap(ap(cons, ap(z0, ap(last, z1))), ap(ap(if2, z0), z1))
ap(ap(if2, z0), z1) → ap(ap(map, z0), ap(dropLast, z1))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, z0), z1)) → null
ap(last, ap(ap(cons, z0), null)) → z0
ap(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → ap(last, ap(ap(cons, z1), z2))
ap(dropLast, ap(ap(cons, z0), null)) → null
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, null), z0), z1) → c2(AP(ap(cons, ap(z0, ap(last, z1))), ap(ap(if2, z0), z1)), AP(cons, ap(z0, ap(last, z1))), AP(z0, ap(last, z1)), AP(last, z1), AP(ap(if2, z0), z1), AP(if2, z0))
AP(ap(if2, z0), z1) → c3(AP(ap(map, z0), ap(dropLast, z1)), AP(map, z0), AP(dropLast, z1))
AP(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c7(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, null), z0), z1) → c2(AP(ap(cons, ap(z0, ap(last, z1))), ap(ap(if2, z0), z1)), AP(cons, ap(z0, ap(last, z1))), AP(z0, ap(last, z1)), AP(last, z1), AP(ap(if2, z0), z1), AP(if2, z0))
AP(ap(if2, z0), z1) → c3(AP(ap(map, z0), ap(dropLast, z1)), AP(map, z0), AP(dropLast, z1))
AP(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c7(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, c3, c7, 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, null), z0), z1) → c2(AP(ap(cons, ap(z0, ap(last, z1))), ap(ap(if2, z0), z1)), AP(cons, ap(z0, ap(last, z1))), AP(z0, ap(last, z1)), AP(last, z1), AP(ap(if2, z0), z1), AP(if2, z0))
AP(ap(if2, z0), z1) → c3(AP(ap(map, z0), ap(dropLast, z1)), AP(map, z0), AP(dropLast, z1))
AP(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → c7(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) → null
ap(ap(ap(if, null), z0), z1) → ap(ap(cons, ap(z0, ap(last, z1))), ap(ap(if2, z0), z1))
ap(ap(if2, z0), z1) → ap(ap(map, z0), ap(dropLast, z1))
ap(isEmpty, null) → true
ap(isEmpty, ap(ap(cons, z0), z1)) → null
ap(last, ap(ap(cons, z0), null)) → z0
ap(last, ap(ap(cons, z0), ap(ap(cons, z1), z2))) → ap(last, ap(ap(cons, z1), z2))
ap(dropLast, ap(ap(cons, z0), null)) → null
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))