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


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, 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), 13 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 268 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), 43.8 s]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 232 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 14 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 622 ms]
        (24) typed CpxTrs


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

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


The TRS R consists of the following rules:

   power(x', Cons(x, xs)) -> mult(x', power(x', xs))
   mult(x', Cons(x, xs)) -> add0(x', mult(x', xs))
   add0(x', Cons(x, xs)) -> Cons(Cons(Nil, Nil), add0(x', xs))
   power(x, Nil) -> Cons(Nil, Nil)
   mult(x, Nil) -> Nil
   add0(x, Nil) -> x
   goal(x, y) -> power(x, y)

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:
   power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
   power(z0, Nil) -> Cons(Nil, Nil)
   mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
   mult(z0, Nil) -> Nil
   add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
   add0(z0, Nil) -> z0
   goal(z0, z1) -> power(z0, z1)
Tuples:
   POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
   POWER(z0, Nil) -> c1
   MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
   MULT(z0, Nil) -> c3
   ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
   ADD0(z0, Nil) -> c5
   GOAL(z0, z1) -> c6(POWER(z0, z1))
S tuples:
   POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
   POWER(z0, Nil) -> c1
   MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
   MULT(z0, Nil) -> c3
   ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
   ADD0(z0, Nil) -> c5
   GOAL(z0, z1) -> c6(POWER(z0, z1))
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, goal_2

Defined Pair Symbols:   POWER_2, MULT_2, ADD0_2, GOAL_2

Compound Symbols:   c_2, c1, c2_2, c3, c4_1, c5, c6_1


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

(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^1, INF).


The TRS R consists of the following rules:

   POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
   POWER(z0, Nil) -> c1
   MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
   MULT(z0, Nil) -> c3
   ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
   ADD0(z0, Nil) -> c5
   GOAL(z0, z1) -> c6(POWER(z0, z1))

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

   power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
   power(z0, Nil) -> Cons(Nil, Nil)
   mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
   mult(z0, Nil) -> Nil
   add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
   add0(z0, Nil) -> z0
   goal(z0, z1) -> power(z0, z1)

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^1, INF).


The TRS R consists of the following rules:

   POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
   POWER(z0, Nil) -> c1
   MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
   MULT(z0, Nil) -> c3
   ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
   ADD0(z0, Nil) -> c5
   GOAL(z0, z1) -> c6(POWER(z0, z1))

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

   power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
   power(z0, Nil) -> Cons(Nil, Nil)
   mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
   mult(z0, Nil) -> Nil
   add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
   add0(z0, Nil) -> z0
   goal(z0, z1) -> power(z0, z1)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
POWER(z0, Nil) -> c1
MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
MULT(z0, Nil) -> c3
ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
ADD0(z0, Nil) -> c5
GOAL(z0, z1) -> c6(POWER(z0, z1))
power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
power(z0, Nil) -> Cons(Nil, Nil)
mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
mult(z0, Nil) -> Nil
add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
add0(z0, Nil) -> z0
goal(z0, z1) -> power(z0, z1)

Types:
POWER :: Cons:Nil -> Cons:Nil -> c:c1
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c :: c2:c3 -> c:c1 -> c:c1
MULT :: Cons:Nil -> Cons:Nil -> c2:c3
power :: Cons:Nil -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c1 :: c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
ADD0 :: Cons:Nil -> Cons:Nil -> c4:c5
mult :: Cons:Nil -> Cons:Nil -> Cons:Nil
c3 :: c2:c3
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c6
c6 :: c:c1 -> c6
add0 :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c:c11_7 :: c:c1
hole_Cons:Nil2_7 :: Cons:Nil
hole_c2:c33_7 :: c2:c3
hole_c4:c54_7 :: c4:c5
hole_c65_7 :: c6
gen_c:c16_7 :: Nat -> c:c1
gen_Cons:Nil7_7 :: Nat -> Cons:Nil
gen_c2:c38_7 :: Nat -> c2:c3
gen_c4:c59_7 :: Nat -> c4:c5

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
POWER, MULT, power, ADD0, mult, add0

They will be analysed ascendingly in the following order:
MULT < POWER
power < POWER
ADD0 < MULT
mult < MULT
mult < power
add0 < mult

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

(10)
Obligation:
Innermost TRS:
Rules:
POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
POWER(z0, Nil) -> c1
MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
MULT(z0, Nil) -> c3
ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
ADD0(z0, Nil) -> c5
GOAL(z0, z1) -> c6(POWER(z0, z1))
power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
power(z0, Nil) -> Cons(Nil, Nil)
mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
mult(z0, Nil) -> Nil
add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
add0(z0, Nil) -> z0
goal(z0, z1) -> power(z0, z1)

Types:
POWER :: Cons:Nil -> Cons:Nil -> c:c1
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c :: c2:c3 -> c:c1 -> c:c1
MULT :: Cons:Nil -> Cons:Nil -> c2:c3
power :: Cons:Nil -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c1 :: c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
ADD0 :: Cons:Nil -> Cons:Nil -> c4:c5
mult :: Cons:Nil -> Cons:Nil -> Cons:Nil
c3 :: c2:c3
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c6
c6 :: c:c1 -> c6
add0 :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c:c11_7 :: c:c1
hole_Cons:Nil2_7 :: Cons:Nil
hole_c2:c33_7 :: c2:c3
hole_c4:c54_7 :: c4:c5
hole_c65_7 :: c6
gen_c:c16_7 :: Nat -> c:c1
gen_Cons:Nil7_7 :: Nat -> Cons:Nil
gen_c2:c38_7 :: Nat -> c2:c3
gen_c4:c59_7 :: Nat -> c4:c5


Generator Equations:
gen_c:c16_7(0) <=> c1
gen_c:c16_7(+(x, 1)) <=> c(c3, gen_c:c16_7(x))
gen_Cons:Nil7_7(0) <=> Nil
gen_Cons:Nil7_7(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil7_7(x))
gen_c2:c38_7(0) <=> c3
gen_c2:c38_7(+(x, 1)) <=> c2(c5, gen_c2:c38_7(x))
gen_c4:c59_7(0) <=> c5
gen_c4:c59_7(+(x, 1)) <=> c4(gen_c4:c59_7(x))


The following defined symbols remain to be analysed:
ADD0, POWER, MULT, power, mult, add0

They will be analysed ascendingly in the following order:
MULT < POWER
power < POWER
ADD0 < MULT
mult < MULT
mult < power
add0 < mult

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(n11_7)) -> gen_c4:c59_7(n11_7), rt in Omega(1 + n11_7)

Induction Base:
ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(0)) ->_R^Omega(1)
c5

