WORST_CASE(Omega(n^2),?)
proof of input_tgpQ2I4WMD.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, INF).

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 4 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 320 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 32 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 6709 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 42 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 25 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 51 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 51 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 894 ms]
        (30) BEST
            (31) proven lower bound
                (32) LowerBoundPropagationProof [FINISHED, 0 ms]
                (33) BOUNDS(n^2, INF)
            (34) typed CpxTrs
                (35) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
                (36) typed CpxTrs
                (37) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
                (38) BOUNDS(1, INF)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, INF).


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

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   sum#1(Nil) -> 0
   sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
   map#2(Nil) -> Nil
   map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
   unfoldr#2(0) -> Nil
   unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
   mult#2(0, z0) -> 0
   mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
   plus#2(0, z0) -> z0
   plus#2(S(z0), z1) -> S(plus#2(z0, z1))
   main(0) -> 0
   main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))
Tuples:
   SUM#1(Nil) -> c
   SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
   MAP#2(Nil) -> c2
   MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
   MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
   UNFOLDR#2(0) -> c5
   UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
   MULT#2(0, z0) -> c7
   MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
   PLUS#2(0, z0) -> c9
   PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
   MAIN(0) -> c11
   MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
S tuples:
   SUM#1(Nil) -> c
   SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
   MAP#2(Nil) -> c2
   MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
   MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
   UNFOLDR#2(0) -> c5
   UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
   MULT#2(0, z0) -> c7
   MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
   PLUS#2(0, z0) -> c9
   PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
   MAIN(0) -> c11
   MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
K tuples:none
Defined Rule Symbols:   sum#1_1, map#2_1, unfoldr#2_1, mult#2_2, plus#2_2, main_1

Defined Pair Symbols:   SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1

Compound Symbols:   c, c1_2, c2, c3_1, c4_1, c5, c6_1, c7, c8_2, c9, c10_1, c11, c12_3


----------------------------------------

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF).


The TRS R consists of the following rules:

   SUM#1(Nil) -> c
   SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
   MAP#2(Nil) -> c2
   MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
   MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
   UNFOLDR#2(0) -> c5
   UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
   MULT#2(0, z0) -> c7
   MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
   PLUS#2(0, z0) -> c9
   PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
   MAIN(0) -> c11
   MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))

The (relative) TRS S consists of the following rules:

   sum#1(Nil) -> 0
   sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
   map#2(Nil) -> Nil
   map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
   unfoldr#2(0) -> Nil
   unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
   mult#2(0, z0) -> 0
   mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
   plus#2(0, z0) -> z0
   plus#2(S(z0), z1) -> S(plus#2(z0, z1))
   main(0) -> 0
   main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Rewrite Strategy: INNERMOST
----------------------------------------

(5) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF).


The TRS R consists of the following rules:

   SUM#1(Nil) -> c
   SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
   MAP#2(Nil) -> c2
   MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
   MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
   UNFOLDR#2(0') -> c5
   UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
   MULT#2(0', z0) -> c7
   MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
   PLUS#2(0', z0) -> c9
   PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
   MAIN(0') -> c11
   MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))

The (relative) TRS S consists of the following rules:

   sum#1(Nil) -> 0'
   sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
   map#2(Nil) -> Nil
   map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
   unfoldr#2(0') -> Nil
   unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
   mult#2(0', z0) -> 0'
   mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
   plus#2(0', z0) -> z0
   plus#2(S(z0), z1) -> S(plus#2(z0, z1))
   main(0') -> 0'
   main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
SUM#1, PLUS#2, sum#1, MAP#2, MULT#2, UNFOLDR#2, mult#2, map#2, unfoldr#2, plus#2

They will be analysed ascendingly in the following order:
PLUS#2 < SUM#1
sum#1 < SUM#1
PLUS#2 < MULT#2
plus#2 < sum#1
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2
plus#2 < mult#2

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
PLUS#2, SUM#1, sum#1, MAP#2, MULT#2, UNFOLDR#2, mult#2, map#2, unfoldr#2, plus#2

They will be analysed ascendingly in the following order:
PLUS#2 < SUM#1
sum#1 < SUM#1
PLUS#2 < MULT#2
plus#2 < sum#1
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2
plus#2 < mult#2

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)

