KILLED
proof of input_XfcIBdQqHN.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 124 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(6) CpxTRS
(7) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(8) CdtProblem
    (9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxRelTRS
    (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) typed CpxTrs
    (15) OrderProof [LOWER BOUND(ID), 0 ms]
    (16) typed CpxTrs
    (17) RewriteLemmaProof [LOWER BOUND(ID), 694 ms]
    (18) typed CpxTrs
    (19) RewriteLemmaProof [LOWER BOUND(ID), 269 ms]
    (20) typed CpxTrs
    (21) RewriteLemmaProof [LOWER BOUND(ID), 55 ms]
    (22) BEST
        (23) proven lower bound
            (24) LowerBoundPropagationProof [FINISHED, 0 ms]
            (25) BOUNDS(n^1, INF)
        (26) typed CpxTrs
            (27) RewriteLemmaProof [LOWER BOUND(ID), 783 ms]
            (28) typed CpxTrs
(29) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(30) CdtProblem
    (31) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (32) CdtProblem
    (33) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (34) CdtProblem
    (35) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (36) CpxRelTRS
        (37) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
        (38) CpxTRS
        (39) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
        (40) CpxWeightedTrs
            (41) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
            (42) CpxWeightedTrs
            (43) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
            (44) CpxTypedWeightedTrs
            (45) CompletionProof [UPPER BOUND(ID), 0 ms]
            (46) CpxTypedWeightedCompleteTrs
                (47) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
                (48) CpxTypedWeightedCompleteTrs
                (49) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
                (50) CpxRNTS
                (51) InliningProof [UPPER BOUND(ID), 86 ms]
                (52) CpxRNTS
                (53) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
                (54) CpxRNTS
                (55) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
                (56) CpxRNTS
                (57) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (58) CpxRNTS
                (59) IntTrsBoundProof [UPPER BOUND(ID), 139 ms]
                (60) CpxRNTS
                (61) IntTrsBoundProof [UPPER BOUND(ID), 62 ms]
                (62) CpxRNTS
                (63) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (64) CpxRNTS
                (65) IntTrsBoundProof [UPPER BOUND(ID), 261 ms]
                (66) CpxRNTS
                (67) IntTrsBoundProof [UPPER BOUND(ID), 5 ms]
                (68) CpxRNTS
                (69) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (70) CpxRNTS
                (71) IntTrsBoundProof [UPPER BOUND(ID), 730 ms]
                (72) CpxRNTS
                (73) IntTrsBoundProof [UPPER BOUND(ID), 76 ms]
                (74) CpxRNTS
                (75) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (76) CpxRNTS
                (77) IntTrsBoundProof [UPPER BOUND(ID), 544 ms]
                (78) CpxRNTS
                (79) IntTrsBoundProof [UPPER BOUND(ID), 116 ms]
                (80) CpxRNTS
                (81) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (82) CpxRNTS
                (83) IntTrsBoundProof [UPPER BOUND(ID), 243 ms]
                (84) CpxRNTS
                (85) IntTrsBoundProof [UPPER BOUND(ID), 136 ms]
                (86) CpxRNTS
                (87) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (88) CpxRNTS
                (89) IntTrsBoundProof [UPPER BOUND(ID), 571 ms]
                (90) CpxRNTS
                (91) IntTrsBoundProof [UPPER BOUND(ID), 55 ms]
                (92) CpxRNTS
                (93) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (94) CpxRNTS
                (95) IntTrsBoundProof [UPPER BOUND(ID), 222 ms]
                (96) CpxRNTS
                (97) IntTrsBoundProof [UPPER BOUND(ID), 54 ms]
                (98) CpxRNTS
            (99) CompletionProof [UPPER BOUND(ID), 0 ms]
            (100) CpxTypedWeightedCompleteTrs
                (101) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
                (102) CpxRNTS
    (103) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 78 ms]
    (104) CdtProblem
        (105) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (106) CdtProblem
        (107) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
        (108) CdtProblem
        (109) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (110) CdtProblem
        (111) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
        (112) CdtProblem
        (113) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 0 ms]
        (114) CdtProblem
        (115) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (116) CdtProblem
        (117) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
        (118) CdtProblem
        (119) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
        (120) CdtProblem
        (121) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (122) CdtProblem
        (123) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
        (124) CdtProblem
        (125) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 18 ms]
        (126) CdtProblem
        (127) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (128) CdtProblem
        (129) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (130) CdtProblem
        (131) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (132) CdtProblem
        (133) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (134) CdtProblem
        (135) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (136) CdtProblem
(137) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(138) CpxWeightedTrs
    (139) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (140) CpxWeightedTrs
    (141) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (142) CpxTypedWeightedTrs
    (143) CompletionProof [UPPER BOUND(ID), 0 ms]
    (144) CpxTypedWeightedCompleteTrs
        (145) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (146) CpxTypedWeightedCompleteTrs
        (147) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (148) CpxRNTS
        (149) InliningProof [UPPER BOUND(ID), 85 ms]
        (150) CpxRNTS
        (151) SimplificationProof [BOTH BOUNDS(ID, ID), 3 ms]
        (152) CpxRNTS
        (153) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
        (154) CpxRNTS
        (155) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (156) CpxRNTS
        (157) IntTrsBoundProof [UPPER BOUND(ID), 234 ms]
        (158) CpxRNTS
        (159) IntTrsBoundProof [UPPER BOUND(ID), 7 ms]
        (160) CpxRNTS
        (161) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (162) CpxRNTS
        (163) IntTrsBoundProof [UPPER BOUND(ID), 549 ms]
        (164) CpxRNTS
        (165) IntTrsBoundProof [UPPER BOUND(ID), 128 ms]
        (166) CpxRNTS
        (167) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (168) CpxRNTS
        (169) IntTrsBoundProof [UPPER BOUND(ID), 485 ms]
        (170) CpxRNTS
        (171) IntTrsBoundProof [UPPER BOUND(ID), 0 ms]
        (172) CpxRNTS
        (173) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (174) CpxRNTS
        (175) IntTrsBoundProof [UPPER BOUND(ID), 602 ms]
        (176) CpxRNTS
        (177) IntTrsBoundProof [UPPER BOUND(ID), 0 ms]
        (178) CpxRNTS
    (179) CompletionProof [UPPER BOUND(ID), 0 ms]
    (180) CpxTypedWeightedCompleteTrs
        (181) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (182) CpxRNTS


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

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


The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x))
   mult(x', S(x)) -> add0(x', mult(x', x))
   add0(x', S(x)) -> +(S(0), add0(x', x))
   power(x, 0) -> S(0)
   mult(x, 0) -> 0
   add0(x, 0) -> x

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

   +(x, S(0)) -> S(x)
   +(S(0), y) -> S(y)

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x))
   mult(x', S(x)) -> add0(x', mult(x', x))
   add0(x', S(x)) -> +(S(0), add0(x', x))
   power(x, 0) -> S(0)
   mult(x, 0) -> 0
   add0(x, 0) -> x

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

   +(x, S(0)) -> S(x)
   +(S(0), y) -> S(y)

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

(4)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x))
   mult(x', S(x)) -> add0(x', mult(x', x))
   add0(x', S(x)) -> +'(S(0'), add0(x', x))
   power(x, 0') -> S(0')
   mult(x, 0') -> 0'
   add0(x, 0') -> x

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

   +'(x, S(0')) -> S(x)
   +'(S(0'), y) -> S(y)

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(5) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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


The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x))
   mult(x', S(x)) -> add0(x', mult(x', x))
   add0(x', S(x)) -> +(S(0), add0(x', x))
   power(x, 0) -> S(0)
   mult(x, 0) -> 0
   add0(x, 0) -> x
   +(x, S(0)) -> S(x)
   +(S(0), y) -> S(y)

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

(7) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   +'(z0, S(0)) -> c
   +'(S(0), z0) -> c1
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   POWER(z0, 0) -> c3
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   MULT(z0, 0) -> c5
   ADD0(z0, S(z1)) -> c6(+'(S(0), add0(z0, z1)), ADD0(z0, z1))
   ADD0(z0, 0) -> c7
S tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   POWER(z0, 0) -> c3
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   MULT(z0, 0) -> c5
   ADD0(z0, S(z1)) -> c6(+'(S(0), add0(z0, z1)), ADD0(z0, z1))
   ADD0(z0, 0) -> c7
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   +'_2, POWER_2, MULT_2, ADD0_2

Compound Symbols:   c, c1, c2_2, c3, c4_2, c5, c6_2, c7


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

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

(10)
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, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   POWER(z0, 0) -> c3
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   MULT(z0, 0) -> c5
   ADD0(z0, S(z1)) -> c6(+'(S(0), add0(z0, z1)), ADD0(z0, z1))
   ADD0(z0, 0) -> c7

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

   +'(z0, S(0)) -> c
   +'(S(0), z0) -> c1
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0

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

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

(12)
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, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   POWER(z0, 0') -> c3
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   MULT(z0, 0') -> c5
   ADD0(z0, S(z1)) -> c6(+'(S(0'), add0(z0, z1)), ADD0(z0, z1))
   ADD0(z0, 0') -> c7

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

   +'(z0, S(0')) -> c
   +'(S(0'), z0) -> c1
   +'(z0, S(0')) -> S(z0)
   +'(S(0'), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0') -> S(0')
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0') -> 0'
   add0(z0, S(z1)) -> +'(S(0'), add0(z0, z1))
   add0(z0, 0') -> z0

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

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

(14)
Obligation:
Innermost TRS:
Rules:
POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
POWER(z0, 0') -> c3
MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
MULT(z0, 0') -> c5
ADD0(z0, S(z1)) -> c6(+'(S(0'), add0(z0, z1)), ADD0(z0, z1))
ADD0(z0, 0') -> c7
+'(z0, S(0')) -> c
+'(S(0'), z0) -> c1
+'(z0, S(0')) -> S(z0)
+'(S(0'), z0) -> S(z0)
power(z0, S(z1)) -> mult(z0, power(z0, z1))
power(z0, 0') -> S(0')
mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
mult(z0, 0') -> 0'
add0(z0, S(z1)) -> +'(S(0'), add0(z0, z1))
add0(z0, 0') -> z0

Types:
POWER :: S:0':c:c1 -> S:0':c:c1 -> c2:c3
S :: S:0':c:c1 -> S:0':c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
MULT :: S:0':c:c1 -> S:0':c:c1 -> c4:c5
power :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
0' :: S:0':c:c1
c3 :: c2:c3
c4 :: c6:c7 -> c4:c5 -> c4:c5
ADD0 :: S:0':c:c1 -> S:0':c:c1 -> c6:c7
mult :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c5 :: c4:c5
c6 :: S:0':c:c1 -> c6:c7 -> c6:c7
+' :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
add0 :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c7 :: c6:c7
c :: S:0':c:c1
c1 :: S:0':c:c1
hole_c2:c31_8 :: c2:c3
hole_S:0':c:c12_8 :: S:0':c:c1
hole_c4:c53_8 :: c4:c5
hole_c6:c74_8 :: c6:c7
gen_c2:c35_8 :: Nat -> c2:c3
gen_S:0':c:c16_8 :: Nat -> S:0':c:c1
gen_c4:c57_8 :: Nat -> c4:c5
gen_c6:c78_8 :: Nat -> c6:c7

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

(15) 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 < ADD0
add0 < mult

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

(16)
Obligation:
Innermost TRS:
Rules:
POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
POWER(z0, 0') -> c3
MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
MULT(z0, 0') -> c5
ADD0(z0, S(z1)) -> c6(+'(S(0'), add0(z0, z1)), ADD0(z0, z1))
ADD0(z0, 0') -> c7
+'(z0, S(0')) -> c
+'(S(0'), z0) -> c1
+'(z0, S(0')) -> S(z0)
+'(S(0'), z0) -> S(z0)
power(z0, S(z1)) -> mult(z0, power(z0, z1))
power(z0, 0') -> S(0')
mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
mult(z0, 0') -> 0'
add0(z0, S(z1)) -> +'(S(0'), add0(z0, z1))
add0(z0, 0') -> z0

Types:
POWER :: S:0':c:c1 -> S:0':c:c1 -> c2:c3
S :: S:0':c:c1 -> S:0':c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
MULT :: S:0':c:c1 -> S:0':c:c1 -> c4:c5
power :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
0' :: S:0':c:c1
c3 :: c2:c3
c4 :: c6:c7 -> c4:c5 -> c4:c5
ADD0 :: S:0':c:c1 -> S:0':c:c1 -> c6:c7
mult :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c5 :: c4:c5
c6 :: S:0':c:c1 -> c6:c7 -> c6:c7
+' :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
add0 :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c7 :: c6:c7
c :: S:0':c:c1
c1 :: S:0':c:c1
hole_c2:c31_8 :: c2:c3
hole_S:0':c:c12_8 :: S:0':c:c1
hole_c4:c53_8 :: c4:c5
hole_c6:c74_8 :: c6:c7
gen_c2:c35_8 :: Nat -> c2:c3
gen_S:0':c:c16_8 :: Nat -> S:0':c:c1
gen_c4:c57_8 :: Nat -> c4:c5
gen_c6:c78_8 :: Nat -> c6:c7


Generator Equations:
gen_c2:c35_8(0) <=> c3
gen_c2:c35_8(+(x, 1)) <=> c2(c5, gen_c2:c35_8(x))
gen_S:0':c:c16_8(0) <=> 0'
gen_S:0':c:c16_8(+(x, 1)) <=> S(gen_S:0':c:c16_8(x))
gen_c4:c57_8(0) <=> c5
gen_c4:c57_8(+(x, 1)) <=> c4(c7, gen_c4:c57_8(x))
gen_c6:c78_8(0) <=> c7
gen_c6:c78_8(+(x, 1)) <=> c6(0', gen_c6:c78_8(x))


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

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

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(n10_8)) -> *9_8, rt in Omega(0)