Induction Step:
ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(n11_7, 1))) ->_R^Omega(1)
c4(ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(n11_7))) ->_IH
c4(gen_c4:c59_7(c12_7))

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:
POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
POWER(z0, Nil) -> c1
MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
MULT(z0, Nil) -> c3
ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
ADD0(z0, Nil) -> c5
GOAL(z0, z1) -> c6(POWER(z0, z1))
power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
power(z0, Nil) -> Cons(Nil, Nil)
mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
mult(z0, Nil) -> Nil
add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
add0(z0, Nil) -> z0
goal(z0, z1) -> power(z0, z1)

Types:
POWER :: Cons:Nil -> Cons:Nil -> c:c1
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c :: c2:c3 -> c:c1 -> c:c1
MULT :: Cons:Nil -> Cons:Nil -> c2:c3
power :: Cons:Nil -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c1 :: c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
ADD0 :: Cons:Nil -> Cons:Nil -> c4:c5
mult :: Cons:Nil -> Cons:Nil -> Cons:Nil
c3 :: c2:c3
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c6
c6 :: c:c1 -> c6
add0 :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c:c11_7 :: c:c1
hole_Cons:Nil2_7 :: Cons:Nil
hole_c2:c33_7 :: c2:c3
hole_c4:c54_7 :: c4:c5
hole_c65_7 :: c6
gen_c:c16_7 :: Nat -> c:c1
gen_Cons:Nil7_7 :: Nat -> Cons:Nil
gen_c2:c38_7 :: Nat -> c2:c3
gen_c4:c59_7 :: Nat -> c4:c5