Induction Base:
PLUS#2(gen_0':S11_13(0), gen_0':S11_13(b)) ->_R^Omega(1)
c9

Induction Step:
PLUS#2(gen_0':S11_13(+(n17_13, 1)), gen_0':S11_13(b)) ->_R^Omega(1)
c10(PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b))) ->_IH
c10(gen_c9:c1012_13(c18_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
PLUS#2, SUM#1, sum#1, MAP#2, MULT#2, UNFOLDR#2, mult#2, map#2, unfoldr#2, plus#2

They will be analysed ascendingly in the following order:
PLUS#2 < SUM#1
sum#1 < SUM#1
PLUS#2 < MULT#2
plus#2 < sum#1
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2
plus#2 < mult#2

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
UNFOLDR#2, SUM#1, sum#1, MAP#2, MULT#2, mult#2, map#2, unfoldr#2, plus#2

They will be analysed ascendingly in the following order:
sum#1 < SUM#1
plus#2 < sum#1
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2
plus#2 < mult#2

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)

Induction Base:
UNFOLDR#2(gen_0':S11_13(0)) ->_R^Omega(1)
c5

Induction Step:
UNFOLDR#2(gen_0':S11_13(+(n777_13, 1))) ->_R^Omega(1)
c6(UNFOLDR#2(gen_0':S11_13(n777_13))) ->_IH
c6(gen_c5:c615_13(c778_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
unfoldr#2, SUM#1, sum#1, MAP#2, MULT#2, mult#2, map#2, plus#2

They will be analysed ascendingly in the following order:
sum#1 < SUM#1
plus#2 < sum#1
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2
plus#2 < mult#2

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)

Induction Base:
unfoldr#2(gen_0':S11_13(+(1, 0)))

Induction Step:
unfoldr#2(gen_0':S11_13(+(1, +(n1305_13, 1)))) ->_R^Omega(0)
Cons(gen_0':S11_13(+(1, n1305_13)), unfoldr#2(gen_0':S11_13(+(1, n1305_13)))) ->_IH
Cons(gen_0':S11_13(+(1, n1305_13)), *16_13)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
plus#2, SUM#1, sum#1, MAP#2, MULT#2, mult#2, map#2

They will be analysed ascendingly in the following order:
sum#1 < SUM#1
plus#2 < sum#1
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2
plus#2 < mult#2

----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b)) -> gen_0':S11_13(+(n43562_13, b)), rt in Omega(0)

Induction Base:
plus#2(gen_0':S11_13(0), gen_0':S11_13(b)) ->_R^Omega(0)
gen_0':S11_13(b)

Induction Step:
plus#2(gen_0':S11_13(+(n43562_13, 1)), gen_0':S11_13(b)) ->_R^Omega(0)
S(plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b))) ->_IH
S(gen_0':S11_13(+(b, c43563_13)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)
plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b)) -> gen_0':S11_13(+(n43562_13, b)), rt in Omega(0)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
sum#1, SUM#1, MAP#2, MULT#2, mult#2, map#2

They will be analysed ascendingly in the following order:
sum#1 < SUM#1
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2

----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sum#1(gen_Nil:Cons10_13(n45346_13)) -> gen_0':S11_13(0), rt in Omega(0)

Induction Base:
sum#1(gen_Nil:Cons10_13(0)) ->_R^Omega(0)
0'

Induction Step:
sum#1(gen_Nil:Cons10_13(+(n45346_13, 1))) ->_R^Omega(0)
plus#2(0', sum#1(gen_Nil:Cons10_13(n45346_13))) ->_IH
plus#2(0', gen_0':S11_13(0)) ->_L^Omega(0)
gen_0':S11_13(+(0, 0))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)
plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b)) -> gen_0':S11_13(+(n43562_13, b)), rt in Omega(0)
sum#1(gen_Nil:Cons10_13(n45346_13)) -> gen_0':S11_13(0), rt in Omega(0)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
SUM#1, MAP#2, MULT#2, mult#2, map#2

They will be analysed ascendingly in the following order:
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2

----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SUM#1(gen_Nil:Cons10_13(n46100_13)) -> gen_c:c19_13(n46100_13), rt in Omega(1 + n46100_13)