Induction Base:
add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(0))

Induction Step:
add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(+(n10_8, 1))) ->_R^Omega(0)
+'(S(0'), add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(n10_8))) ->_IH
+'(S(0'), *9_8)

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, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
POWER(z0, 0') -> c3
MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
MULT(z0, 0') -> c5
ADD0(z0, S(z1)) -> c6(+'(S(0'), add0(z0, z1)), ADD0(z0, z1))
ADD0(z0, 0') -> c7
+'(z0, S(0')) -> c
+'(S(0'), z0) -> c1
+'(z0, S(0')) -> S(z0)
+'(S(0'), z0) -> S(z0)
power(z0, S(z1)) -> mult(z0, power(z0, z1))
power(z0, 0') -> S(0')
mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
mult(z0, 0') -> 0'
add0(z0, S(z1)) -> +'(S(0'), add0(z0, z1))
add0(z0, 0') -> z0

Types:
POWER :: S:0':c:c1 -> S:0':c:c1 -> c2:c3
S :: S:0':c:c1 -> S:0':c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
MULT :: S:0':c:c1 -> S:0':c:c1 -> c4:c5
power :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
0' :: S:0':c:c1
c3 :: c2:c3
c4 :: c6:c7 -> c4:c5 -> c4:c5
ADD0 :: S:0':c:c1 -> S:0':c:c1 -> c6:c7
mult :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c5 :: c4:c5
c6 :: S:0':c:c1 -> c6:c7 -> c6:c7
+' :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
add0 :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c7 :: c6:c7
c :: S:0':c:c1
c1 :: S:0':c:c1
hole_c2:c31_8 :: c2:c3
hole_S:0':c:c12_8 :: S:0':c:c1
hole_c4:c53_8 :: c4:c5
hole_c6:c74_8 :: c6:c7
gen_c2:c35_8 :: Nat -> c2:c3
gen_S:0':c:c16_8 :: Nat -> S:0':c:c1
gen_c4:c57_8 :: Nat -> c4:c5
gen_c6:c78_8 :: Nat -> c6:c7


Lemmas:
add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(n10_8)) -> *9_8, rt in Omega(0)


Generator Equations:
gen_c2:c35_8(0) <=> c3
gen_c2:c35_8(+(x, 1)) <=> c2(c5, gen_c2:c35_8(x))
gen_S:0':c:c16_8(0) <=> 0'
gen_S:0':c:c16_8(+(x, 1)) <=> S(gen_S:0':c:c16_8(x))
gen_c4:c57_8(0) <=> c5
gen_c4:c57_8(+(x, 1)) <=> c4(c7, gen_c4:c57_8(x))
gen_c6:c78_8(0) <=> c7
gen_c6:c78_8(+(x, 1)) <=> c6(0', gen_c6:c78_8(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
ADD0 < MULT
mult < MULT
mult < power

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n5493_8)) -> gen_S:0':c:c16_8(0), rt in Omega(0)

Induction Base:
mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(0)) ->_R^Omega(0)
0'

Induction Step:
mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(+(n5493_8, 1))) ->_R^Omega(0)
add0(gen_S:0':c:c16_8(0), mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n5493_8))) ->_IH
add0(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(0)) ->_R^Omega(0)
gen_S:0':c:c16_8(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, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
POWER(z0, 0') -> c3
MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
MULT(z0, 0') -> c5
ADD0(z0, S(z1)) -> c6(+'(S(0'), add0(z0, z1)), ADD0(z0, z1))
ADD0(z0, 0') -> c7
+'(z0, S(0')) -> c
+'(S(0'), z0) -> c1
+'(z0, S(0')) -> S(z0)
+'(S(0'), z0) -> S(z0)
power(z0, S(z1)) -> mult(z0, power(z0, z1))
power(z0, 0') -> S(0')
mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
mult(z0, 0') -> 0'
add0(z0, S(z1)) -> +'(S(0'), add0(z0, z1))
add0(z0, 0') -> z0

Types:
POWER :: S:0':c:c1 -> S:0':c:c1 -> c2:c3
S :: S:0':c:c1 -> S:0':c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
MULT :: S:0':c:c1 -> S:0':c:c1 -> c4:c5
power :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
0' :: S:0':c:c1
c3 :: c2:c3
c4 :: c6:c7 -> c4:c5 -> c4:c5
ADD0 :: S:0':c:c1 -> S:0':c:c1 -> c6:c7
mult :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c5 :: c4:c5
c6 :: S:0':c:c1 -> c6:c7 -> c6:c7
+' :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
add0 :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c7 :: c6:c7
c :: S:0':c:c1
c1 :: S:0':c:c1
hole_c2:c31_8 :: c2:c3
hole_S:0':c:c12_8 :: S:0':c:c1
hole_c4:c53_8 :: c4:c5
hole_c6:c74_8 :: c6:c7
gen_c2:c35_8 :: Nat -> c2:c3
gen_S:0':c:c16_8 :: Nat -> S:0':c:c1
gen_c4:c57_8 :: Nat -> c4:c5
gen_c6:c78_8 :: Nat -> c6:c7


Lemmas:
add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(n10_8)) -> *9_8, rt in Omega(0)
mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n5493_8)) -> gen_S:0':c:c16_8(0), rt in Omega(0)


Generator Equations:
gen_c2:c35_8(0) <=> c3
gen_c2:c35_8(+(x, 1)) <=> c2(c5, gen_c2:c35_8(x))
gen_S:0':c:c16_8(0) <=> 0'
gen_S:0':c:c16_8(+(x, 1)) <=> S(gen_S:0':c:c16_8(x))
gen_c4:c57_8(0) <=> c5
gen_c4:c57_8(+(x, 1)) <=> c4(c7, gen_c4:c57_8(x))
gen_c6:c78_8(0) <=> c7
gen_c6:c78_8(+(x, 1)) <=> c6(0', gen_c6:c78_8(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_S:0':c:c16_8(0), gen_S:0':c:c16_8(n7886_8)) -> gen_c4:c57_8(n7886_8), rt in Omega(1 + n7886_8)

Induction Base:
MULT(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(0)) ->_R^Omega(1)
c5

Induction Step:
MULT(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(+(n7886_8, 1))) ->_R^Omega(1)
c4(ADD0(gen_S:0':c:c16_8(0), mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n7886_8))), MULT(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n7886_8))) ->_L^Omega(0)
c4(ADD0(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(0)), MULT(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n7886_8))) ->_R^Omega(1)
c4(c7, MULT(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n7886_8))) ->_IH
c4(c7, gen_c4:c57_8(c7887_8))

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

(22)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
POWER(z0, 0') -> c3
MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
MULT(z0, 0') -> c5
ADD0(z0, S(z1)) -> c6(+'(S(0'), add0(z0, z1)), ADD0(z0, z1))
ADD0(z0, 0') -> c7
+'(z0, S(0')) -> c
+'(S(0'), z0) -> c1
+'(z0, S(0')) -> S(z0)
+'(S(0'), z0) -> S(z0)
power(z0, S(z1)) -> mult(z0, power(z0, z1))
power(z0, 0') -> S(0')
mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
mult(z0, 0') -> 0'
add0(z0, S(z1)) -> +'(S(0'), add0(z0, z1))
add0(z0, 0') -> z0

Types:
POWER :: S:0':c:c1 -> S:0':c:c1 -> c2:c3
S :: S:0':c:c1 -> S:0':c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
MULT :: S:0':c:c1 -> S:0':c:c1 -> c4:c5
power :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
0' :: S:0':c:c1
c3 :: c2:c3
c4 :: c6:c7 -> c4:c5 -> c4:c5
ADD0 :: S:0':c:c1 -> S:0':c:c1 -> c6:c7
mult :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c5 :: c4:c5
c6 :: S:0':c:c1 -> c6:c7 -> c6:c7
+' :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
add0 :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c7 :: c6:c7
c :: S:0':c:c1
c1 :: S:0':c:c1
hole_c2:c31_8 :: c2:c3
hole_S:0':c:c12_8 :: S:0':c:c1
hole_c4:c53_8 :: c4:c5
hole_c6:c74_8 :: c6:c7
gen_c2:c35_8 :: Nat -> c2:c3
gen_S:0':c:c16_8 :: Nat -> S:0':c:c1
gen_c4:c57_8 :: Nat -> c4:c5
gen_c6:c78_8 :: Nat -> c6:c7


Lemmas:
add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(n10_8)) -> *9_8, rt in Omega(0)
mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n5493_8)) -> gen_S:0':c:c16_8(0), rt in Omega(0)