Generator Equations:
gen_c:c16_7(0) <=> c1
gen_c:c16_7(+(x, 1)) <=> c(c3, gen_c:c16_7(x))
gen_Cons:Nil7_7(0) <=> Nil
gen_Cons:Nil7_7(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil7_7(x))
gen_c2:c38_7(0) <=> c3
gen_c2:c38_7(+(x, 1)) <=> c2(c5, gen_c2:c38_7(x))
gen_c4:c59_7(0) <=> c5
gen_c4:c59_7(+(x, 1)) <=> c4(gen_c4:c59_7(x))


The following defined symbols remain to be analysed:
ADD0, POWER, MULT, power, mult, add0

They will be analysed ascendingly in the following order:
MULT < POWER
power < POWER
ADD0 < MULT
mult < MULT
mult < power
add0 < mult

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
POWER(z0, Nil) -> c1
MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
MULT(z0, Nil) -> c3
ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
ADD0(z0, Nil) -> c5
GOAL(z0, z1) -> c6(POWER(z0, z1))
power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
power(z0, Nil) -> Cons(Nil, Nil)
mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
mult(z0, Nil) -> Nil
add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
add0(z0, Nil) -> z0
goal(z0, z1) -> power(z0, z1)

Types:
POWER :: Cons:Nil -> Cons:Nil -> c:c1
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c :: c2:c3 -> c:c1 -> c:c1
MULT :: Cons:Nil -> Cons:Nil -> c2:c3
power :: Cons:Nil -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c1 :: c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
ADD0 :: Cons:Nil -> Cons:Nil -> c4:c5
mult :: Cons:Nil -> Cons:Nil -> Cons:Nil
c3 :: c2:c3
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c6
c6 :: c:c1 -> c6
add0 :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c:c11_7 :: c:c1
hole_Cons:Nil2_7 :: Cons:Nil
hole_c2:c33_7 :: c2:c3
hole_c4:c54_7 :: c4:c5
hole_c65_7 :: c6
gen_c:c16_7 :: Nat -> c:c1
gen_Cons:Nil7_7 :: Nat -> Cons:Nil
gen_c2:c38_7 :: Nat -> c2:c3
gen_c4:c59_7 :: Nat -> c4:c5


Lemmas:
ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(n11_7)) -> gen_c4:c59_7(n11_7), rt in Omega(1 + n11_7)


Generator Equations:
gen_c:c16_7(0) <=> c1
gen_c:c16_7(+(x, 1)) <=> c(c3, gen_c:c16_7(x))
gen_Cons:Nil7_7(0) <=> Nil
gen_Cons:Nil7_7(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil7_7(x))
gen_c2:c38_7(0) <=> c3
gen_c2:c38_7(+(x, 1)) <=> c2(c5, gen_c2:c38_7(x))
gen_c4:c59_7(0) <=> c5
gen_c4:c59_7(+(x, 1)) <=> c4(gen_c4:c59_7(x))


The following defined symbols remain to be analysed:
add0, POWER, MULT, power, mult

They will be analysed ascendingly in the following order:
MULT < POWER
power < POWER
mult < MULT
mult < power
add0 < mult

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
add0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(1, n574_7))) -> *10_7, rt in Omega(0)

Induction Base:
add0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(1, 0)))

Induction Step:
add0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(1, +(n574_7, 1)))) ->_R^Omega(0)
Cons(Cons(Nil, Nil), add0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(1, n574_7)))) ->_IH
Cons(Cons(Nil, Nil), *10_7)

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

(18)
Obligation:
Innermost TRS:
Rules:
POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
POWER(z0, Nil) -> c1
MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
MULT(z0, Nil) -> c3
ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
ADD0(z0, Nil) -> c5
GOAL(z0, z1) -> c6(POWER(z0, z1))
power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
power(z0, Nil) -> Cons(Nil, Nil)
mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
mult(z0, Nil) -> Nil
add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
add0(z0, Nil) -> z0
goal(z0, z1) -> power(z0, z1)