Induction Base:
SUM#1(gen_Nil:Cons10_13(0)) ->_R^Omega(1)
c

Induction Step:
SUM#1(gen_Nil:Cons10_13(+(n46100_13, 1))) ->_R^Omega(1)
c1(PLUS#2(0', sum#1(gen_Nil:Cons10_13(n46100_13))), SUM#1(gen_Nil:Cons10_13(n46100_13))) ->_L^Omega(0)
c1(PLUS#2(0', gen_0':S11_13(0)), SUM#1(gen_Nil:Cons10_13(n46100_13))) ->_L^Omega(1)
c1(gen_c9:c1012_13(0), SUM#1(gen_Nil:Cons10_13(n46100_13))) ->_IH
c1(gen_c9:c1012_13(0), gen_c:c19_13(c46101_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)
plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b)) -> gen_0':S11_13(+(n43562_13, b)), rt in Omega(0)
sum#1(gen_Nil:Cons10_13(n45346_13)) -> gen_0':S11_13(0), rt in Omega(0)
SUM#1(gen_Nil:Cons10_13(n46100_13)) -> gen_c:c19_13(n46100_13), rt in Omega(1 + n46100_13)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
mult#2, MAP#2, MULT#2, map#2

They will be analysed ascendingly in the following order:
MULT#2 < MAP#2
mult#2 < MULT#2
mult#2 < map#2

----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
mult#2(gen_0':S11_13(n46858_13), gen_0':S11_13(b)) -> gen_0':S11_13(*(n46858_13, b)), rt in Omega(0)

Induction Base:
mult#2(gen_0':S11_13(0), gen_0':S11_13(b)) ->_R^Omega(0)
0'

Induction Step:
mult#2(gen_0':S11_13(+(n46858_13, 1)), gen_0':S11_13(b)) ->_R^Omega(0)
plus#2(gen_0':S11_13(b), mult#2(gen_0':S11_13(n46858_13), gen_0':S11_13(b))) ->_IH
plus#2(gen_0':S11_13(b), gen_0':S11_13(*(c46859_13, b))) ->_L^Omega(0)
gen_0':S11_13(+(b, *(n46858_13, b)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)
plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b)) -> gen_0':S11_13(+(n43562_13, b)), rt in Omega(0)
sum#1(gen_Nil:Cons10_13(n45346_13)) -> gen_0':S11_13(0), rt in Omega(0)
SUM#1(gen_Nil:Cons10_13(n46100_13)) -> gen_c:c19_13(n46100_13), rt in Omega(1 + n46100_13)
mult#2(gen_0':S11_13(n46858_13), gen_0':S11_13(b)) -> gen_0':S11_13(*(n46858_13, b)), rt in Omega(0)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
MULT#2, MAP#2, map#2

They will be analysed ascendingly in the following order:
MULT#2 < MAP#2

----------------------------------------

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MULT#2(gen_0':S11_13(n49745_13), gen_0':S11_13(b)) -> *16_13, rt in Omega(b*n49745_13 + n49745_13)

Induction Base:
MULT#2(gen_0':S11_13(0), gen_0':S11_13(b))

Induction Step:
MULT#2(gen_0':S11_13(+(n49745_13, 1)), gen_0':S11_13(b)) ->_R^Omega(1)
c8(PLUS#2(gen_0':S11_13(b), mult#2(gen_0':S11_13(n49745_13), gen_0':S11_13(b))), MULT#2(gen_0':S11_13(n49745_13), gen_0':S11_13(b))) ->_L^Omega(0)
c8(PLUS#2(gen_0':S11_13(b), gen_0':S11_13(*(n49745_13, b))), MULT#2(gen_0':S11_13(n49745_13), gen_0':S11_13(b))) ->_L^Omega(1 + b)
c8(gen_c9:c1012_13(b), MULT#2(gen_0':S11_13(n49745_13), gen_0':S11_13(*(n49745_13, b)))) ->_IH
c8(gen_c9:c1012_13(*(n49745_13, b)), *16_13)

We have rt in Omega(n^2) and sz in O(n). Thus, we have irc_R in Omega(n^2).
----------------------------------------

(30)
Complex Obligation (BEST)

----------------------------------------

(31)
Obligation:
Proved the lower bound n^2 for the following obligation:

Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)
plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b)) -> gen_0':S11_13(+(n43562_13, b)), rt in Omega(0)
sum#1(gen_Nil:Cons10_13(n45346_13)) -> gen_0':S11_13(0), rt in Omega(0)
SUM#1(gen_Nil:Cons10_13(n46100_13)) -> gen_c:c19_13(n46100_13), rt in Omega(1 + n46100_13)
mult#2(gen_0':S11_13(n46858_13), gen_0':S11_13(b)) -> gen_0':S11_13(*(n46858_13, b)), rt in Omega(0)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
MULT#2, MAP#2, map#2