Generator Equations:
gen_c2:c35_8(0) <=> c3
gen_c2:c35_8(+(x, 1)) <=> c2(c5, gen_c2:c35_8(x))
gen_S:0':c:c16_8(0) <=> 0'
gen_S:0':c:c16_8(+(x, 1)) <=> S(gen_S:0':c:c16_8(x))
gen_c4:c57_8(0) <=> c5
gen_c4:c57_8(+(x, 1)) <=> c4(c7, gen_c4:c57_8(x))
gen_c6:c78_8(0) <=> c7
gen_c6:c78_8(+(x, 1)) <=> c6(0', gen_c6:c78_8(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

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

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

(25)
BOUNDS(n^1, INF)

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

(26)
Obligation:
Innermost TRS:
Rules:
POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
POWER(z0, 0') -> c3
MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
MULT(z0, 0') -> c5
ADD0(z0, S(z1)) -> c6(+'(S(0'), add0(z0, z1)), ADD0(z0, z1))
ADD0(z0, 0') -> c7
+'(z0, S(0')) -> c
+'(S(0'), z0) -> c1
+'(z0, S(0')) -> S(z0)
+'(S(0'), z0) -> S(z0)
power(z0, S(z1)) -> mult(z0, power(z0, z1))
power(z0, 0') -> S(0')
mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
mult(z0, 0') -> 0'
add0(z0, S(z1)) -> +'(S(0'), add0(z0, z1))
add0(z0, 0') -> z0

Types:
POWER :: S:0':c:c1 -> S:0':c:c1 -> c2:c3
S :: S:0':c:c1 -> S:0':c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
MULT :: S:0':c:c1 -> S:0':c:c1 -> c4:c5
power :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
0' :: S:0':c:c1
c3 :: c2:c3
c4 :: c6:c7 -> c4:c5 -> c4:c5
ADD0 :: S:0':c:c1 -> S:0':c:c1 -> c6:c7
mult :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c5 :: c4:c5
c6 :: S:0':c:c1 -> c6:c7 -> c6:c7
+' :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
add0 :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c7 :: c6:c7
c :: S:0':c:c1
c1 :: S:0':c:c1
hole_c2:c31_8 :: c2:c3
hole_S:0':c:c12_8 :: S:0':c:c1
hole_c4:c53_8 :: c4:c5
hole_c6:c74_8 :: c6:c7
gen_c2:c35_8 :: Nat -> c2:c3
gen_S:0':c:c16_8 :: Nat -> S:0':c:c1
gen_c4:c57_8 :: Nat -> c4:c5
gen_c6:c78_8 :: Nat -> c6:c7


Lemmas:
add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(n10_8)) -> *9_8, rt in Omega(0)
mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n5493_8)) -> gen_S:0':c:c16_8(0), rt in Omega(0)
MULT(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n7886_8)) -> gen_c4:c57_8(n7886_8), rt in Omega(1 + n7886_8)


Generator Equations:
gen_c2:c35_8(0) <=> c3
gen_c2:c35_8(+(x, 1)) <=> c2(c5, gen_c2:c35_8(x))
gen_S:0':c:c16_8(0) <=> 0'
gen_S:0':c:c16_8(+(x, 1)) <=> S(gen_S:0':c:c16_8(x))
gen_c4:c57_8(0) <=> c5
gen_c4:c57_8(+(x, 1)) <=> c4(c7, gen_c4:c57_8(x))
gen_c6:c78_8(0) <=> c7
gen_c6:c78_8(+(x, 1)) <=> c6(0', gen_c6:c78_8(x))


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

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

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
power(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n8559_8)) -> *9_8, rt in Omega(0)

Induction Base:
power(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(0))

Induction Step:
power(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(+(n8559_8, 1))) ->_R^Omega(0)
mult(gen_S:0':c:c16_8(0), power(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n8559_8))) ->_IH
mult(gen_S:0':c:c16_8(0), *9_8)

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:
POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
POWER(z0, 0') -> c3
MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
MULT(z0, 0') -> c5
ADD0(z0, S(z1)) -> c6(+'(S(0'), add0(z0, z1)), ADD0(z0, z1))
ADD0(z0, 0') -> c7
+'(z0, S(0')) -> c
+'(S(0'), z0) -> c1
+'(z0, S(0')) -> S(z0)
+'(S(0'), z0) -> S(z0)
power(z0, S(z1)) -> mult(z0, power(z0, z1))
power(z0, 0') -> S(0')
mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
mult(z0, 0') -> 0'
add0(z0, S(z1)) -> +'(S(0'), add0(z0, z1))
add0(z0, 0') -> z0

Types:
POWER :: S:0':c:c1 -> S:0':c:c1 -> c2:c3
S :: S:0':c:c1 -> S:0':c:c1
c2 :: c4:c5 -> c2:c3 -> c2:c3
MULT :: S:0':c:c1 -> S:0':c:c1 -> c4:c5
power :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
0' :: S:0':c:c1
c3 :: c2:c3
c4 :: c6:c7 -> c4:c5 -> c4:c5
ADD0 :: S:0':c:c1 -> S:0':c:c1 -> c6:c7
mult :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c5 :: c4:c5
c6 :: S:0':c:c1 -> c6:c7 -> c6:c7
+' :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
add0 :: S:0':c:c1 -> S:0':c:c1 -> S:0':c:c1
c7 :: c6:c7
c :: S:0':c:c1
c1 :: S:0':c:c1
hole_c2:c31_8 :: c2:c3
hole_S:0':c:c12_8 :: S:0':c:c1
hole_c4:c53_8 :: c4:c5
hole_c6:c74_8 :: c6:c7
gen_c2:c35_8 :: Nat -> c2:c3
gen_S:0':c:c16_8 :: Nat -> S:0':c:c1
gen_c4:c57_8 :: Nat -> c4:c5
gen_c6:c78_8 :: Nat -> c6:c7


Lemmas:
add0(gen_S:0':c:c16_8(1), gen_S:0':c:c16_8(n10_8)) -> *9_8, rt in Omega(0)
mult(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n5493_8)) -> gen_S:0':c:c16_8(0), rt in Omega(0)
MULT(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n7886_8)) -> gen_c4:c57_8(n7886_8), rt in Omega(1 + n7886_8)
power(gen_S:0':c:c16_8(0), gen_S:0':c:c16_8(n8559_8)) -> *9_8, rt in Omega(0)


Generator Equations:
gen_c2:c35_8(0) <=> c3
gen_c2:c35_8(+(x, 1)) <=> c2(c5, gen_c2:c35_8(x))
gen_S:0':c:c16_8(0) <=> 0'
gen_S:0':c:c16_8(+(x, 1)) <=> S(gen_S:0':c:c16_8(x))
gen_c4:c57_8(0) <=> c5
gen_c4:c57_8(+(x, 1)) <=> c4(c7, gen_c4:c57_8(x))
gen_c6:c78_8(0) <=> c7
gen_c6:c78_8(+(x, 1)) <=> c6(0', gen_c6:c78_8(x))


The following defined symbols remain to be analysed:
POWER
----------------------------------------

(29) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(30)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   +'(z0, S(0)) -> c
   +'(S(0), z0) -> c1
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   POWER(z0, 0) -> c3
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   MULT(z0, 0) -> c5
   ADD0(z0, S(z1)) -> c6(+'(S(0), add0(z0, z1)), ADD0(z0, z1))
   ADD0(z0, 0) -> c7
S tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   POWER(z0, 0) -> c3
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   MULT(z0, 0) -> c5
   ADD0(z0, S(z1)) -> c6(+'(S(0), add0(z0, z1)), ADD0(z0, z1))
   ADD0(z0, 0) -> c7
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   +'_2, POWER_2, MULT_2, ADD0_2

Compound Symbols:   c, c1, c2_2, c3, c4_2, c5, c6_2, c7


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

(31) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 5 trailing nodes:
   +'(S(0), z0) -> c1
   POWER(z0, 0) -> c3
   MULT(z0, 0) -> c5
   +'(z0, S(0)) -> c
   ADD0(z0, 0) -> c7

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

(32)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(+'(S(0), add0(z0, z1)), ADD0(z0, z1))
S tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(+'(S(0), add0(z0, z1)), ADD0(z0, z1))
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   POWER_2, MULT_2, ADD0_2

Compound Symbols:   c2_2, c4_2, c6_2


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

(33) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing tuple parts
----------------------------------------

(34)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
S tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   POWER_2, MULT_2, ADD0_2

Compound Symbols:   c2_2, c4_2, c6_1


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

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

(36)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))

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

   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0

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

(37) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(38)
Obligation:
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0

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

(39) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(40)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1)) [1]
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1)) [1]
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1)) [1]
   +(z0, S(0)) -> S(z0) [0]
   +(S(0), z0) -> S(z0) [0]
   power(z0, S(z1)) -> mult(z0, power(z0, z1)) [0]
   power(z0, 0) -> S(0) [0]
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1)) [0]
   mult(z0, 0) -> 0 [0]
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1)) [0]
   add0(z0, 0) -> z0 [0]

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

(41) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID))
Renamed defined symbols to avoid conflicts with arithmetic symbols:

+ => plus

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

(42)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1)) [1]
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1)) [1]
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1)) [1]
   plus(z0, S(0)) -> S(z0) [0]
   plus(S(0), z0) -> S(z0) [0]
   power(z0, S(z1)) -> mult(z0, power(z0, z1)) [0]
   power(z0, 0) -> S(0) [0]
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1)) [0]
   mult(z0, 0) -> 0 [0]
   add0(z0, S(z1)) -> plus(S(0), add0(z0, z1)) [0]
   add0(z0, 0) -> z0 [0]

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

(43) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(44)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1)) [1]
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1)) [1]
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1)) [1]
   plus(z0, S(0)) -> S(z0) [0]
   plus(S(0), z0) -> S(z0) [0]
   power(z0, S(z1)) -> mult(z0, power(z0, z1)) [0]
   power(z0, 0) -> S(0) [0]
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1)) [0]
   mult(z0, 0) -> 0 [0]
   add0(z0, S(z1)) -> plus(S(0), add0(z0, z1)) [0]
   add0(z0, 0) -> z0 [0]