Types:
POWER :: Cons:Nil -> Cons:Nil -> c:c1
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c :: c2:c3 -> c:c1 -> c:c1
MULT :: Cons:Nil -> Cons:Nil -> c2:c3
power :: Cons:Nil -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c1 :: c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
ADD0 :: Cons:Nil -> Cons:Nil -> c4:c5
mult :: Cons:Nil -> Cons:Nil -> Cons:Nil
c3 :: c2:c3
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c6
c6 :: c:c1 -> c6
add0 :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c:c11_7 :: c:c1
hole_Cons:Nil2_7 :: Cons:Nil
hole_c2:c33_7 :: c2:c3
hole_c4:c54_7 :: c4:c5
hole_c65_7 :: c6
gen_c:c16_7 :: Nat -> c:c1
gen_Cons:Nil7_7 :: Nat -> Cons:Nil
gen_c2:c38_7 :: Nat -> c2:c3
gen_c4:c59_7 :: Nat -> c4:c5


Lemmas:
ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(n11_7)) -> gen_c4:c59_7(n11_7), rt in Omega(1 + n11_7)
add0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(1, n574_7))) -> *10_7, rt in Omega(0)


Generator Equations:
gen_c:c16_7(0) <=> c1
gen_c:c16_7(+(x, 1)) <=> c(c3, gen_c:c16_7(x))
gen_Cons:Nil7_7(0) <=> Nil
gen_Cons:Nil7_7(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil7_7(x))
gen_c2:c38_7(0) <=> c3
gen_c2:c38_7(+(x, 1)) <=> c2(c5, gen_c2:c38_7(x))
gen_c4:c59_7(0) <=> c5
gen_c4:c59_7(+(x, 1)) <=> c4(gen_c4:c59_7(x))


The following defined symbols remain to be analysed:
mult, POWER, MULT, power

They will be analysed ascendingly in the following order:
MULT < POWER
power < POWER
mult < MULT
mult < power

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
mult(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1659106_7)) -> gen_Cons:Nil7_7(0), rt in Omega(0)

Induction Base:
mult(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(0)) ->_R^Omega(0)
Nil

Induction Step:
mult(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(+(n1659106_7, 1))) ->_R^Omega(0)
add0(gen_Cons:Nil7_7(0), mult(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1659106_7))) ->_IH
add0(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(0)) ->_R^Omega(0)
gen_Cons:Nil7_7(0)

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:
POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
POWER(z0, Nil) -> c1
MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
MULT(z0, Nil) -> c3
ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
ADD0(z0, Nil) -> c5
GOAL(z0, z1) -> c6(POWER(z0, z1))
power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
power(z0, Nil) -> Cons(Nil, Nil)
mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
mult(z0, Nil) -> Nil
add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
add0(z0, Nil) -> z0
goal(z0, z1) -> power(z0, z1)

Types:
POWER :: Cons:Nil -> Cons:Nil -> c:c1
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c :: c2:c3 -> c:c1 -> c:c1
MULT :: Cons:Nil -> Cons:Nil -> c2:c3
power :: Cons:Nil -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c1 :: c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
ADD0 :: Cons:Nil -> Cons:Nil -> c4:c5
mult :: Cons:Nil -> Cons:Nil -> Cons:Nil
c3 :: c2:c3
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c6
c6 :: c:c1 -> c6
add0 :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c:c11_7 :: c:c1
hole_Cons:Nil2_7 :: Cons:Nil
hole_c2:c33_7 :: c2:c3
hole_c4:c54_7 :: c4:c5
hole_c65_7 :: c6
gen_c:c16_7 :: Nat -> c:c1
gen_Cons:Nil7_7 :: Nat -> Cons:Nil
gen_c2:c38_7 :: Nat -> c2:c3
gen_c4:c59_7 :: Nat -> c4:c5