They will be analysed ascendingly in the following order:
MULT#2 < MAP#2

----------------------------------------

(32) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(33)
BOUNDS(n^2, INF)

----------------------------------------

(34)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)
plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b)) -> gen_0':S11_13(+(n43562_13, b)), rt in Omega(0)
sum#1(gen_Nil:Cons10_13(n45346_13)) -> gen_0':S11_13(0), rt in Omega(0)
SUM#1(gen_Nil:Cons10_13(n46100_13)) -> gen_c:c19_13(n46100_13), rt in Omega(1 + n46100_13)
mult#2(gen_0':S11_13(n46858_13), gen_0':S11_13(b)) -> gen_0':S11_13(*(n46858_13, b)), rt in Omega(0)
MULT#2(gen_0':S11_13(n49745_13), gen_0':S11_13(b)) -> *16_13, rt in Omega(b*n49745_13 + n49745_13)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
MAP#2, map#2
----------------------------------------

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MAP#2(gen_Nil:Cons10_13(n96031_13)) -> gen_c2:c3:c413_13(n96031_13), rt in Omega(1 + n96031_13)

Induction Base:
MAP#2(gen_Nil:Cons10_13(0)) ->_R^Omega(1)
c2

Induction Step:
MAP#2(gen_Nil:Cons10_13(+(n96031_13, 1))) ->_R^Omega(1)
c4(MAP#2(gen_Nil:Cons10_13(n96031_13))) ->_IH
c4(gen_c2:c3:c413_13(c96032_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(36)
Obligation:
Innermost TRS:
Rules:
SUM#1(Nil) -> c
SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1))
MAP#2(Nil) -> c2
MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0))
MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1))
UNFOLDR#2(0') -> c5
UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
MULT#2(0', z0) -> c7
MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1))
PLUS#2(0', z0) -> c9
PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1))
MAIN(0') -> c11
MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0)))
sum#1(Nil) -> 0'
sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1))
map#2(Nil) -> Nil
map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1))
unfoldr#2(0') -> Nil
unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0))
mult#2(0', z0) -> 0'
mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1))
plus#2(0', z0) -> z0
plus#2(S(z0), z1) -> S(plus#2(z0, z1))
main(0') -> 0'
main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))

Types:
SUM#1 :: Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: 0':S -> Nil:Cons -> Nil:Cons
c1 :: c9:c10 -> c:c1 -> c:c1
PLUS#2 :: 0':S -> 0':S -> c9:c10
sum#1 :: Nil:Cons -> 0':S
MAP#2 :: Nil:Cons -> c2:c3:c4
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4
MULT#2 :: 0':S -> 0':S -> c7:c8
c4 :: c2:c3:c4 -> c2:c3:c4
UNFOLDR#2 :: 0':S -> c5:c6
0' :: 0':S
c5 :: c5:c6
S :: 0':S -> 0':S
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c9:c10 -> c7:c8 -> c7:c8
mult#2 :: 0':S -> 0':S -> 0':S
c9 :: c9:c10
c10 :: c9:c10 -> c9:c10
MAIN :: 0':S -> c11:c12
c11 :: c11:c12
c12 :: c:c1 -> c2:c3:c4 -> c5:c6 -> c11:c12
map#2 :: Nil:Cons -> Nil:Cons
unfoldr#2 :: 0':S -> Nil:Cons
plus#2 :: 0':S -> 0':S -> 0':S
main :: 0':S -> 0':S
hole_c:c11_13 :: c:c1
hole_Nil:Cons2_13 :: Nil:Cons
hole_0':S3_13 :: 0':S
hole_c9:c104_13 :: c9:c10
hole_c2:c3:c45_13 :: c2:c3:c4
hole_c7:c86_13 :: c7:c8
hole_c5:c67_13 :: c5:c6
hole_c11:c128_13 :: c11:c12
gen_c:c19_13 :: Nat -> c:c1
gen_Nil:Cons10_13 :: Nat -> Nil:Cons
gen_0':S11_13 :: Nat -> 0':S
gen_c9:c1012_13 :: Nat -> c9:c10
gen_c2:c3:c413_13 :: Nat -> c2:c3:c4
gen_c7:c814_13 :: Nat -> c7:c8
gen_c5:c615_13 :: Nat -> c5:c6