The TRS has the following type information:
POWER :: S:0 -> S:0 -> c2
S :: S:0 -> S:0
c2 :: c4 -> c2 -> c2
MULT :: S:0 -> S:0 -> c4
power :: S:0 -> S:0 -> S:0
c4 :: c6 -> c4 -> c4
ADD0 :: S:0 -> S:0 -> c6
mult :: S:0 -> S:0 -> S:0
c6 :: c6 -> c6
plus :: S:0 -> S:0 -> S:0
0 :: S:0
add0 :: S:0 -> S:0 -> S:0

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

(45) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

   POWER_2
   MULT_2
   ADD0_2

(c) The following functions are completely defined:

   plus_2
   power_2
   mult_2
   add0_2

Due to the following rules being added:

   plus(v0, v1) -> 0 [0]
   power(v0, v1) -> 0 [0]
   mult(v0, v1) -> 0 [0]
   add0(v0, v1) -> 0 [0]

And the following fresh constants:    const, const1, const2

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

(46)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1)) [1]
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1)) [1]
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1)) [1]
   plus(z0, S(0)) -> S(z0) [0]
   plus(S(0), z0) -> S(z0) [0]
   power(z0, S(z1)) -> mult(z0, power(z0, z1)) [0]
   power(z0, 0) -> S(0) [0]
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1)) [0]
   mult(z0, 0) -> 0 [0]
   add0(z0, S(z1)) -> plus(S(0), add0(z0, z1)) [0]
   add0(z0, 0) -> z0 [0]
   plus(v0, v1) -> 0 [0]
   power(v0, v1) -> 0 [0]
   mult(v0, v1) -> 0 [0]
   add0(v0, v1) -> 0 [0]

The TRS has the following type information:
POWER :: S:0 -> S:0 -> c2
S :: S:0 -> S:0
c2 :: c4 -> c2 -> c2
MULT :: S:0 -> S:0 -> c4
power :: S:0 -> S:0 -> S:0
c4 :: c6 -> c4 -> c4
ADD0 :: S:0 -> S:0 -> c6
mult :: S:0 -> S:0 -> S:0
c6 :: c6 -> c6
plus :: S:0 -> S:0 -> S:0
0 :: S:0
add0 :: S:0 -> S:0 -> S:0
const :: c2
const1 :: c4
const2 :: c6

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

(47) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(48)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   POWER(z0, S(S(z1'))) -> c2(MULT(z0, mult(z0, power(z0, z1'))), POWER(z0, S(z1'))) [1]
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)), POWER(z0, 0)) [1]
   POWER(z0, S(z1)) -> c2(MULT(z0, 0), POWER(z0, z1)) [1]
   MULT(z0, S(S(z1''))) -> c4(ADD0(z0, add0(z0, mult(z0, z1''))), MULT(z0, S(z1''))) [1]
   MULT(z0, S(0)) -> c4(ADD0(z0, 0), MULT(z0, 0)) [1]
   MULT(z0, S(z1)) -> c4(ADD0(z0, 0), MULT(z0, z1)) [1]
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1)) [1]
   plus(z0, S(0)) -> S(z0) [0]
   plus(S(0), z0) -> S(z0) [0]
   power(z0, S(S(z11))) -> mult(z0, mult(z0, power(z0, z11))) [0]
   power(z0, S(0)) -> mult(z0, S(0)) [0]
   power(z0, S(z1)) -> mult(z0, 0) [0]
   power(z0, 0) -> S(0) [0]
   mult(z0, S(S(z12))) -> add0(z0, add0(z0, mult(z0, z12))) [0]
   mult(z0, S(0)) -> add0(z0, 0) [0]
   mult(z0, S(z1)) -> add0(z0, 0) [0]
   mult(z0, 0) -> 0 [0]
   add0(z0, S(S(z13))) -> plus(S(0), plus(S(0), add0(z0, z13))) [0]
   add0(z0, S(0)) -> plus(S(0), z0) [0]
   add0(z0, S(z1)) -> plus(S(0), 0) [0]
   add0(z0, 0) -> z0 [0]
   plus(v0, v1) -> 0 [0]
   power(v0, v1) -> 0 [0]
   mult(v0, v1) -> 0 [0]
   add0(v0, v1) -> 0 [0]

The TRS has the following type information:
POWER :: S:0 -> S:0 -> c2
S :: S:0 -> S:0
c2 :: c4 -> c2 -> c2
MULT :: S:0 -> S:0 -> c4
power :: S:0 -> S:0 -> S:0
c4 :: c6 -> c4 -> c4
ADD0 :: S:0 -> S:0 -> c6
mult :: S:0 -> S:0 -> S:0
c6 :: c6 -> c6
plus :: S:0 -> S:0 -> S:0
0 :: S:0
add0 :: S:0 -> S:0 -> S:0
const :: c2
const1 :: c4
const2 :: c6

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

(49) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   0 => 0
   const => 0
   const1 => 0
   const2 => 0

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