Lemmas:
ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(n11_7)) -> gen_c4:c59_7(n11_7), rt in Omega(1 + n11_7)
add0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(1, n574_7))) -> *10_7, rt in Omega(0)
mult(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1659106_7)) -> gen_Cons:Nil7_7(0), rt in Omega(0)


Generator Equations:
gen_c:c16_7(0) <=> c1
gen_c:c16_7(+(x, 1)) <=> c(c3, gen_c:c16_7(x))
gen_Cons:Nil7_7(0) <=> Nil
gen_Cons:Nil7_7(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil7_7(x))
gen_c2:c38_7(0) <=> c3
gen_c2:c38_7(+(x, 1)) <=> c2(c5, gen_c2:c38_7(x))
gen_c4:c59_7(0) <=> c5
gen_c4:c59_7(+(x, 1)) <=> c4(gen_c4:c59_7(x))


The following defined symbols remain to be analysed:
MULT, POWER, power

They will be analysed ascendingly in the following order:
MULT < POWER
power < POWER

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MULT(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1665969_7)) -> gen_c2:c38_7(n1665969_7), rt in Omega(1 + n1665969_7)

Induction Base:
MULT(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(0)) ->_R^Omega(1)
c3

Induction Step:
MULT(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(+(n1665969_7, 1))) ->_R^Omega(1)
c2(ADD0(gen_Cons:Nil7_7(0), mult(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1665969_7))), MULT(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1665969_7))) ->_L^Omega(0)
c2(ADD0(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(0)), MULT(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1665969_7))) ->_L^Omega(1)
c2(gen_c4:c59_7(0), MULT(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1665969_7))) ->_IH
c2(gen_c4:c59_7(0), gen_c2:c38_7(c1665970_7))

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

(22)
Obligation:
Innermost TRS:
Rules:
POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
POWER(z0, Nil) -> c1
MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
MULT(z0, Nil) -> c3
ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
ADD0(z0, Nil) -> c5
GOAL(z0, z1) -> c6(POWER(z0, z1))
power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
power(z0, Nil) -> Cons(Nil, Nil)
mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
mult(z0, Nil) -> Nil
add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
add0(z0, Nil) -> z0
goal(z0, z1) -> power(z0, z1)

Types:
POWER :: Cons:Nil -> Cons:Nil -> c:c1
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c :: c2:c3 -> c:c1 -> c:c1
MULT :: Cons:Nil -> Cons:Nil -> c2:c3
power :: Cons:Nil -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c1 :: c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
ADD0 :: Cons:Nil -> Cons:Nil -> c4:c5
mult :: Cons:Nil -> Cons:Nil -> Cons:Nil
c3 :: c2:c3
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c6
c6 :: c:c1 -> c6
add0 :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c:c11_7 :: c:c1
hole_Cons:Nil2_7 :: Cons:Nil
hole_c2:c33_7 :: c2:c3
hole_c4:c54_7 :: c4:c5
hole_c65_7 :: c6
gen_c:c16_7 :: Nat -> c:c1
gen_Cons:Nil7_7 :: Nat -> Cons:Nil
gen_c2:c38_7 :: Nat -> c2:c3
gen_c4:c59_7 :: Nat -> c4:c5


Lemmas:
ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(n11_7)) -> gen_c4:c59_7(n11_7), rt in Omega(1 + n11_7)
add0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(1, n574_7))) -> *10_7, rt in Omega(0)
mult(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1659106_7)) -> gen_Cons:Nil7_7(0), rt in Omega(0)
MULT(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1665969_7)) -> gen_c2:c38_7(n1665969_7), rt in Omega(1 + n1665969_7)


Generator Equations:
gen_c:c16_7(0) <=> c1
gen_c:c16_7(+(x, 1)) <=> c(c3, gen_c:c16_7(x))
gen_Cons:Nil7_7(0) <=> Nil
gen_Cons:Nil7_7(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil7_7(x))
gen_c2:c38_7(0) <=> c3
gen_c2:c38_7(+(x, 1)) <=> c2(c5, gen_c2:c38_7(x))
gen_c4:c59_7(0) <=> c5
gen_c4:c59_7(+(x, 1)) <=> c4(gen_c4:c59_7(x))