Lemmas:
PLUS#2(gen_0':S11_13(n17_13), gen_0':S11_13(b)) -> gen_c9:c1012_13(n17_13), rt in Omega(1 + n17_13)
UNFOLDR#2(gen_0':S11_13(n777_13)) -> gen_c5:c615_13(n777_13), rt in Omega(1 + n777_13)
unfoldr#2(gen_0':S11_13(+(1, n1305_13))) -> *16_13, rt in Omega(0)
plus#2(gen_0':S11_13(n43562_13), gen_0':S11_13(b)) -> gen_0':S11_13(+(n43562_13, b)), rt in Omega(0)
sum#1(gen_Nil:Cons10_13(n45346_13)) -> gen_0':S11_13(0), rt in Omega(0)
SUM#1(gen_Nil:Cons10_13(n46100_13)) -> gen_c:c19_13(n46100_13), rt in Omega(1 + n46100_13)
mult#2(gen_0':S11_13(n46858_13), gen_0':S11_13(b)) -> gen_0':S11_13(*(n46858_13, b)), rt in Omega(0)
MULT#2(gen_0':S11_13(n49745_13), gen_0':S11_13(b)) -> *16_13, rt in Omega(b*n49745_13 + n49745_13)
MAP#2(gen_Nil:Cons10_13(n96031_13)) -> gen_c2:c3:c413_13(n96031_13), rt in Omega(1 + n96031_13)


Generator Equations:
gen_c:c19_13(0) <=> c
gen_c:c19_13(+(x, 1)) <=> c1(c9, gen_c:c19_13(x))
gen_Nil:Cons10_13(0) <=> Nil
gen_Nil:Cons10_13(+(x, 1)) <=> Cons(0', gen_Nil:Cons10_13(x))
gen_0':S11_13(0) <=> 0'
gen_0':S11_13(+(x, 1)) <=> S(gen_0':S11_13(x))
gen_c9:c1012_13(0) <=> c9
gen_c9:c1012_13(+(x, 1)) <=> c10(gen_c9:c1012_13(x))
gen_c2:c3:c413_13(0) <=> c2
gen_c2:c3:c413_13(+(x, 1)) <=> c4(gen_c2:c3:c413_13(x))
gen_c7:c814_13(0) <=> c7
gen_c7:c814_13(+(x, 1)) <=> c8(c9, gen_c7:c814_13(x))
gen_c5:c615_13(0) <=> c5
gen_c5:c615_13(+(x, 1)) <=> c6(gen_c5:c615_13(x))


The following defined symbols remain to be analysed:
map#2
----------------------------------------

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
map#2(gen_Nil:Cons10_13(n96778_13)) -> gen_Nil:Cons10_13(n96778_13), rt in Omega(0)

Induction Base:
map#2(gen_Nil:Cons10_13(0)) ->_R^Omega(0)
Nil

Induction Step:
map#2(gen_Nil:Cons10_13(+(n96778_13, 1))) ->_R^Omega(0)
Cons(mult#2(0', 0'), map#2(gen_Nil:Cons10_13(n96778_13))) ->_L^Omega(0)
Cons(gen_0':S11_13(*(0, 0)), map#2(gen_Nil:Cons10_13(n96778_13))) ->_IH
Cons(gen_0':S11_13(0), gen_Nil:Cons10_13(c96779_13))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(38)
BOUNDS(1, INF)