(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
sum#1(Nil) → 0
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0) → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0, x2) → 0
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0, x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0) → 0
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
sum#1(Cons(x2, x1)) →+ plus#2(x2, sum#1(x1))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [x1 / Cons(x2, x1)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)