(50)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ 1 }-> 1 + ADD0(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   MULT(z, z') -{ 1 }-> 1 + ADD0(z0, add0(z0, mult(z0, z1''))) + MULT(z0, 1 + z1'') :|: z = z0, z' = 1 + (1 + z1''), z0 >= 0, z1'' >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z0, 0) + MULT(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   MULT(z, z') -{ 1 }-> 1 + ADD0(z0, 0) + MULT(z0, 0) :|: z = z0, z' = 1 + 0, z0 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z0, mult(z0, power(z0, z1'))) + POWER(z0, 1 + z1') :|: z' = 1 + (1 + z1'), z = z0, z1' >= 0, z0 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z0, 0) + POWER(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   POWER(z, z') -{ 1 }-> 1 + MULT(z0, 1 + 0) + POWER(z0, 0) :|: z = z0, z' = 1 + 0, z0 >= 0
   add0(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, z0) :|: z = z0, z' = 1 + 0, z0 >= 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z0, z13))) :|: z = z0, z' = 1 + (1 + z13), z0 >= 0, z13 >= 0
   add0(z, z') -{ 0 }-> plus(1 + 0, 0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   add0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   mult(z, z') -{ 0 }-> add0(z0, add0(z0, mult(z0, z12))) :|: z = z0, z' = 1 + (1 + z12), z0 >= 0, z12 >= 0
   mult(z, z') -{ 0 }-> add0(z0, 0) :|: z = z0, z' = 1 + 0, z0 >= 0
   mult(z, z') -{ 0 }-> add0(z0, 0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   mult(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + z0 :|: z = z0, z' = 1 + 0, z0 >= 0
   plus(z, z') -{ 0 }-> 1 + z0 :|: z = 1 + 0, z0 >= 0, z' = z0
   power(z, z') -{ 0 }-> mult(z0, mult(z0, power(z0, z11))) :|: z = z0, z11 >= 0, z0 >= 0, z' = 1 + (1 + z11)
   power(z, z') -{ 0 }-> mult(z0, 0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   power(z, z') -{ 0 }-> mult(z0, 1 + 0) :|: z = z0, z' = 1 + 0, z0 >= 0
   power(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   power(z, z') -{ 0 }-> 1 + 0 :|: z = z0, z0 >= 0, z' = 0


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

(51) InliningProof (UPPER BOUND(ID))
Inlined the following terminating rules on right-hand sides where appropriate:

   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + z0 :|: z = z0, z' = 1 + 0, z0 >= 0
   plus(z, z') -{ 0 }-> 1 + z0 :|: z = 1 + 0, z0 >= 0, z' = z0

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

(52)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ 1 }-> 1 + ADD0(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   MULT(z, z') -{ 1 }-> 1 + ADD0(z0, add0(z0, mult(z0, z1''))) + MULT(z0, 1 + z1'') :|: z = z0, z' = 1 + (1 + z1''), z0 >= 0, z1'' >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z0, 0) + MULT(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   MULT(z, z') -{ 1 }-> 1 + ADD0(z0, 0) + MULT(z0, 0) :|: z = z0, z' = 1 + 0, z0 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z0, mult(z0, power(z0, z1'))) + POWER(z0, 1 + z1') :|: z' = 1 + (1 + z1'), z = z0, z1' >= 0, z0 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z0, 0) + POWER(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   POWER(z, z') -{ 1 }-> 1 + MULT(z0, 1 + 0) + POWER(z0, 0) :|: z = z0, z' = 1 + 0, z0 >= 0
   add0(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z0, z13))) :|: z = z0, z' = 1 + (1 + z13), z0 >= 0, z13 >= 0
   add0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   add0(z, z') -{ 0 }-> 0 :|: z = z0, z' = 1 + 0, z0 >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, z0 = v1
   add0(z, z') -{ 0 }-> 0 :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z0' :|: z = z0, z' = 1 + 0, z0 >= 0, 1 + 0 = z0', z0 = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z = z0, z' = 1 + 0, z0 >= 0, 1 + 0 = 1 + 0, z0' >= 0, z0 = z0'
   add0(z, z') -{ 0 }-> 1 + z0' :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z0, add0(z0, mult(z0, z12))) :|: z = z0, z' = 1 + (1 + z12), z0 >= 0, z12 >= 0
   mult(z, z') -{ 0 }-> add0(z0, 0) :|: z = z0, z' = 1 + 0, z0 >= 0
   mult(z, z') -{ 0 }-> add0(z0, 0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   mult(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + z0 :|: z = z0, z' = 1 + 0, z0 >= 0
   plus(z, z') -{ 0 }-> 1 + z0 :|: z = 1 + 0, z0 >= 0, z' = z0
   power(z, z') -{ 0 }-> mult(z0, mult(z0, power(z0, z11))) :|: z = z0, z11 >= 0, z0 >= 0, z' = 1 + (1 + z11)
   power(z, z') -{ 0 }-> mult(z0, 0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   power(z, z') -{ 0 }-> mult(z0, 1 + 0) :|: z = z0, z' = 1 + 0, z0 >= 0
   power(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   power(z, z') -{ 0 }-> 1 + 0 :|: z = z0, z0 >= 0, z' = 0


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

(53) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(54)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ 1 }-> 1 + ADD0(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, 0) :|: z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0


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

(55) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { ADD0 }
   { plus }
   { add0 }
   { mult }
   { MULT }
   { power }
   { POWER }

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

(56)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ 1 }-> 1 + ADD0(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, 0) :|: z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {ADD0}, {plus}, {add0}, {mult}, {MULT}, {power}, {POWER}

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

(57) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(58)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ 1 }-> 1 + ADD0(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, 0) :|: z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {ADD0}, {plus}, {add0}, {mult}, {MULT}, {power}, {POWER}

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

(59) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: ADD0
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(60)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ 1 }-> 1 + ADD0(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, 0) :|: z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {ADD0}, {plus}, {add0}, {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: ?, size: O(1) [0]

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

(61) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: ADD0
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z'

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

(62)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ 1 }-> 1 + ADD0(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, 0) :|: z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, 0) + MULT(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {plus}, {add0}, {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]

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

(63) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(64)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {plus}, {add0}, {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]

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

(65) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: plus
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z + z'

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

(66)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {plus}, {add0}, {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: ?, size: O(n^1) [z + z']

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

(67) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: plus
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(68)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {add0}, {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']

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

(69) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(70)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {add0}, {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']

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

(71) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: add0
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z + z'

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

(72)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {add0}, {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: ?, size: O(n^1) [z + z']

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

(73) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: add0
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(74)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, 0) :|: z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']

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

(75) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(76)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']

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

(77) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: mult
after applying outer abstraction to obtain an ITS,
resulting in: O(n^2) with polynomial bound: 2*z + 2*z*z'

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

(78)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {mult}, {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: ?, size: O(n^2) [2*z + 2*z*z']

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

(79) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: mult
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(80)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + ADD0(z, add0(z, mult(z, z' - 2))) + MULT(z, 1 + (z' - 2)) :|: z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 0) :|: z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, 1 + 0) :|: z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']

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

(81) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(82)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 + s7 }-> 1 + s8 + MULT(z, 1 + (z' - 2)) :|: s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']

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

(83) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: MULT
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(84)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 + s7 }-> 1 + s8 + MULT(z, 1 + (z' - 2)) :|: s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {MULT}, {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']
  MULT: runtime: ?, size: O(1) [0]

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

(85) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: MULT
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 3*z*z' + 2*z*z'^2 + 3*z'

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

(86)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + MULT(z, 0) :|: s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s' + MULT(z, z' - 1) :|: s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 + s7 }-> 1 + s8 + MULT(z, 1 + (z' - 2)) :|: s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 0) + POWER(z, z' - 1) :|: z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, 1 + 0) + POWER(z, 0) :|: z' = 1 + 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']
  MULT: runtime: O(n^3) [3*z*z' + 2*z*z'^2 + 3*z'], size: O(1) [0]

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

(87) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(88)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + s17 :|: s17 >= 0, s17 <= 0, s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ -2 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s' + s18 :|: s18 >= 0, s18 <= 0, s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ -2 + s7 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s8 + s16 :|: s16 >= 0, s16 <= 0, s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 4 + 5*z }-> 1 + s14 + POWER(z, 0) :|: s14 >= 0, s14 <= 0, z' = 1 + 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + s15 + POWER(z, z' - 1) :|: s15 >= 0, s15 <= 0, z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']
  MULT: runtime: O(n^3) [3*z*z' + 2*z*z'^2 + 3*z'], size: O(1) [0]

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

(89) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: power
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

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

(90)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + s17 :|: s17 >= 0, s17 <= 0, s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ -2 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s' + s18 :|: s18 >= 0, s18 <= 0, s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ -2 + s7 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s8 + s16 :|: s16 >= 0, s16 <= 0, s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 4 + 5*z }-> 1 + s14 + POWER(z, 0) :|: s14 >= 0, s14 <= 0, z' = 1 + 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + s15 + POWER(z, z' - 1) :|: s15 >= 0, s15 <= 0, z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {power}, {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']
  MULT: runtime: O(n^3) [3*z*z' + 2*z*z'^2 + 3*z'], size: O(1) [0]
  power: runtime: ?, size: INF

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

(91) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: power
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(92)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + s17 :|: s17 >= 0, s17 <= 0, s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ -2 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s' + s18 :|: s18 >= 0, s18 <= 0, s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ -2 + s7 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s8 + s16 :|: s16 >= 0, s16 <= 0, s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 4 + 5*z }-> 1 + s14 + POWER(z, 0) :|: s14 >= 0, s14 <= 0, z' = 1 + 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + s15 + POWER(z, z' - 1) :|: s15 >= 0, s15 <= 0, z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + MULT(z, mult(z, power(z, z' - 2))) + POWER(z, 1 + (z' - 2)) :|: z' - 2 >= 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']
  MULT: runtime: O(n^3) [3*z*z' + 2*z*z'^2 + 3*z'], size: O(1) [0]
  power: runtime: O(1) [0], size: INF

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

(93) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(94)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + s17 :|: s17 >= 0, s17 <= 0, s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ -2 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s' + s18 :|: s18 >= 0, s18 <= 0, s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ -2 + s7 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s8 + s16 :|: s16 >= 0, s16 <= 0, s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 4 + 5*z }-> 1 + s14 + POWER(z, 0) :|: s14 >= 0, s14 <= 0, z' = 1 + 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + s15 + POWER(z, z' - 1) :|: s15 >= 0, s15 <= 0, z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 + 3*s20 + 3*s20*z + 2*s20^2*z }-> 1 + s21 + POWER(z, 1 + (z' - 2)) :|: s19 >= 0, s19 <= inf, s20 >= 0, s20 <= 2 * (s19 * z) + 2 * z, s21 >= 0, s21 <= 0, z' - 2 >= 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s24 :|: s22 >= 0, s22 <= inf', s23 >= 0, s23 <= 2 * (s22 * z) + 2 * z, s24 >= 0, s24 <= 2 * (s23 * z) + 2 * z, z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']
  MULT: runtime: O(n^3) [3*z*z' + 2*z*z'^2 + 3*z'], size: O(1) [0]
  power: runtime: O(1) [0], size: INF

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

(95) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: POWER
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(96)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + s17 :|: s17 >= 0, s17 <= 0, s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ -2 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s' + s18 :|: s18 >= 0, s18 <= 0, s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ -2 + s7 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s8 + s16 :|: s16 >= 0, s16 <= 0, s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 4 + 5*z }-> 1 + s14 + POWER(z, 0) :|: s14 >= 0, s14 <= 0, z' = 1 + 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + s15 + POWER(z, z' - 1) :|: s15 >= 0, s15 <= 0, z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 + 3*s20 + 3*s20*z + 2*s20^2*z }-> 1 + s21 + POWER(z, 1 + (z' - 2)) :|: s19 >= 0, s19 <= inf, s20 >= 0, s20 <= 2 * (s19 * z) + 2 * z, s21 >= 0, s21 <= 0, z' - 2 >= 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s24 :|: s22 >= 0, s22 <= inf', s23 >= 0, s23 <= 2 * (s22 * z) + 2 * z, s24 >= 0, s24 <= 2 * (s23 * z) + 2 * z, z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']
  MULT: runtime: O(n^3) [3*z*z' + 2*z*z'^2 + 3*z'], size: O(1) [0]
  power: runtime: O(1) [0], size: INF
  POWER: runtime: ?, size: O(1) [0]

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

(97) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: POWER
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

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

(98)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ z' }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ 1 }-> 1 + s + s17 :|: s17 >= 0, s17 <= 0, s >= 0, s <= 0, z' = 1 + 0, z >= 0
   MULT(z, z') -{ -2 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s' + s18 :|: s18 >= 0, s18 <= 0, s' >= 0, s' <= 0, z' - 1 >= 0, z >= 0
   MULT(z, z') -{ -2 + s7 + -1*z + -1*z*z' + 2*z*z'^2 + 3*z' }-> 1 + s8 + s16 :|: s16 >= 0, s16 <= 0, s6 >= 0, s6 <= 2 * ((z' - 2) * z) + 2 * z, s7 >= 0, s7 <= z + s6, s8 >= 0, s8 <= 0, z >= 0, z' - 2 >= 0
   POWER(z, z') -{ 4 + 5*z }-> 1 + s14 + POWER(z, 0) :|: s14 >= 0, s14 <= 0, z' = 1 + 0, z >= 0
   POWER(z, z') -{ 1 }-> 1 + s15 + POWER(z, z' - 1) :|: s15 >= 0, s15 <= 0, z' - 1 >= 0, z >= 0
   POWER(z, z') -{ 1 + 3*s20 + 3*s20*z + 2*s20^2*z }-> 1 + s21 + POWER(z, 1 + (z' - 2)) :|: s19 >= 0, s19 <= inf, s20 >= 0, s20 <= 2 * (s19 * z) + 2 * z, s21 >= 0, s21 <= 0, z' - 2 >= 0, z >= 0
   add0(z, z') -{ 0 }-> s5 :|: s3 >= 0, s3 <= z + (z' - 2), s4 >= 0, s4 <= 1 + 0 + s3, s5 >= 0, s5 <= 1 + 0 + s4, z >= 0, z' - 2 >= 0
   add0(z, z') -{ 0 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   add0(z, z') -{ 0 }-> 0 :|: z' = 1 + 0, z >= 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 0 }-> 0 :|: z' - 1 >= 0, z >= 0, v0 >= 0, v1 >= 0, 1 + 0 = v0, 0 = v1
   add0(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0, 1 + 0 = 1 + 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' = 1 + 0, z >= 0, 1 + 0 = z0', z = 1 + 0, z0' >= 0
   add0(z, z') -{ 0 }-> 1 + z0' :|: z' - 1 >= 0, z >= 0, 1 + 0 = 1 + 0, z0' >= 0, 0 = z0'
   mult(z, z') -{ 0 }-> s1 :|: s1 >= 0, s1 <= z + 0, z' = 1 + 0, z >= 0
   mult(z, z') -{ 0 }-> s13 :|: s11 >= 0, s11 <= 2 * ((z' - 2) * z) + 2 * z, s12 >= 0, s12 <= z + s11, s13 >= 0, s13 <= z + s12, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 0 }-> s2 :|: s2 >= 0, s2 <= z + 0, z' - 1 >= 0, z >= 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z' = 1 + 0, z >= 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 0 }-> s10 :|: s10 >= 0, s10 <= 2 * (0 * z) + 2 * z, z' - 1 >= 0, z >= 0
   power(z, z') -{ 0 }-> s24 :|: s22 >= 0, s22 <= inf', s23 >= 0, s23 <= 2 * (s22 * z) + 2 * z, s24 >= 0, s24 <= 2 * (s23 * z) + 2 * z, z' - 2 >= 0, z >= 0
   power(z, z') -{ 0 }-> s9 :|: s9 >= 0, s9 <= 2 * ((1 + 0) * z) + 2 * z, z' = 1 + 0, z >= 0
   power(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   power(z, z') -{ 0 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {POWER}
Previous analysis results are:
  ADD0: runtime: O(n^1) [z'], size: O(1) [0]
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(1) [0], size: O(n^1) [z + z']
  mult: runtime: O(1) [0], size: O(n^2) [2*z + 2*z*z']
  MULT: runtime: O(n^3) [3*z*z' + 2*z*z'^2 + 3*z'], size: O(1) [0]
  power: runtime: O(1) [0], size: INF
  POWER: runtime: INF, size: O(1) [0]

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

(99) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   plus(v0, v1) -> null_plus [0]
   power(v0, v1) -> null_power [0]
   mult(v0, v1) -> null_mult [0]
   add0(v0, v1) -> null_add0 [0]
   POWER(v0, v1) -> null_POWER [0]
   MULT(v0, v1) -> null_MULT [0]
   ADD0(v0, v1) -> null_ADD0 [0]

And the following fresh constants:    null_plus, null_power, null_mult, null_add0, null_POWER, null_MULT, null_ADD0

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

(100)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1)) [1]
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1)) [1]
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1)) [1]
   plus(z0, S(0)) -> S(z0) [0]
   plus(S(0), z0) -> S(z0) [0]
   power(z0, S(z1)) -> mult(z0, power(z0, z1)) [0]
   power(z0, 0) -> S(0) [0]
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1)) [0]
   mult(z0, 0) -> 0 [0]
   add0(z0, S(z1)) -> plus(S(0), add0(z0, z1)) [0]
   add0(z0, 0) -> z0 [0]
   plus(v0, v1) -> null_plus [0]
   power(v0, v1) -> null_power [0]
   mult(v0, v1) -> null_mult [0]
   add0(v0, v1) -> null_add0 [0]
   POWER(v0, v1) -> null_POWER [0]
   MULT(v0, v1) -> null_MULT [0]
   ADD0(v0, v1) -> null_ADD0 [0]

The TRS has the following type information:
POWER :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> c2:null_POWER
S :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
c2 :: c4:null_MULT -> c2:null_POWER -> c2:null_POWER
MULT :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> c4:null_MULT
power :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
c4 :: c6:null_ADD0 -> c4:null_MULT -> c4:null_MULT
ADD0 :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> c6:null_ADD0
mult :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
c6 :: c6:null_ADD0 -> c6:null_ADD0
plus :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
0 :: S:0:null_plus:null_power:null_mult:null_add0
add0 :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
null_plus :: S:0:null_plus:null_power:null_mult:null_add0
null_power :: S:0:null_plus:null_power:null_mult:null_add0
null_mult :: S:0:null_plus:null_power:null_mult:null_add0
null_add0 :: S:0:null_plus:null_power:null_mult:null_add0
null_POWER :: c2:null_POWER
null_MULT :: c4:null_MULT
null_ADD0 :: c6:null_ADD0

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

(101) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   0 => 0
   null_plus => 0
   null_power => 0
   null_mult => 0
   null_add0 => 0
   null_POWER => 0
   null_MULT => 0
   null_ADD0 => 0

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

(102)
Obligation:
Complexity RNTS consisting of the following rules:

   ADD0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   ADD0(z, z') -{ 1 }-> 1 + ADD0(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   MULT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MULT(z, z') -{ 1 }-> 1 + ADD0(z0, mult(z0, z1)) + MULT(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   POWER(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   POWER(z, z') -{ 1 }-> 1 + MULT(z0, power(z0, z1)) + POWER(z0, z1) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   add0(z, z') -{ 0 }-> z0 :|: z = z0, z0 >= 0, z' = 0
   add0(z, z') -{ 0 }-> plus(1 + 0, add0(z0, z1)) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   add0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   mult(z, z') -{ 0 }-> add0(z0, mult(z0, z1)) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   mult(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + z0 :|: z = z0, z' = 1 + 0, z0 >= 0
   plus(z, z') -{ 0 }-> 1 + z0 :|: z = 1 + 0, z0 >= 0, z' = z0
   power(z, z') -{ 0 }-> mult(z0, power(z0, z1)) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1
   power(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   power(z, z') -{ 0 }-> 1 + 0 :|: z = z0, z0 >= 0, z' = 0

Only complete derivations are relevant for the runtime complexity.

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

(103) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(+(x_1, x_2)) = [3] + [3]x_1 + [3]x_2
   POL(0) = 0
   POL(ADD0(x_1, x_2)) = 0
   POL(MULT(x_1, x_2)) = [1]
   POL(POWER(x_1, x_2)) = [2]x_2
   POL(S(x_1)) = [2] + x_1
   POL(add0(x_1, x_2)) = [3] + [3]x_1
   POL(c2(x_1, x_2)) = x_1 + x_2
   POL(c4(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1)) = x_1
   POL(mult(x_1, x_2)) = [3] + [3]x_1
   POL(power(x_1, x_2)) = [3] + [3]x_1

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

(104)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
S tuples:
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
K tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   POWER_2, MULT_2, ADD0_2

Compound Symbols:   c2_2, c4_2, c6_1


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

(105) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1)) by 
   POWER(z0, S(S(z1))) -> c2(MULT(z0, mult(z0, power(z0, z1))), POWER(z0, S(z1)))
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)), POWER(z0, 0))

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

(106)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(z1))) -> c2(MULT(z0, mult(z0, power(z0, z1))), POWER(z0, S(z1)))
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)), POWER(z0, 0))
S tuples:
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
K tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   MULT_2, ADD0_2, POWER_2

Compound Symbols:   c4_2, c6_1, c2_2


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

(107) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing tuple parts
----------------------------------------

(108)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(z1))) -> c2(MULT(z0, mult(z0, power(z0, z1))), POWER(z0, S(z1)))
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)))
S tuples:
   MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1))
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
K tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   MULT_2, ADD0_2, POWER_2

Compound Symbols:   c4_2, c6_1, c2_2, c2_1


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

(109) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace MULT(z0, S(z1)) -> c4(ADD0(z0, mult(z0, z1)), MULT(z0, z1)) by 
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   MULT(z0, S(0)) -> c4(ADD0(z0, 0), MULT(z0, 0))

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

(110)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(z1))) -> c2(MULT(z0, mult(z0, power(z0, z1))), POWER(z0, S(z1)))
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   MULT(z0, S(0)) -> c4(ADD0(z0, 0), MULT(z0, 0))
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   MULT(z0, S(0)) -> c4(ADD0(z0, 0), MULT(z0, 0))
K tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, POWER_2, MULT_2

Compound Symbols:   c6_1, c2_2, c2_1, c4_2


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

(111) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing tuple parts
----------------------------------------

(112)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(z1))) -> c2(MULT(z0, mult(z0, power(z0, z1))), POWER(z0, S(z1)))
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   MULT(z0, S(0)) -> c4
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   MULT(z0, S(0)) -> c4
K tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, POWER_2, MULT_2

Compound Symbols:   c6_1, c2_2, c2_1, c4_2, c4


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

(113) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   MULT(z0, S(0)) -> c4
We considered the (Usable) Rules:none
And the Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(z1))) -> c2(MULT(z0, mult(z0, power(z0, z1))), POWER(z0, S(z1)))
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   MULT(z0, S(0)) -> c4
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(+(x_1, x_2)) = x_1 + x_2
   POL(0) = 0
   POL(ADD0(x_1, x_2)) = 0
   POL(MULT(x_1, x_2)) = [1]
   POL(POWER(x_1, x_2)) = [1] + x_2
   POL(S(x_1)) = [1] + x_1
   POL(add0(x_1, x_2)) = [1] + x_1 + x_2
   POL(c2(x_1)) = x_1
   POL(c2(x_1, x_2)) = x_1 + x_2
   POL(c4) = 0
   POL(c4(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1)) = x_1
   POL(mult(x_1, x_2)) = [1] + x_2
   POL(power(x_1, x_2)) = [1] + x_1 + x_2

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

(114)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(z1))) -> c2(MULT(z0, mult(z0, power(z0, z1))), POWER(z0, S(z1)))
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   MULT(z0, S(0)) -> c4
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
K tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(0)) -> c4
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, POWER_2, MULT_2

Compound Symbols:   c6_1, c2_2, c2_1, c4_2, c4


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

(115) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace POWER(z0, S(S(z1))) -> c2(MULT(z0, mult(z0, power(z0, z1))), POWER(z0, S(z1))) by 
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))), POWER(z0, S(0)))

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