The following defined symbols remain to be analysed:
power, POWER

They will be analysed ascendingly in the following order:
power < POWER

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
power(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1667010_7)) -> *10_7, rt in Omega(0)

Induction Base:
power(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(0))

Induction Step:
power(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(+(n1667010_7, 1))) ->_R^Omega(0)
mult(gen_Cons:Nil7_7(0), power(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1667010_7))) ->_IH
mult(gen_Cons:Nil7_7(0), *10_7)

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:
POWER(z0, Cons(z1, z2)) -> c(MULT(z0, power(z0, z2)), POWER(z0, z2))
POWER(z0, Nil) -> c1
MULT(z0, Cons(z1, z2)) -> c2(ADD0(z0, mult(z0, z2)), MULT(z0, z2))
MULT(z0, Nil) -> c3
ADD0(z0, Cons(z1, z2)) -> c4(ADD0(z0, z2))
ADD0(z0, Nil) -> c5
GOAL(z0, z1) -> c6(POWER(z0, z1))
power(z0, Cons(z1, z2)) -> mult(z0, power(z0, z2))
power(z0, Nil) -> Cons(Nil, Nil)
mult(z0, Cons(z1, z2)) -> add0(z0, mult(z0, z2))
mult(z0, Nil) -> Nil
add0(z0, Cons(z1, z2)) -> Cons(Cons(Nil, Nil), add0(z0, z2))
add0(z0, Nil) -> z0
goal(z0, z1) -> power(z0, z1)

Types:
POWER :: Cons:Nil -> Cons:Nil -> c:c1
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c :: c2:c3 -> c:c1 -> c:c1
MULT :: Cons:Nil -> Cons:Nil -> c2:c3
power :: Cons:Nil -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c1 :: c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
ADD0 :: Cons:Nil -> Cons:Nil -> c4:c5
mult :: Cons:Nil -> Cons:Nil -> Cons:Nil
c3 :: c2:c3
c4 :: c4:c5 -> c4:c5
c5 :: c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c6
c6 :: c:c1 -> c6
add0 :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c:c11_7 :: c:c1
hole_Cons:Nil2_7 :: Cons:Nil
hole_c2:c33_7 :: c2:c3
hole_c4:c54_7 :: c4:c5
hole_c65_7 :: c6
gen_c:c16_7 :: Nat -> c:c1
gen_Cons:Nil7_7 :: Nat -> Cons:Nil
gen_c2:c38_7 :: Nat -> c2:c3
gen_c4:c59_7 :: Nat -> c4:c5


Lemmas:
ADD0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(n11_7)) -> gen_c4:c59_7(n11_7), rt in Omega(1 + n11_7)
add0(gen_Cons:Nil7_7(a), gen_Cons:Nil7_7(+(1, n574_7))) -> *10_7, rt in Omega(0)
mult(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1659106_7)) -> gen_Cons:Nil7_7(0), rt in Omega(0)
MULT(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1665969_7)) -> gen_c2:c38_7(n1665969_7), rt in Omega(1 + n1665969_7)
power(gen_Cons:Nil7_7(0), gen_Cons:Nil7_7(n1667010_7)) -> *10_7, rt in Omega(0)


Generator Equations:
gen_c:c16_7(0) <=> c1
gen_c:c16_7(+(x, 1)) <=> c(c3, gen_c:c16_7(x))
gen_Cons:Nil7_7(0) <=> Nil
gen_Cons:Nil7_7(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil7_7(x))
gen_c2:c38_7(0) <=> c3
gen_c2:c38_7(+(x, 1)) <=> c2(c5, gen_c2:c38_7(x))
gen_c4:c59_7(0) <=> c5
gen_c4:c59_7(+(x, 1)) <=> c4(gen_c4:c59_7(x))


The following defined symbols remain to be analysed:
POWER