(116)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   MULT(z0, S(0)) -> c4
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))), POWER(z0, S(0)))
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
K tuples:
   POWER(z0, S(z1)) -> c2(MULT(z0, power(z0, z1)), POWER(z0, z1))
   MULT(z0, S(0)) -> c4
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, POWER_2, MULT_2

Compound Symbols:   c6_1, c2_1, c4_2, c4, c2_2


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

(117) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing nodes:
   MULT(z0, S(0)) -> c4
   POWER(z0, S(0)) -> c2(MULT(z0, S(0)))

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

(118)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))), POWER(z0, S(0)))
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, MULT_2, POWER_2

Compound Symbols:   c6_1, c4_2, c2_2


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

(119) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing tuple parts
----------------------------------------

(120)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1)))
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, MULT_2, POWER_2

Compound Symbols:   c6_1, c4_2, c2_2, c2_1


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

(121) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace MULT(z0, S(S(z1))) -> c4(ADD0(z0, add0(z0, mult(z0, z1))), MULT(z0, S(z1))) by 
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)), MULT(z0, S(0)))

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

(122)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)), MULT(z0, S(0)))
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)), MULT(z0, S(0)))
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, POWER_2, MULT_2

Compound Symbols:   c6_1, c2_2, c2_1, c4_2


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

(123) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing tuple parts
----------------------------------------

(124)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
K tuples:none
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, POWER_2, MULT_2

Compound Symbols:   c6_1, c2_2, c2_1, c4_2, c4_1


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

(125) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
We considered the (Usable) Rules:none
And the Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(+(x_1, x_2)) = x_1 + x_2
   POL(0) = 0
   POL(ADD0(x_1, x_2)) = 0
   POL(MULT(x_1, x_2)) = [1]
   POL(POWER(x_1, x_2)) = [1] + x_2
   POL(S(x_1)) = [1] + x_1
   POL(add0(x_1, x_2)) = [1] + x_2
   POL(c2(x_1)) = x_1
   POL(c2(x_1, x_2)) = x_1 + x_2
   POL(c4(x_1)) = x_1
   POL(c4(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1)) = x_1
   POL(mult(x_1, x_2)) = [1] + x_2
   POL(power(x_1, x_2)) = [1] + x_1 + x_2

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

(126)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
K tuples:
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, POWER_2, MULT_2

Compound Symbols:   c6_1, c2_2, c2_1, c4_2, c4_1


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

(127) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0))) by MULT(z0, S(S(0))) -> c4(ADD0(z0, z0))
----------------------------------------

(128)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, z0))
S tuples:
   ADD0(z0, S(z1)) -> c6(ADD0(z0, z1))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
K tuples:
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   ADD0_2, POWER_2, MULT_2

Compound Symbols:   c6_1, c2_2, c2_1, c4_2, c4_1


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

(129) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ADD0(z0, S(z1)) -> c6(ADD0(z0, z1)) by 
   ADD0(z0, S(S(y1))) -> c6(ADD0(z0, S(y1)))

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

(130)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(z0, S(S(0))) -> c4(ADD0(z0, z0))
   ADD0(z0, S(S(y1))) -> c6(ADD0(z0, S(y1)))
S tuples:
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   ADD0(z0, S(S(y1))) -> c6(ADD0(z0, S(y1)))
K tuples:
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   POWER_2, MULT_2, ADD0_2

Compound Symbols:   c2_2, c2_1, c4_2, c4_1, c6_1


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

(131) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace MULT(z0, S(S(0))) -> c4(ADD0(z0, z0)) by 
   MULT(S(S(y1)), S(S(0))) -> c4(ADD0(S(S(y1)), S(S(y1))))

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

(132)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   ADD0(z0, S(S(y1))) -> c6(ADD0(z0, S(y1)))
   MULT(S(S(y1)), S(S(0))) -> c4(ADD0(S(S(y1)), S(S(y1))))
S tuples:
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   ADD0(z0, S(S(y1))) -> c6(ADD0(z0, S(y1)))
K tuples:
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   POWER_2, MULT_2, ADD0_2

Compound Symbols:   c2_2, c2_1, c4_2, c6_1, c4_1


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

(133) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ADD0(z0, S(S(y1))) -> c6(ADD0(z0, S(y1))) by 
   ADD0(z0, S(S(S(y1)))) -> c6(ADD0(z0, S(S(y1))))

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

(134)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   MULT(S(S(y1)), S(S(0))) -> c4(ADD0(S(S(y1)), S(S(y1))))
   ADD0(z0, S(S(S(y1)))) -> c6(ADD0(z0, S(S(y1))))
S tuples:
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   ADD0(z0, S(S(S(y1)))) -> c6(ADD0(z0, S(S(y1))))
K tuples:
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   POWER_2, MULT_2, ADD0_2

Compound Symbols:   c2_2, c2_1, c4_2, c4_1, c6_1


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

(135) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace MULT(S(S(y1)), S(S(0))) -> c4(ADD0(S(S(y1)), S(S(y1)))) by 
   MULT(S(S(S(y1))), S(S(0))) -> c4(ADD0(S(S(S(y1))), S(S(S(y1)))))

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

(136)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   +(z0, S(0)) -> S(z0)
   +(S(0), z0) -> S(z0)
   power(z0, S(z1)) -> mult(z0, power(z0, z1))
   power(z0, 0) -> S(0)
   mult(z0, S(z1)) -> add0(z0, mult(z0, z1))
   mult(z0, 0) -> 0
   add0(z0, S(z1)) -> +(S(0), add0(z0, z1))
   add0(z0, 0) -> z0
Tuples:
   POWER(z0, S(S(S(z1)))) -> c2(MULT(z0, mult(z0, mult(z0, power(z0, z1)))), POWER(z0, S(S(z1))))
   POWER(z0, S(S(0))) -> c2(MULT(z0, mult(z0, S(0))))
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   ADD0(z0, S(S(S(y1)))) -> c6(ADD0(z0, S(S(y1))))
   MULT(S(S(S(y1))), S(S(0))) -> c4(ADD0(S(S(S(y1))), S(S(S(y1)))))
S tuples:
   MULT(z0, S(S(S(z1)))) -> c4(ADD0(z0, add0(z0, add0(z0, mult(z0, z1)))), MULT(z0, S(S(z1))))
   ADD0(z0, S(S(S(y1)))) -> c6(ADD0(z0, S(S(y1))))
K tuples:
   MULT(z0, S(S(0))) -> c4(ADD0(z0, add0(z0, 0)))
Defined Rule Symbols:   power_2, mult_2, add0_2, +_2

Defined Pair Symbols:   POWER_2, MULT_2, ADD0_2

Compound Symbols:   c2_2, c2_1, c4_2, c6_1, c4_1


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

(137) RelTrsToWeightedTrsProof (UPPER BOUND(ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(138)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x)) [1]
   mult(x', S(x)) -> add0(x', mult(x', x)) [1]
   add0(x', S(x)) -> +(S(0), add0(x', x)) [1]
   power(x, 0) -> S(0) [1]
   mult(x, 0) -> 0 [1]
   add0(x, 0) -> x [1]
   +(x, S(0)) -> S(x) [0]
   +(S(0), y) -> S(y) [0]

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

(139) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID))
Renamed defined symbols to avoid conflicts with arithmetic symbols:

+ => plus

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

(140)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x)) [1]
   mult(x', S(x)) -> add0(x', mult(x', x)) [1]
   add0(x', S(x)) -> plus(S(0), add0(x', x)) [1]
   power(x, 0) -> S(0) [1]
   mult(x, 0) -> 0 [1]
   add0(x, 0) -> x [1]
   plus(x, S(0)) -> S(x) [0]
   plus(S(0), y) -> S(y) [0]

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

(141) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(142)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x)) [1]
   mult(x', S(x)) -> add0(x', mult(x', x)) [1]
   add0(x', S(x)) -> plus(S(0), add0(x', x)) [1]
   power(x, 0) -> S(0) [1]
   mult(x, 0) -> 0 [1]
   add0(x, 0) -> x [1]
   plus(x, S(0)) -> S(x) [0]
   plus(S(0), y) -> S(y) [0]

The TRS has the following type information:
power :: S:0 -> S:0 -> S:0
S :: S:0 -> S:0
mult :: S:0 -> S:0 -> S:0
add0 :: S:0 -> S:0 -> S:0
plus :: S:0 -> S:0 -> S:0
0 :: S:0

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

(143) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
none

(c) The following functions are completely defined:

   power_2
   mult_2
   add0_2
   plus_2

Due to the following rules being added:

   plus(v0, v1) -> 0 [0]

And the following fresh constants: none

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

(144)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x)) [1]
   mult(x', S(x)) -> add0(x', mult(x', x)) [1]
   add0(x', S(x)) -> plus(S(0), add0(x', x)) [1]
   power(x, 0) -> S(0) [1]
   mult(x, 0) -> 0 [1]
   add0(x, 0) -> x [1]
   plus(x, S(0)) -> S(x) [0]
   plus(S(0), y) -> S(y) [0]
   plus(v0, v1) -> 0 [0]

The TRS has the following type information:
power :: S:0 -> S:0 -> S:0
S :: S:0 -> S:0
mult :: S:0 -> S:0 -> S:0
add0 :: S:0 -> S:0 -> S:0
plus :: S:0 -> S:0 -> S:0
0 :: S:0

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

(145) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(146)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   power(x', S(S(x1))) -> mult(x', mult(x', power(x', x1))) [2]
   power(x', S(0)) -> mult(x', S(0)) [2]
   mult(x', S(S(x2))) -> add0(x', add0(x', mult(x', x2))) [2]
   mult(x', S(0)) -> add0(x', 0) [2]
   add0(x', S(S(x3))) -> plus(S(0), plus(S(0), add0(x', x3))) [2]
   add0(x', S(0)) -> plus(S(0), x') [2]
   power(x, 0) -> S(0) [1]
   mult(x, 0) -> 0 [1]
   add0(x, 0) -> x [1]
   plus(x, S(0)) -> S(x) [0]
   plus(S(0), y) -> S(y) [0]
   plus(v0, v1) -> 0 [0]

The TRS has the following type information:
power :: S:0 -> S:0 -> S:0
S :: S:0 -> S:0
mult :: S:0 -> S:0 -> S:0
add0 :: S:0 -> S:0 -> S:0
plus :: S:0 -> S:0 -> S:0
0 :: S:0

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

(147) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   0 => 0

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

(148)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> x :|: x >= 0, z = x, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, x') :|: x' >= 0, z' = 1 + 0, z = x'
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(x', x3))) :|: z' = 1 + (1 + x3), x' >= 0, x3 >= 0, z = x'
   mult(z, z') -{ 2 }-> add0(x', add0(x', mult(x', x2))) :|: z' = 1 + (1 + x2), x' >= 0, x2 >= 0, z = x'
   mult(z, z') -{ 2 }-> add0(x', 0) :|: x' >= 0, z' = 1 + 0, z = x'
   mult(z, z') -{ 1 }-> 0 :|: x >= 0, z = x, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + x :|: x >= 0, z' = 1 + 0, z = x
   plus(z, z') -{ 0 }-> 1 + y :|: z = 1 + 0, y >= 0, z' = y
   power(z, z') -{ 2 }-> mult(x', mult(x', power(x', x1))) :|: x1 >= 0, z' = 1 + (1 + x1), x' >= 0, z = x'
   power(z, z') -{ 2 }-> mult(x', 1 + 0) :|: x' >= 0, z' = 1 + 0, z = x'
   power(z, z') -{ 1 }-> 1 + 0 :|: x >= 0, z = x, z' = 0


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

(149) InliningProof (UPPER BOUND(ID))
Inlined the following terminating rules on right-hand sides where appropriate:

   plus(z, z') -{ 0 }-> 1 + x :|: x >= 0, z' = 1 + 0, z = x
   plus(z, z') -{ 0 }-> 1 + y :|: z = 1 + 0, y >= 0, z' = y
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

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

(150)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> x :|: x >= 0, z = x, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(x', x3))) :|: z' = 1 + (1 + x3), x' >= 0, x3 >= 0, z = x'
   add0(z, z') -{ 2 }-> 0 :|: x' >= 0, z' = 1 + 0, z = x', v0 >= 0, v1 >= 0, 1 + 0 = v0, x' = v1
   add0(z, z') -{ 2 }-> 1 + x :|: x' >= 0, z' = 1 + 0, z = x', x >= 0, x' = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + y :|: x' >= 0, z' = 1 + 0, z = x', 1 + 0 = 1 + 0, y >= 0, x' = y
   mult(z, z') -{ 2 }-> add0(x', add0(x', mult(x', x2))) :|: z' = 1 + (1 + x2), x' >= 0, x2 >= 0, z = x'
   mult(z, z') -{ 2 }-> add0(x', 0) :|: x' >= 0, z' = 1 + 0, z = x'
   mult(z, z') -{ 1 }-> 0 :|: x >= 0, z = x, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + x :|: x >= 0, z' = 1 + 0, z = x
   plus(z, z') -{ 0 }-> 1 + y :|: z = 1 + 0, y >= 0, z' = y
   power(z, z') -{ 2 }-> mult(x', mult(x', power(x', x1))) :|: x1 >= 0, z' = 1 + (1 + x1), x' >= 0, z = x'
   power(z, z') -{ 2 }-> mult(x', 1 + 0) :|: x' >= 0, z' = 1 + 0, z = x'
   power(z, z') -{ 1 }-> 1 + 0 :|: x >= 0, z = x, z' = 0


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

(151) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(152)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 2 }-> add0(z, 0) :|: z >= 0, z' = 1 + 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0


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

(153) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { plus }
   { add0 }
   { mult }
   { power }

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

(154)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 2 }-> add0(z, 0) :|: z >= 0, z' = 1 + 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {plus}, {add0}, {mult}, {power}

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

(155) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(156)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 2 }-> add0(z, 0) :|: z >= 0, z' = 1 + 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {plus}, {add0}, {mult}, {power}

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

(157) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: plus
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z + z'

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

(158)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 2 }-> add0(z, 0) :|: z >= 0, z' = 1 + 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {plus}, {add0}, {mult}, {power}
Previous analysis results are:
  plus: runtime: ?, size: O(n^1) [z + z']

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

(159) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: plus
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(160)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 2 }-> add0(z, 0) :|: z >= 0, z' = 1 + 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {add0}, {mult}, {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']

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

(161) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(162)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 2 }-> add0(z, 0) :|: z >= 0, z' = 1 + 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {add0}, {mult}, {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']

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

(163) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: add0
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z + z'

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

(164)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 2 }-> add0(z, 0) :|: z >= 0, z' = 1 + 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {add0}, {mult}, {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: ?, size: O(n^1) [z + z']

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

(165) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: add0
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 4 + 2*z'

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

(166)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> plus(1 + 0, plus(1 + 0, add0(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 2 }-> add0(z, 0) :|: z >= 0, z' = 1 + 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {mult}, {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(n^1) [4 + 2*z'], size: O(n^1) [z + z']

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

(167) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(168)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 2 + 2*z' }-> s1 :|: s' >= 0, s' <= z + (z' - 2), s'' >= 0, s'' <= 1 + 0 + s', s1 >= 0, s1 <= 1 + 0 + s'', z >= 0, z' - 2 >= 0
   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 6 }-> s :|: s >= 0, s <= z + 0, z >= 0, z' = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {mult}, {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(n^1) [4 + 2*z'], size: O(n^1) [z + z']

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

(169) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: mult
after applying outer abstraction to obtain an ITS,
resulting in: O(n^2) with polynomial bound: z + 2*z*z'

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

(170)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 2 + 2*z' }-> s1 :|: s' >= 0, s' <= z + (z' - 2), s'' >= 0, s'' <= 1 + 0 + s', s1 >= 0, s1 <= 1 + 0 + s'', z >= 0, z' - 2 >= 0
   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 6 }-> s :|: s >= 0, s <= z + 0, z >= 0, z' = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {mult}, {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(n^1) [4 + 2*z'], size: O(n^1) [z + z']
  mult: runtime: ?, size: O(n^2) [z + 2*z*z']

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

(171) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: mult
after applying outer abstraction to obtain an ITS,
resulting in: O(n^3) with polynomial bound: 7 + 8*z*z'^2 + 10*z'

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

(172)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 2 + 2*z' }-> s1 :|: s' >= 0, s' <= z + (z' - 2), s'' >= 0, s'' <= 1 + 0 + s', s1 >= 0, s1 <= 1 + 0 + s'', z >= 0, z' - 2 >= 0
   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 6 }-> s :|: s >= 0, s <= z + 0, z >= 0, z' = 1 + 0
   mult(z, z') -{ 2 }-> add0(z, add0(z, mult(z, z' - 2))) :|: z >= 0, z' - 2 >= 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 2 }-> mult(z, 1 + 0) :|: z >= 0, z' = 1 + 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(n^1) [4 + 2*z'], size: O(n^1) [z + z']
  mult: runtime: O(n^3) [7 + 8*z*z'^2 + 10*z'], size: O(n^2) [z + 2*z*z']

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

(173) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(174)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 2 + 2*z' }-> s1 :|: s' >= 0, s' <= z + (z' - 2), s'' >= 0, s'' <= 1 + 0 + s', s1 >= 0, s1 <= 1 + 0 + s'', z >= 0, z' - 2 >= 0
   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 6 }-> s :|: s >= 0, s <= z + 0, z >= 0, z' = 1 + 0
   mult(z, z') -{ -3 + 2*s3 + 2*s4 + 32*z + -32*z*z' + 8*z*z'^2 + 10*z' }-> s5 :|: s3 >= 0, s3 <= 2 * ((z' - 2) * z) + z, s4 >= 0, s4 <= z + s3, s5 >= 0, s5 <= z + s4, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 19 + 8*z }-> s2 :|: s2 >= 0, s2 <= 2 * ((1 + 0) * z) + z, z >= 0, z' = 1 + 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(n^1) [4 + 2*z'], size: O(n^1) [z + z']
  mult: runtime: O(n^3) [7 + 8*z*z'^2 + 10*z'], size: O(n^2) [z + 2*z*z']

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

(175) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: power
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

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

(176)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 2 + 2*z' }-> s1 :|: s' >= 0, s' <= z + (z' - 2), s'' >= 0, s'' <= 1 + 0 + s', s1 >= 0, s1 <= 1 + 0 + s'', z >= 0, z' - 2 >= 0
   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 6 }-> s :|: s >= 0, s <= z + 0, z >= 0, z' = 1 + 0
   mult(z, z') -{ -3 + 2*s3 + 2*s4 + 32*z + -32*z*z' + 8*z*z'^2 + 10*z' }-> s5 :|: s3 >= 0, s3 <= 2 * ((z' - 2) * z) + z, s4 >= 0, s4 <= z + s3, s5 >= 0, s5 <= z + s4, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 19 + 8*z }-> s2 :|: s2 >= 0, s2 <= 2 * ((1 + 0) * z) + z, z >= 0, z' = 1 + 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(n^1) [4 + 2*z'], size: O(n^1) [z + z']
  mult: runtime: O(n^3) [7 + 8*z*z'^2 + 10*z'], size: O(n^2) [z + 2*z*z']
  power: runtime: ?, size: INF

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

(177) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: power
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

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

(178)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 2 + 2*z' }-> s1 :|: s' >= 0, s' <= z + (z' - 2), s'' >= 0, s'' <= 1 + 0 + s', s1 >= 0, s1 <= 1 + 0 + s'', z >= 0, z' - 2 >= 0
   add0(z, z') -{ 1 }-> z :|: z >= 0, z' = 0
   add0(z, z') -{ 2 }-> 0 :|: z >= 0, z' = 1 + 0, v0 >= 0, 1 + 0 = v0
   add0(z, z') -{ 2 }-> 1 + x :|: z >= 0, z' = 1 + 0, x >= 0, z = 1 + 0, 1 + 0 = x
   add0(z, z') -{ 2 }-> 1 + z :|: z >= 0, z' = 1 + 0, 1 + 0 = 1 + 0
   mult(z, z') -{ 6 }-> s :|: s >= 0, s <= z + 0, z >= 0, z' = 1 + 0
   mult(z, z') -{ -3 + 2*s3 + 2*s4 + 32*z + -32*z*z' + 8*z*z'^2 + 10*z' }-> s5 :|: s3 >= 0, s3 <= 2 * ((z' - 2) * z) + z, s4 >= 0, s4 <= z + s3, s5 >= 0, s5 <= z + s4, z >= 0, z' - 2 >= 0
   mult(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   plus(z, z') -{ 0 }-> 1 + z :|: z >= 0, z' = 1 + 0
   plus(z, z') -{ 0 }-> 1 + z' :|: z = 1 + 0, z' >= 0
   power(z, z') -{ 19 + 8*z }-> s2 :|: s2 >= 0, s2 <= 2 * ((1 + 0) * z) + z, z >= 0, z' = 1 + 0
   power(z, z') -{ 2 }-> mult(z, mult(z, power(z, z' - 2))) :|: z' - 2 >= 0, z >= 0
   power(z, z') -{ 1 }-> 1 + 0 :|: z >= 0, z' = 0

Function symbols to be analyzed: {power}
Previous analysis results are:
  plus: runtime: O(1) [0], size: O(n^1) [z + z']
  add0: runtime: O(n^1) [4 + 2*z'], size: O(n^1) [z + z']
  mult: runtime: O(n^3) [7 + 8*z*z'^2 + 10*z'], size: O(n^2) [z + 2*z*z']
  power: runtime: INF, size: INF

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

(179) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   plus(v0, v1) -> null_plus [0]
   power(v0, v1) -> null_power [0]
   mult(v0, v1) -> null_mult [0]
   add0(v0, v1) -> null_add0 [0]

And the following fresh constants:    null_plus, null_power, null_mult, null_add0

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

(180)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   power(x', S(x)) -> mult(x', power(x', x)) [1]
   mult(x', S(x)) -> add0(x', mult(x', x)) [1]
   add0(x', S(x)) -> plus(S(0), add0(x', x)) [1]
   power(x, 0) -> S(0) [1]
   mult(x, 0) -> 0 [1]
   add0(x, 0) -> x [1]
   plus(x, S(0)) -> S(x) [0]
   plus(S(0), y) -> S(y) [0]
   plus(v0, v1) -> null_plus [0]
   power(v0, v1) -> null_power [0]
   mult(v0, v1) -> null_mult [0]
   add0(v0, v1) -> null_add0 [0]

The TRS has the following type information:
power :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
S :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
mult :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
add0 :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
plus :: S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0 -> S:0:null_plus:null_power:null_mult:null_add0
0 :: S:0:null_plus:null_power:null_mult:null_add0
null_plus :: S:0:null_plus:null_power:null_mult:null_add0
null_power :: S:0:null_plus:null_power:null_mult:null_add0
null_mult :: S:0:null_plus:null_power:null_mult:null_add0
null_add0 :: S:0:null_plus:null_power:null_mult:null_add0

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

(181) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   0 => 0
   null_plus => 0
   null_power => 0
   null_mult => 0
   null_add0 => 0

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

(182)
Obligation:
Complexity RNTS consisting of the following rules:

   add0(z, z') -{ 1 }-> x :|: x >= 0, z = x, z' = 0
   add0(z, z') -{ 1 }-> plus(1 + 0, add0(x', x)) :|: z' = 1 + x, x' >= 0, x >= 0, z = x'
   add0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   mult(z, z') -{ 1 }-> add0(x', mult(x', x)) :|: z' = 1 + x, x' >= 0, x >= 0, z = x'
   mult(z, z') -{ 1 }-> 0 :|: x >= 0, z = x, z' = 0
   mult(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   plus(z, z') -{ 0 }-> 1 + x :|: x >= 0, z' = 1 + 0, z = x
   plus(z, z') -{ 0 }-> 1 + y :|: z = 1 + 0, y >= 0, z' = y
   power(z, z') -{ 1 }-> mult(x', power(x', x)) :|: z' = 1 + x, x' >= 0, x >= 0, z = x'
   power(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   power(z, z') -{ 1 }-> 1 + 0 :|: x >= 0, z = x, z' = 0

Only complete derivations are relevant for the runtime complexity.