WORST_CASE(Omega(n^1),O(n^1))
proof of input_ecmXzHc3oJ.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 411 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (10) CdtProblem
    (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CdtProblem
    (13) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxRelTRS
    (15) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CpxWeightedTrs
    (17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) CpxTypedWeightedTrs
    (19) CompletionProof [UPPER BOUND(ID), 0 ms]
    (20) CpxTypedWeightedCompleteTrs
    (21) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (22) CpxRNTS
    (23) CompleteCoflocoProof [FINISHED, 605 ms]
    (24) BOUNDS(1, n^1)
(25) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 17 ms]
(26) CdtProblem
    (27) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) CpxRelTRS
    (29) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (30) CpxRelTRS
    (31) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (32) typed CpxTrs
    (33) OrderProof [LOWER BOUND(ID), 5 ms]
    (34) typed CpxTrs
    (35) RewriteLemmaProof [LOWER BOUND(ID), 11.1 s]
    (36) BEST
        (37) proven lower bound
            (38) LowerBoundPropagationProof [FINISHED, 0 ms]
            (39) BOUNDS(n^1, INF)
        (40) typed CpxTrs


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

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


The TRS R consists of the following rules:

   *(@x, @y) -> #mult(@x, @y)
   dyade(@l1, @l2) -> dyade#1(@l1, @l2)
   dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2))
   dyade#1(nil, @l2) -> nil
   mult(@n, @l) -> mult#1(@l, @n)
   mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs))
   mult#1(nil, @n) -> nil

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

   #add(#0, @y) -> @y
   #add(#neg(#s(#0)), @y) -> #pred(@y)
   #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
   #add(#pos(#s(#0)), @y) -> #succ(@y)
   #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(@y)) -> #0
   #mult(#0, #pos(@y)) -> #0
   #mult(#neg(@x), #0) -> #0
   #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
   #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
   #mult(#pos(@x), #0) -> #0
   #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
   #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
   #natmult(#0, @y) -> #0
   #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
   #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))

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


The TRS R consists of the following rules:

   *(@x, @y) -> #mult(@x, @y)
   dyade(@l1, @l2) -> dyade#1(@l1, @l2)
   dyade#1(::(@x, @xs), @l2) -> ::(mult(@x, @l2), dyade(@xs, @l2))
   dyade#1(nil, @l2) -> nil
   mult(@n, @l) -> mult#1(@l, @n)
   mult#1(::(@x, @xs), @n) -> ::(*(@n, @x), mult(@n, @xs))
   mult#1(nil, @n) -> nil

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

   #add(#0, @y) -> @y
   #add(#neg(#s(#0)), @y) -> #pred(@y)
   #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
   #add(#pos(#s(#0)), @y) -> #succ(@y)
   #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(@y)) -> #0
   #mult(#0, #pos(@y)) -> #0
   #mult(#neg(@x), #0) -> #0
   #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
   #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
   #mult(#pos(@x), #0) -> #0
   #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
   #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
   #natmult(#0, @y) -> #0
   #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
   #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   #add(#0, z0) -> z0
   #add(#neg(#s(#0)), z0) -> #pred(z0)
   #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(z0)) -> #0
   #mult(#0, #pos(z0)) -> #0
   #mult(#neg(z0), #0) -> #0
   #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
   #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #0) -> #0
   #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
   *(z0, z1) -> #mult(z0, z1)
   dyade(z0, z1) -> dyade#1(z0, z1)
   dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
   dyade#1(nil, z0) -> nil
   mult(z0, z1) -> mult#1(z1, z0)
   mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1))
   mult#1(nil, z0) -> nil
Tuples:
   #ADD(#0, z0) -> c
   #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
   #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #MULT(#0, #0) -> c5
   #MULT(#0, #neg(z0)) -> c6
   #MULT(#0, #pos(z0)) -> c7
   #MULT(#neg(z0), #0) -> c8
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #0) -> c11
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#0, z0) -> c14
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   #PRED(#0) -> c16
   #PRED(#neg(#s(z0))) -> c17
   #PRED(#pos(#s(#0))) -> c18
   #PRED(#pos(#s(#s(z0)))) -> c19
   #SUCC(#0) -> c20
   #SUCC(#neg(#s(#0))) -> c21
   #SUCC(#neg(#s(#s(z0)))) -> c22
   #SUCC(#pos(#s(z0))) -> c23
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   DYADE#1(nil, z0) -> c28
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   MULT#1(nil, z0) -> c32
S tuples:
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   DYADE#1(nil, z0) -> c28
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   MULT#1(nil, z0) -> c32
K tuples:none
Defined Rule Symbols:   *_2, dyade_2, dyade#1_2, mult_2, mult#1_2, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1

Defined Pair Symbols:   #ADD_2, #MULT_2, #NATMULT_2, #PRED_1, #SUCC_1, *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2

Compound Symbols:   c, c1_1, c2_2, c3_1, c4_2, c5, c6, c7, c8, c9_1, c10_1, c11, c12_1, c13_1, c14, c15_2, c16, c17, c18, c19, c20, c21, c22, c23, c24_1, c25_1, c26_1, c27_1, c28, c29_1, c30_1, c31_1, c32


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 19 trailing nodes:
   DYADE#1(nil, z0) -> c28
   #MULT(#pos(z0), #0) -> c11
   #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
   #PRED(#pos(#s(#s(z0)))) -> c19
   #SUCC(#pos(#s(z0))) -> c23
   MULT#1(nil, z0) -> c32
   #MULT(#0, #pos(z0)) -> c7
   #SUCC(#neg(#s(#0))) -> c21
   #PRED(#pos(#s(#0))) -> c18
   #MULT(#neg(z0), #0) -> c8
   #SUCC(#neg(#s(#s(z0)))) -> c22
   #ADD(#0, z0) -> c
   #NATMULT(#0, z0) -> c14
   #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
   #MULT(#0, #0) -> c5
   #SUCC(#0) -> c20
   #PRED(#0) -> c16
   #MULT(#0, #neg(z0)) -> c6
   #PRED(#neg(#s(z0))) -> c17

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   #add(#0, z0) -> z0
   #add(#neg(#s(#0)), z0) -> #pred(z0)
   #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(z0)) -> #0
   #mult(#0, #pos(z0)) -> #0
   #mult(#neg(z0), #0) -> #0
   #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
   #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #0) -> #0
   #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
   *(z0, z1) -> #mult(z0, z1)
   dyade(z0, z1) -> dyade#1(z0, z1)
   dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
   dyade#1(nil, z0) -> nil
   mult(z0, z1) -> mult#1(z1, z0)
   mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1))
   mult#1(nil, z0) -> nil
Tuples:
   #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
S tuples:
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
K tuples:none
Defined Rule Symbols:   *_2, dyade_2, dyade#1_2, mult_2, mult#1_2, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1

Defined Pair Symbols:   #ADD_2, #MULT_2, #NATMULT_2, *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2

Compound Symbols:   c2_2, c4_2, c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1, c31_1


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

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   #add(#0, z0) -> z0
   #add(#neg(#s(#0)), z0) -> #pred(z0)
   #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(z0)) -> #0
   #mult(#0, #pos(z0)) -> #0
   #mult(#neg(z0), #0) -> #0
   #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
   #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #0) -> #0
   #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
   *(z0, z1) -> #mult(z0, z1)
   dyade(z0, z1) -> dyade#1(z0, z1)
   dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
   dyade#1(nil, z0) -> nil
   mult(z0, z1) -> mult#1(z1, z0)
   mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1))
   mult#1(nil, z0) -> nil
Tuples:
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1))
S tuples:
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
K tuples:none
Defined Rule Symbols:   *_2, dyade_2, dyade#1_2, mult_2, mult#1_2, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1

Defined Pair Symbols:   #MULT_2, #NATMULT_2, *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2, #ADD_2

Compound Symbols:   c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1, c31_1, c2_1, c4_1


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

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1))

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   #add(#0, z0) -> z0
   #add(#neg(#s(#0)), z0) -> #pred(z0)
   #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(z0)) -> #0
   #mult(#0, #pos(z0)) -> #0
   #mult(#neg(z0), #0) -> #0
   #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
   #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #0) -> #0
   #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
   *(z0, z1) -> #mult(z0, z1)
   dyade(z0, z1) -> dyade#1(z0, z1)
   dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
   dyade#1(nil, z0) -> nil
   mult(z0, z1) -> mult#1(z1, z0)
   mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1))
   mult#1(nil, z0) -> nil
Tuples:
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1))
S tuples:
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
K tuples:none
Defined Rule Symbols:   *_2, dyade_2, dyade#1_2, mult_2, mult#1_2, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1

Defined Pair Symbols:   #MULT_2, #NATMULT_2, *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2, #ADD_2

Compound Symbols:   c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1, c31_1, c4_1


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

(11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   #add(#0, z0) -> z0
   #add(#neg(#s(#0)), z0) -> #pred(z0)
   #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(z0)) -> #0
   #mult(#0, #pos(z0)) -> #0
   #mult(#neg(z0), #0) -> #0
   #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
   #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #0) -> #0
   #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
   *(z0, z1) -> #mult(z0, z1)
   dyade(z0, z1) -> dyade#1(z0, z1)
   dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
   dyade#1(nil, z0) -> nil
   mult(z0, z1) -> mult#1(z1, z0)
   mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1))
   mult#1(nil, z0) -> nil

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
Tuples:
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1))
S tuples:
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
K tuples:none
Defined Rule Symbols:   #natmult_2, #add_2, #succ_1

Defined Pair Symbols:   #MULT_2, #NATMULT_2, *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2, #ADD_2

Compound Symbols:   c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_1, c30_1, c31_1, c4_1


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

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

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


The TRS R consists of the following rules:

   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))

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

   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1))
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))

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

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

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


The TRS R consists of the following rules:

   *'(z0, z1) -> c24(#MULT(z0, z1)) [1]
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) [1]
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) [1]
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) [1]
   MULT(z0, z1) -> c29(MULT#1(z1, z0)) [1]
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) [1]
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) [1]
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) [0]
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) [0]
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) [0]
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) [0]
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) [0]
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) [0]
   #natmult(#0, z0) -> #0 [0]
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) [0]
   #add(#pos(#s(#0)), z0) -> #succ(z0) [0]
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) [0]
   #succ(#0) -> #pos(#s(#0)) [0]
   #succ(#neg(#s(#0))) -> #0 [0]
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) [0]
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) [0]

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

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

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

   *'(z0, z1) -> c24(#MULT(z0, z1)) [1]
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) [1]
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) [1]
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) [1]
   MULT(z0, z1) -> c29(MULT#1(z1, z0)) [1]
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) [1]
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) [1]
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) [0]
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) [0]
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) [0]
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) [0]
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) [0]
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) [0]
   #natmult(#0, z0) -> #0 [0]
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) [0]
   #add(#pos(#s(#0)), z0) -> #succ(z0) [0]
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) [0]
   #succ(#0) -> #pos(#s(#0)) [0]
   #succ(#neg(#s(#0))) -> #0 [0]
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) [0]
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) [0]

The TRS has the following type information:
*' :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0 -> c24
c24 :: c9:c10:c12:c13 -> c24
#MULT :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0 -> c9:c10:c12:c13
DYADE :: :: -> :: -> c25
c25 :: c26:c27 -> c25
DYADE#1 :: :: -> :: -> c26:c27
:: :: #neg:#pos:#s:#0 -> :: -> ::
c26 :: c29 -> c26:c27
MULT :: #neg:#pos:#s:#0 -> :: -> c29
c27 :: c25 -> c26:c27
c29 :: c30:c31 -> c29
MULT#1 :: :: -> #neg:#pos:#s:#0 -> c30:c31
c30 :: c24 -> c30:c31
c31 :: c29 -> c30:c31
#neg :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0
c9 :: c15 -> c9:c10:c12:c13
#NATMULT :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0 -> c15
#pos :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0
c10 :: c15 -> c9:c10:c12:c13
c12 :: c15 -> c9:c10:c12:c13
c13 :: c15 -> c9:c10:c12:c13
#s :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0
c15 :: c4 -> c15 -> c15
#ADD :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0 -> c4
#natmult :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0 -> #neg:#pos:#s:#0
c4 :: c4 -> c4
#0 :: #neg:#pos:#s:#0
#add :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0 -> #neg:#pos:#s:#0
#succ :: #neg:#pos:#s:#0 -> #neg:#pos:#s:#0

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

(19) 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:

   #MULT(v0, v1) -> null_#MULT [0]
   #NATMULT(v0, v1) -> null_#NATMULT [0]
   #ADD(v0, v1) -> null_#ADD [0]
   #natmult(v0, v1) -> null_#natmult [0]
   #add(v0, v1) -> null_#add [0]
   #succ(v0) -> null_#succ [0]
   DYADE#1(v0, v1) -> null_DYADE#1 [0]
   MULT#1(v0, v1) -> null_MULT#1 [0]

And the following fresh constants:    null_#MULT, null_#NATMULT, null_#ADD, null_#natmult, null_#add, null_#succ, null_DYADE#1, null_MULT#1, const, const1, const2, const3

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

(20)
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:

   *'(z0, z1) -> c24(#MULT(z0, z1)) [1]
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1)) [1]
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2)) [1]
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2)) [1]
   MULT(z0, z1) -> c29(MULT#1(z1, z0)) [1]
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0)) [1]
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1)) [1]
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) [0]
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) [0]
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) [0]
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) [0]
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) [0]
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) [0]
   #natmult(#0, z0) -> #0 [0]
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) [0]
   #add(#pos(#s(#0)), z0) -> #succ(z0) [0]
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) [0]
   #succ(#0) -> #pos(#s(#0)) [0]
   #succ(#neg(#s(#0))) -> #0 [0]
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) [0]
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) [0]
   #MULT(v0, v1) -> null_#MULT [0]
   #NATMULT(v0, v1) -> null_#NATMULT [0]
   #ADD(v0, v1) -> null_#ADD [0]
   #natmult(v0, v1) -> null_#natmult [0]
   #add(v0, v1) -> null_#add [0]
   #succ(v0) -> null_#succ [0]
   DYADE#1(v0, v1) -> null_DYADE#1 [0]
   MULT#1(v0, v1) -> null_MULT#1 [0]

The TRS has the following type information:
*' :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> c24
c24 :: c9:c10:c12:c13:null_#MULT -> c24
#MULT :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> c9:c10:c12:c13:null_#MULT
DYADE :: :: -> :: -> c25
c25 :: c26:c27:null_DYADE#1 -> c25
DYADE#1 :: :: -> :: -> c26:c27:null_DYADE#1
:: :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> :: -> ::
c26 :: c29 -> c26:c27:null_DYADE#1
MULT :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> :: -> c29
c27 :: c25 -> c26:c27:null_DYADE#1
c29 :: c30:c31:null_MULT#1 -> c29
MULT#1 :: :: -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> c30:c31:null_MULT#1
c30 :: c24 -> c30:c31:null_MULT#1
c31 :: c29 -> c30:c31:null_MULT#1
#neg :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
c9 :: c15:null_#NATMULT -> c9:c10:c12:c13:null_#MULT
#NATMULT :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> c15:null_#NATMULT
#pos :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
c10 :: c15:null_#NATMULT -> c9:c10:c12:c13:null_#MULT
c12 :: c15:null_#NATMULT -> c9:c10:c12:c13:null_#MULT
c13 :: c15:null_#NATMULT -> c9:c10:c12:c13:null_#MULT
#s :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
c15 :: c4:null_#ADD -> c15:null_#NATMULT -> c15:null_#NATMULT
#ADD :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> c4:null_#ADD
#natmult :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
c4 :: c4:null_#ADD -> c4:null_#ADD
#0 :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
#add :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
#succ :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ -> #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
null_#MULT :: c9:c10:c12:c13:null_#MULT
null_#NATMULT :: c15:null_#NATMULT
null_#ADD :: c4:null_#ADD
null_#natmult :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
null_#add :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
null_#succ :: #neg:#pos:#s:#0:null_#natmult:null_#add:null_#succ
null_DYADE#1 :: c26:c27:null_DYADE#1
null_MULT#1 :: c30:c31:null_MULT#1
const :: c24
const1 :: c25
const2 :: ::
const3 :: c29

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

(21) 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_#MULT => 0
   null_#NATMULT => 0
   null_#ADD => 0
   null_#natmult => 0
   null_#add => 0
   null_#succ => 0
   null_DYADE#1 => 0
   null_MULT#1 => 0
   const => 0
   const1 => 0
   const2 => 0
   const3 => 0

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

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

   #ADD(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   #ADD(z, z') -{ 0 }-> 1 + #ADD(1 + (1 + z0), z1) :|: z1 >= 0, z' = z1, z0 >= 0, z = 1 + (1 + (1 + z0))
   #MULT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   #MULT(z, z') -{ 0 }-> 1 + #NATMULT(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   #NATMULT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   #NATMULT(z, z') -{ 0 }-> 1 + #ADD(1 + z1, #natmult(z0, z1)) + #NATMULT(z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   #add(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   #add(z, z') -{ 0 }-> #succ(z0) :|: z = 1 + (1 + 0), z0 >= 0, z' = z0
   #add(z, z') -{ 0 }-> #succ(#add(1 + (1 + z0), z1)) :|: z1 >= 0, z' = z1, z0 >= 0, z = 1 + (1 + (1 + z0))
   #natmult(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   #natmult(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   #natmult(z, z') -{ 0 }-> #add(1 + z1, #natmult(z0, z1)) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   #succ(z) -{ 0 }-> 0 :|: z = 1 + (1 + 0)
   #succ(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   #succ(z) -{ 0 }-> 1 + (1 + z0) :|: z0 >= 0, z = 1 + (1 + (1 + z0))
   #succ(z) -{ 0 }-> 1 + (1 + 0) :|: z = 0
   #succ(z) -{ 0 }-> 1 + (1 + (1 + z0)) :|: z0 >= 0, z = 1 + (1 + z0)
   *'(z, z') -{ 1 }-> 1 + #MULT(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   DYADE(z, z') -{ 1 }-> 1 + DYADE#1(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   DYADE#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   DYADE#1(z, z') -{ 1 }-> 1 + MULT(z0, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   DYADE#1(z, z') -{ 1 }-> 1 + DYADE(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   MULT(z, z') -{ 1 }-> 1 + MULT#1(z1, z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   MULT#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MULT#1(z, z') -{ 1 }-> 1 + MULT(z2, z1) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   MULT#1(z, z') -{ 1 }-> 1 + *'(z2, z0) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0

Only complete derivations are relevant for the runtime complexity.

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

(23) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V1, V),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun2(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun4(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun5(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun6(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun7(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun8(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun9(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun10(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[fun1(V3, V2, Ret1)],[Out = 1 + Ret1,V1 = V3,V2 >= 0,V = V2,V3 >= 0]).
eq(fun2(V1, V, Out),1,[fun3(V5, V4, Ret11)],[Out = 1 + Ret11,V1 = V5,V4 >= 0,V = V4,V5 >= 0]).
eq(fun3(V1, V, Out),1,[fun4(V7, V8, Ret12)],[Out = 1 + Ret12,V6 >= 0,V = V8,V7 >= 0,V1 = 1 + V6 + V7,V8 >= 0]).
eq(fun3(V1, V, Out),1,[fun2(V11, V10, Ret13)],[Out = 1 + Ret13,V11 >= 0,V = V10,V9 >= 0,V1 = 1 + V11 + V9,V10 >= 0]).
eq(fun4(V1, V, Out),1,[fun5(V12, V13, Ret14)],[Out = 1 + Ret14,V1 = V13,V12 >= 0,V = V12,V13 >= 0]).
eq(fun5(V1, V, Out),1,[fun(V16, V15, Ret15)],[Out = 1 + Ret15,V14 >= 0,V = V16,V15 >= 0,V1 = 1 + V14 + V15,V16 >= 0]).
eq(fun5(V1, V, Out),1,[fun4(V19, V17, Ret16)],[Out = 1 + Ret16,V17 >= 0,V = V19,V18 >= 0,V1 = 1 + V17 + V18,V19 >= 0]).
eq(fun1(V1, V, Out),0,[fun6(V21, V20, Ret17)],[Out = 1 + Ret17,V20 >= 0,V1 = 1 + V21,V21 >= 0,V = 1 + V20]).
eq(fun6(V1, V, Out),0,[fun8(V23, V22, Ret011),fun7(1 + V22, Ret011, Ret01),fun6(V23, V22, Ret18)],[Out = 1 + Ret01 + Ret18,V22 >= 0,V1 = 1 + V23,V = V22,V23 >= 0]).
eq(fun7(V1, V, Out),0,[fun7(1 + (1 + V24), V25, Ret19)],[Out = 1 + Ret19,V25 >= 0,V = V25,V24 >= 0,V1 = 3 + V24]).
eq(fun8(V1, V, Out),0,[],[Out = 0,V26 >= 0,V1 = 0,V = V26]).
eq(fun8(V1, V, Out),0,[fun8(V28, V27, Ret110),fun9(1 + V27, Ret110, Ret)],[Out = Ret,V27 >= 0,V1 = 1 + V28,V = V27,V28 >= 0]).
eq(fun9(V1, V, Out),0,[fun10(V29, Ret2)],[Out = Ret2,V1 = 2,V29 >= 0,V = V29]).
eq(fun9(V1, V, Out),0,[fun9(1 + (1 + V31), V30, Ret0),fun10(Ret0, Ret3)],[Out = Ret3,V30 >= 0,V = V30,V31 >= 0,V1 = 3 + V31]).
eq(fun10(V1, Out),0,[],[Out = 2,V1 = 0]).
eq(fun10(V1, Out),0,[],[Out = 0,V1 = 2]).
eq(fun10(V1, Out),0,[],[Out = 2 + V32,V32 >= 0,V1 = 3 + V32]).
eq(fun10(V1, Out),0,[],[Out = 3 + V33,V33 >= 0,V1 = 2 + V33]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V35 >= 0,V34 >= 0,V1 = V35,V = V34]).
eq(fun6(V1, V, Out),0,[],[Out = 0,V37 >= 0,V36 >= 0,V1 = V37,V = V36]).
eq(fun7(V1, V, Out),0,[],[Out = 0,V39 >= 0,V38 >= 0,V1 = V39,V = V38]).
eq(fun8(V1, V, Out),0,[],[Out = 0,V40 >= 0,V41 >= 0,V1 = V40,V = V41]).
eq(fun9(V1, V, Out),0,[],[Out = 0,V43 >= 0,V42 >= 0,V1 = V43,V = V42]).
eq(fun10(V1, Out),0,[],[Out = 0,V44 >= 0,V1 = V44]).
eq(fun3(V1, V, Out),0,[],[Out = 0,V46 >= 0,V45 >= 0,V1 = V46,V = V45]).
eq(fun5(V1, V, Out),0,[],[Out = 0,V47 >= 0,V48 >= 0,V1 = V47,V = V48]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun4(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun5(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun6(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun7(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun8(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun9(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun10(V1,Out),[V1],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [fun7/3]
1. non_recursive  : [fun10/2]
2. recursive [non_tail] : [fun9/3]
3. recursive [non_tail] : [fun8/3]
4. recursive  : [fun6/3]
5. non_recursive  : [fun1/3]
6. non_recursive  : [fun/3]
7. recursive  : [fun4/3,fun5/3]
8. recursive  : [fun2/3,fun3/3]
9. non_recursive  : [start/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun7/3
1. SCC is partially evaluated into fun10/2
2. SCC is partially evaluated into fun9/3
3. SCC is partially evaluated into fun8/3
4. SCC is partially evaluated into fun6/3
5. SCC is partially evaluated into fun1/3
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into fun4/3
8. SCC is partially evaluated into fun3/3
9. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations fun7/3 
* CE 25 is refined into CE [35] 
* CE 24 is refined into CE [36] 


### Cost equations --> "Loop" of fun7/3 
* CEs [36] --> Loop 23 
* CEs [35] --> Loop 24 

### Ranking functions of CR fun7(V1,V,Out) 
* RF of phase [23]: [V1-2]

#### Partial ranking functions of CR fun7(V1,V,Out) 
* Partial RF of phase [23]:
  - RF of loop [23:1]:
    V1-2


### Specialization of cost equations fun10/2 
* CE 33 is refined into CE [37] 
* CE 34 is refined into CE [38] 
* CE 32 is refined into CE [39] 
* CE 31 is refined into CE [40] 


### Cost equations --> "Loop" of fun10/2 
* CEs [37] --> Loop 25 
* CEs [38] --> Loop 26 
* CEs [39] --> Loop 27 
* CEs [40] --> Loop 28 

### Ranking functions of CR fun10(V1,Out) 

#### Partial ranking functions of CR fun10(V1,Out) 


### Specialization of cost equations fun9/3 
* CE 30 is refined into CE [41] 
* CE 28 is refined into CE [42,43,44,45] 
* CE 29 is refined into CE [46,47,48,49] 


### Cost equations --> "Loop" of fun9/3 
* CEs [48] --> Loop 29 
* CEs [49] --> Loop 30 
* CEs [46] --> Loop 31 
* CEs [47] --> Loop 32 
* CEs [45] --> Loop 33 
* CEs [44] --> Loop 34 
* CEs [41,43] --> Loop 35 
* CEs [42] --> Loop 36 

### Ranking functions of CR fun9(V1,V,Out) 
* RF of phase [29,30,31,32]: [V1-2]

#### Partial ranking functions of CR fun9(V1,V,Out) 
* Partial RF of phase [29,30,31,32]:
  - RF of loop [29:1,30:1,31:1,32:1]:
    V1-2


### Specialization of cost equations fun8/3 
* CE 26 is refined into CE [50] 
* CE 27 is refined into CE [51,52,53,54,55,56,57] 


### Cost equations --> "Loop" of fun8/3 
* CEs [57] --> Loop 37 
* CEs [56] --> Loop 38 
* CEs [54] --> Loop 39 
* CEs [55] --> Loop 40 
* CEs [52] --> Loop 41 
* CEs [53] --> Loop 42 
* CEs [51] --> Loop 43 
* CEs [50] --> Loop 44 

### Ranking functions of CR fun8(V1,V,Out) 
* RF of phase [37,38,39,40,41,42,43]: [V1]

#### Partial ranking functions of CR fun8(V1,V,Out) 
* Partial RF of phase [37,38,39,40,41,42,43]:
  - RF of loop [37:1,38:1,39:1,40:1,41:1,42:1,43:1]:
    V1


### Specialization of cost equations fun6/3 
* CE 23 is refined into CE [58] 
* CE 22 is refined into CE [59,60,61,62] 


### Cost equations --> "Loop" of fun6/3 
* CEs [60,62] --> Loop 45 
* CEs [59,61] --> Loop 46 
* CEs [58] --> Loop 47 

### Ranking functions of CR fun6(V1,V,Out) 
* RF of phase [45,46]: [V1]

#### Partial ranking functions of CR fun6(V1,V,Out) 
* Partial RF of phase [45,46]:
  - RF of loop [45:1,46:1]:
    V1


### Specialization of cost equations fun1/3 
* CE 20 is refined into CE [63,64] 
* CE 21 is refined into CE [65] 


### Cost equations --> "Loop" of fun1/3 
* CEs [64] --> Loop 48 
* CEs [63] --> Loop 49 
* CEs [65] --> Loop 50 

### Ranking functions of CR fun1(V1,V,Out) 

#### Partial ranking functions of CR fun1(V1,V,Out) 


### Specialization of cost equations fun4/3 
* CE 19 is refined into CE [66,67,68] 
* CE 17 is refined into CE [69] 
* CE 18 is refined into CE [70] 


### Cost equations --> "Loop" of fun4/3 
* CEs [70] --> Loop 51 
* CEs [68] --> Loop 52 
* CEs [67] --> Loop 53 
* CEs [66] --> Loop 54 
* CEs [69] --> Loop 55 

### Ranking functions of CR fun4(V1,V,Out) 
* RF of phase [51]: [V]

#### Partial ranking functions of CR fun4(V1,V,Out) 
* Partial RF of phase [51]:
  - RF of loop [51:1]:
    V


### Specialization of cost equations fun3/3 
* CE 15 is refined into CE [71,72,73,74] 
* CE 16 is refined into CE [75] 
* CE 14 is refined into CE [76] 


### Cost equations --> "Loop" of fun3/3 
* CEs [76] --> Loop 56 
* CEs [74] --> Loop 57 
* CEs [72,73] --> Loop 58 
* CEs [71] --> Loop 59 
* CEs [75] --> Loop 60 

### Ranking functions of CR fun3(V1,V,Out) 
* RF of phase [56]: [V1]

#### Partial ranking functions of CR fun3(V1,V,Out) 
* Partial RF of phase [56]:
  - RF of loop [56:1]:
    V1


### Specialization of cost equations start/2 
* CE 1 is refined into CE [77,78,79,80,81] 
* CE 2 is refined into CE [82] 
* CE 3 is refined into CE [83,84,85,86] 
* CE 4 is refined into CE [87,88,89] 
* CE 5 is refined into CE [90,91,92] 
* CE 6 is refined into CE [93,94,95,96,97] 
* CE 7 is refined into CE [98,99,100,101] 
* CE 8 is refined into CE [102,103,104] 
* CE 9 is refined into CE [105,106] 
* CE 10 is refined into CE [107,108] 
* CE 11 is refined into CE [109,110] 
* CE 12 is refined into CE [111,112,113,114,115,116,117] 
* CE 13 is refined into CE [118,119,120,121] 


### Cost equations --> "Loop" of start/2 
* CEs [114] --> Loop 61 
* CEs [112,113] --> Loop 62 
* CEs [111] --> Loop 63 
* CEs [77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,115,116,117,118,119,120,121] --> Loop 64 

### Ranking functions of CR start(V1,V) 

#### Partial ranking functions of CR start(V1,V) 


Computing Bounds
=====================================

#### Cost of chains of fun7(V1,V,Out):
* Chain [[23],24]: 0
  with precondition: [V>=0,Out>=1,V1>=Out+2] 

* Chain [24]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun10(V1,Out):
* Chain [28]: 0
  with precondition: [V1=0,Out=2] 

* Chain [27]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [26]: 0
  with precondition: [V1+1=Out,V1>=2] 

* Chain [25]: 0
  with precondition: [V1=Out+1,V1>=3] 


#### Cost of chains of fun9(V1,V,Out):
* Chain [[29,30,31,32],36]: 0
  with precondition: [V=0,V1>=3,Out>=0,V1>=Out] 

* Chain [[29,30,31,32],35]: 0
  with precondition: [V1>=3,V>=0,Out>=0,V1>=Out+1] 

* Chain [[29,30,31,32],34]: 0
  with precondition: [V1>=3,V>=2,Out>=0,V+V1>=Out+1] 

* Chain [[29,30,31,32],33]: 0
  with precondition: [V1>=3,V>=3,Out>=0,V+V1>=Out+3] 

* Chain [36]: 0
  with precondition: [V1=2,V=0,Out=2] 

* Chain [35]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [34]: 0
  with precondition: [V1=2,V+1=Out,V>=2] 

* Chain [33]: 0
  with precondition: [V1=2,V=Out+1,V>=3] 


#### Cost of chains of fun8(V1,V,Out):
* Chain [[37,38,39,40,41,42,43],44]: 0
  with precondition: [V1>=1,V>=0,Out>=0] 

* Chain [44]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun6(V1,V,Out):
* Chain [[45,46],47]: 0
  with precondition: [V1>=1,V>=0,Out>=1] 

* Chain [47]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun1(V1,V,Out):
* Chain [50]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [49]: 0
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [48]: 0
  with precondition: [V1>=2,V>=1,Out>=2] 


#### Cost of chains of fun4(V1,V,Out):
* Chain [[51],55]: 2*it(51)+1
  Such that:it(51) =< V

  with precondition: [V1>=0,Out>=3,2*V+1>=Out] 

* Chain [[51],54]: 2*it(51)+3
  Such that:it(51) =< V

  with precondition: [V1>=0,Out>=5,2*V+1>=Out] 

* Chain [[51],53]: 2*it(51)+3
  Such that:it(51) =< V

  with precondition: [V1>=1,Out>=6,2*V>=Out] 

* Chain [[51],52]: 2*it(51)+3
  Such that:it(51) =< V

  with precondition: [V1>=2,V>=3,Out>=7] 

* Chain [55]: 1
  with precondition: [Out=1,V1>=0,V>=0] 

* Chain [54]: 3
  with precondition: [Out=3,V1>=0,V>=1] 

* Chain [53]: 3
  with precondition: [Out=4,V1>=1,V>=2] 

* Chain [52]: 3
  with precondition: [V1>=2,V>=2,Out>=5] 


#### Cost of chains of fun3(V1,V,Out):
* Chain [[56],60]: 2*it(56)+0
  Such that:it(56) =< V1

  with precondition: [V>=0,Out>=2,2*V1>=Out] 

* Chain [[56],59]: 2*it(56)+2
  Such that:it(56) =< V1

  with precondition: [V>=0,Out>=4,2*V1>=Out] 

* Chain [[56],58]: 2*it(56)+6*s(6)+4
  Such that:it(56) =< V1
s(5) =< V
s(6) =< s(5)

  with precondition: [V1>=2,V>=1,Out>=6,2*V+2*V1>=Out] 

* Chain [[56],57]: 2*it(56)+2*s(7)+4
  Such that:it(56) =< V1
s(7) =< V

  with precondition: [V1>=4,V>=2,Out>=8] 

* Chain [60]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [59]: 2
  with precondition: [Out=2,V1>=1,V>=0] 

* Chain [58]: 6*s(6)+4
  Such that:s(5) =< V
s(6) =< s(5)

  with precondition: [V1>=1,Out>=4,2*V+2>=Out] 

* Chain [57]: 2*s(7)+4
  Such that:s(7) =< V

  with precondition: [V1>=3,V>=2,Out>=6] 


#### Cost of chains of start(V1,V):
* Chain [64]: 24*s(14)+40*s(16)+5
  Such that:aux(10) =< V1
aux(11) =< V
s(14) =< aux(10)
s(16) =< aux(11)

  with precondition: [V1>=0] 

* Chain [63]: 0
  with precondition: [V1=2,V=0] 

* Chain [62]: 0
  with precondition: [V1=2,V>=2] 

* Chain [61]: 0
  with precondition: [V=0,V1>=3] 


Closed-form bounds of start(V1,V): 
-------------------------------------
* Chain [64] with precondition: [V1>=0] 
    - Upper bound: 24*V1+5+nat(V)*40 
    - Complexity: n 
* Chain [63] with precondition: [V1=2,V=0] 
    - Upper bound: 0 
    - Complexity: constant 
* Chain [62] with precondition: [V1=2,V>=2] 
    - Upper bound: 0 
    - Complexity: constant 
* Chain [61] with precondition: [V=0,V1>=3] 
    - Upper bound: 0 
    - Complexity: constant 

### Maximum cost of start(V1,V): 24*V1+5+nat(V)*40 
Asymptotic class: n 
* Total analysis performed in 600 ms.


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

(24)
BOUNDS(1, n^1)

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

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

(26)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   #add(#0, z0) -> z0
   #add(#neg(#s(#0)), z0) -> #pred(z0)
   #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(z0)) -> #0
   #mult(#0, #pos(z0)) -> #0
   #mult(#neg(z0), #0) -> #0
   #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
   #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #0) -> #0
   #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
   *(z0, z1) -> #mult(z0, z1)
   dyade(z0, z1) -> dyade#1(z0, z1)
   dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
   dyade#1(nil, z0) -> nil
   mult(z0, z1) -> mult#1(z1, z0)
   mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1))
   mult#1(nil, z0) -> nil
Tuples:
   #ADD(#0, z0) -> c
   #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
   #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #MULT(#0, #0) -> c5
   #MULT(#0, #neg(z0)) -> c6
   #MULT(#0, #pos(z0)) -> c7
   #MULT(#neg(z0), #0) -> c8
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #0) -> c11
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#0, z0) -> c14
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   #PRED(#0) -> c16
   #PRED(#neg(#s(z0))) -> c17
   #PRED(#pos(#s(#0))) -> c18
   #PRED(#pos(#s(#s(z0)))) -> c19
   #SUCC(#0) -> c20
   #SUCC(#neg(#s(#0))) -> c21
   #SUCC(#neg(#s(#s(z0)))) -> c22
   #SUCC(#pos(#s(z0))) -> c23
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   DYADE#1(nil, z0) -> c28
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   MULT#1(nil, z0) -> c32
S tuples:
   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   DYADE#1(nil, z0) -> c28
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   MULT#1(nil, z0) -> c32
K tuples:none
Defined Rule Symbols:   *_2, dyade_2, dyade#1_2, mult_2, mult#1_2, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1

Defined Pair Symbols:   #ADD_2, #MULT_2, #NATMULT_2, #PRED_1, #SUCC_1, *'_2, DYADE_2, DYADE#1_2, MULT_2, MULT#1_2

Compound Symbols:   c, c1_1, c2_2, c3_1, c4_2, c5, c6, c7, c8, c9_1, c10_1, c11, c12_1, c13_1, c14, c15_2, c16, c17, c18, c19, c20, c21, c22, c23, c24_1, c25_1, c26_1, c27_1, c28, c29_1, c30_1, c31_1, c32


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

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

(28)
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:

   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   DYADE#1(nil, z0) -> c28
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   MULT#1(nil, z0) -> c32

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

   #ADD(#0, z0) -> c
   #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
   #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #MULT(#0, #0) -> c5
   #MULT(#0, #neg(z0)) -> c6
   #MULT(#0, #pos(z0)) -> c7
   #MULT(#neg(z0), #0) -> c8
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #0) -> c11
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#0, z0) -> c14
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   #PRED(#0) -> c16
   #PRED(#neg(#s(z0))) -> c17
   #PRED(#pos(#s(#0))) -> c18
   #PRED(#pos(#s(#s(z0)))) -> c19
   #SUCC(#0) -> c20
   #SUCC(#neg(#s(#0))) -> c21
   #SUCC(#neg(#s(#s(z0)))) -> c22
   #SUCC(#pos(#s(z0))) -> c23
   #add(#0, z0) -> z0
   #add(#neg(#s(#0)), z0) -> #pred(z0)
   #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(z0)) -> #0
   #mult(#0, #pos(z0)) -> #0
   #mult(#neg(z0), #0) -> #0
   #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
   #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #0) -> #0
   #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
   *(z0, z1) -> #mult(z0, z1)
   dyade(z0, z1) -> dyade#1(z0, z1)
   dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
   dyade#1(nil, z0) -> nil
   mult(z0, z1) -> mult#1(z1, z0)
   mult#1(::(z0, z1), z2) -> ::(*(z2, z0), mult(z2, z1))
   mult#1(nil, z0) -> nil

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

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

(30)
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:

   *'(z0, z1) -> c24(#MULT(z0, z1))
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   DYADE#1(nil, z0) -> c28
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   MULT#1(nil, z0) -> c32

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

   #ADD(#0, z0) -> c
   #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
   #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
   #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
   #MULT(#0, #0) -> c5
   #MULT(#0, #neg(z0)) -> c6
   #MULT(#0, #pos(z0)) -> c7
   #MULT(#neg(z0), #0) -> c8
   #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
   #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
   #MULT(#pos(z0), #0) -> c11
   #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
   #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
   #NATMULT(#0, z0) -> c14
   #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
   #PRED(#0) -> c16
   #PRED(#neg(#s(z0))) -> c17
   #PRED(#pos(#s(#0))) -> c18
   #PRED(#pos(#s(#s(z0)))) -> c19
   #SUCC(#0) -> c20
   #SUCC(#neg(#s(#0))) -> c21
   #SUCC(#neg(#s(#s(z0)))) -> c22
   #SUCC(#pos(#s(z0))) -> c23
   #add(#0, z0) -> z0
   #add(#neg(#s(#0)), z0) -> #pred(z0)
   #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
   #add(#pos(#s(#0)), z0) -> #succ(z0)
   #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
   #mult(#0, #0) -> #0
   #mult(#0, #neg(z0)) -> #0
   #mult(#0, #pos(z0)) -> #0
   #mult(#neg(z0), #0) -> #0
   #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
   #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #0) -> #0
   #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
   #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
   #natmult(#0, z0) -> #0
   #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
   #pred(#0) -> #neg(#s(#0))
   #pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
   #pred(#pos(#s(#0))) -> #0
   #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
   #succ(#0) -> #pos(#s(#0))
   #succ(#neg(#s(#0))) -> #0
   #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
   #succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
   *'(z0, z1) -> #mult(z0, z1)
   dyade(z0, z1) -> dyade#1(z0, z1)
   dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
   dyade#1(nil, z0) -> nil
   mult(z0, z1) -> mult#1(z1, z0)
   mult#1(::(z0, z1), z2) -> ::(*'(z2, z0), mult(z2, z1))
   mult#1(nil, z0) -> nil

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

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

(32)
Obligation:
Innermost TRS:
Rules:
*'(z0, z1) -> c24(#MULT(z0, z1))
DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
DYADE#1(nil, z0) -> c28
MULT(z0, z1) -> c29(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
MULT#1(nil, z0) -> c32
#ADD(#0, z0) -> c
#ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
#ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
#ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#MULT(#0, #0) -> c5
#MULT(#0, #neg(z0)) -> c6
#MULT(#0, #pos(z0)) -> c7
#MULT(#neg(z0), #0) -> c8
#MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
#MULT(#pos(z0), #0) -> c11
#MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
#NATMULT(#0, z0) -> c14
#NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#PRED(#0) -> c16
#PRED(#neg(#s(z0))) -> c17
#PRED(#pos(#s(#0))) -> c18
#PRED(#pos(#s(#s(z0)))) -> c19
#SUCC(#0) -> c20
#SUCC(#neg(#s(#0))) -> c21
#SUCC(#neg(#s(#s(z0)))) -> c22
#SUCC(#pos(#s(z0))) -> c23
#add(#0, z0) -> z0
#add(#neg(#s(#0)), z0) -> #pred(z0)
#add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) -> #succ(z0)
#add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
#mult(#0, #0) -> #0
#mult(#0, #neg(z0)) -> #0
#mult(#0, #pos(z0)) -> #0
#mult(#neg(z0), #0) -> #0
#mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) -> #0
#mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
#natmult(#0, z0) -> #0
#natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
#pred(#0) -> #neg(#s(#0))
#pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) -> #0
#pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
#succ(#0) -> #pos(#s(#0))
#succ(#neg(#s(#0))) -> #0
#succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
#succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
*'(z0, z1) -> #mult(z0, z1)
dyade(z0, z1) -> dyade#1(z0, z1)
dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
dyade#1(nil, z0) -> nil
mult(z0, z1) -> mult#1(z1, z0)
mult#1(::(z0, z1), z2) -> ::(*'(z2, z0), mult(z2, z1))
mult#1(nil, z0) -> nil

Types:
*' :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c24 :: c5:c6:c7:c8:c9:c10:c11:c12:c13 -> c24::::nil:#0:#s:#neg:#pos
#MULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c5:c6:c7:c8:c9:c10:c11:c12:c13
DYADE :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c25
c25 :: c26:c27:c28 -> c25
DYADE#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c26:c27:c28
:: :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c26 :: c29 -> c26:c27:c28
MULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c29
c27 :: c25 -> c26:c27:c28
nil :: c24::::nil:#0:#s:#neg:#pos
c28 :: c26:c27:c28
c29 :: c30:c31:c32 -> c29
MULT#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c30:c31:c32
c30 :: c24::::nil:#0:#s:#neg:#pos -> c30:c31:c32
c31 :: c29 -> c30:c31:c32
c32 :: c30:c31:c32
#ADD :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c:c1:c2:c3:c4
#0 :: c24::::nil:#0:#s:#neg:#pos
c :: c:c1:c2:c3:c4
#neg :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#s :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c1 :: c16:c17:c18:c19 -> c:c1:c2:c3:c4
#PRED :: c24::::nil:#0:#s:#neg:#pos -> c16:c17:c18:c19
c2 :: c16:c17:c18:c19 -> c:c1:c2:c3:c4 -> c:c1:c2:c3:c4
#add :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#pos :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c3 :: c20:c21:c22:c23 -> c:c1:c2:c3:c4
#SUCC :: c24::::nil:#0:#s:#neg:#pos -> c20:c21:c22:c23
c4 :: c20:c21:c22:c23 -> c:c1:c2:c3:c4 -> c:c1:c2:c3:c4
c5 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c6 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c7 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c8 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c9 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
#NATMULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c14:c15
c10 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c11 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c12 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c13 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c14 :: c14:c15
c15 :: c:c1:c2:c3:c4 -> c14:c15 -> c14:c15
#natmult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19
c20 :: c20:c21:c22:c23
c21 :: c20:c21:c22:c23
c22 :: c20:c21:c22:c23
c23 :: c20:c21:c22:c23
#pred :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#succ :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#mult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
dyade :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
dyade#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
mult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
mult#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
hole_c24::::nil:#0:#s:#neg:#pos1_33 :: c24::::nil:#0:#s:#neg:#pos
hole_c5:c6:c7:c8:c9:c10:c11:c12:c132_33 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
hole_c253_33 :: c25
hole_c26:c27:c284_33 :: c26:c27:c28
hole_c295_33 :: c29
hole_c30:c31:c326_33 :: c30:c31:c32
hole_c:c1:c2:c3:c47_33 :: c:c1:c2:c3:c4
hole_c16:c17:c18:c198_33 :: c16:c17:c18:c19
hole_c20:c21:c22:c239_33 :: c20:c21:c22:c23
hole_c14:c1510_33 :: c14:c15
gen_c24::::nil:#0:#s:#neg:#pos11_33 :: Nat -> c24::::nil:#0:#s:#neg:#pos
gen_c:c1:c2:c3:c412_33 :: Nat -> c:c1:c2:c3:c4
gen_c14:c1513_33 :: Nat -> c14:c15

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

(33) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
DYADE, DYADE#1, MULT, MULT#1, #ADD, #add, #NATMULT, #natmult, dyade, dyade#1, mult, mult#1

They will be analysed ascendingly in the following order:
DYADE = DYADE#1
MULT < DYADE#1
MULT = MULT#1
#add < #ADD
#ADD < #NATMULT
#add < #natmult
#natmult < #NATMULT
dyade = dyade#1
mult < dyade#1
mult = mult#1

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

(34)
Obligation:
Innermost TRS:
Rules:
*'(z0, z1) -> c24(#MULT(z0, z1))
DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
DYADE#1(nil, z0) -> c28
MULT(z0, z1) -> c29(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
MULT#1(nil, z0) -> c32
#ADD(#0, z0) -> c
#ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
#ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
#ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#MULT(#0, #0) -> c5
#MULT(#0, #neg(z0)) -> c6
#MULT(#0, #pos(z0)) -> c7
#MULT(#neg(z0), #0) -> c8
#MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
#MULT(#pos(z0), #0) -> c11
#MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
#NATMULT(#0, z0) -> c14
#NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#PRED(#0) -> c16
#PRED(#neg(#s(z0))) -> c17
#PRED(#pos(#s(#0))) -> c18
#PRED(#pos(#s(#s(z0)))) -> c19
#SUCC(#0) -> c20
#SUCC(#neg(#s(#0))) -> c21
#SUCC(#neg(#s(#s(z0)))) -> c22
#SUCC(#pos(#s(z0))) -> c23
#add(#0, z0) -> z0
#add(#neg(#s(#0)), z0) -> #pred(z0)
#add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) -> #succ(z0)
#add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
#mult(#0, #0) -> #0
#mult(#0, #neg(z0)) -> #0
#mult(#0, #pos(z0)) -> #0
#mult(#neg(z0), #0) -> #0
#mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) -> #0
#mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
#natmult(#0, z0) -> #0
#natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
#pred(#0) -> #neg(#s(#0))
#pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) -> #0
#pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
#succ(#0) -> #pos(#s(#0))
#succ(#neg(#s(#0))) -> #0
#succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
#succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
*'(z0, z1) -> #mult(z0, z1)
dyade(z0, z1) -> dyade#1(z0, z1)
dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
dyade#1(nil, z0) -> nil
mult(z0, z1) -> mult#1(z1, z0)
mult#1(::(z0, z1), z2) -> ::(*'(z2, z0), mult(z2, z1))
mult#1(nil, z0) -> nil

Types:
*' :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c24 :: c5:c6:c7:c8:c9:c10:c11:c12:c13 -> c24::::nil:#0:#s:#neg:#pos
#MULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c5:c6:c7:c8:c9:c10:c11:c12:c13
DYADE :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c25
c25 :: c26:c27:c28 -> c25
DYADE#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c26:c27:c28
:: :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c26 :: c29 -> c26:c27:c28
MULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c29
c27 :: c25 -> c26:c27:c28
nil :: c24::::nil:#0:#s:#neg:#pos
c28 :: c26:c27:c28
c29 :: c30:c31:c32 -> c29
MULT#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c30:c31:c32
c30 :: c24::::nil:#0:#s:#neg:#pos -> c30:c31:c32
c31 :: c29 -> c30:c31:c32
c32 :: c30:c31:c32
#ADD :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c:c1:c2:c3:c4
#0 :: c24::::nil:#0:#s:#neg:#pos
c :: c:c1:c2:c3:c4
#neg :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#s :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c1 :: c16:c17:c18:c19 -> c:c1:c2:c3:c4
#PRED :: c24::::nil:#0:#s:#neg:#pos -> c16:c17:c18:c19
c2 :: c16:c17:c18:c19 -> c:c1:c2:c3:c4 -> c:c1:c2:c3:c4
#add :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#pos :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c3 :: c20:c21:c22:c23 -> c:c1:c2:c3:c4
#SUCC :: c24::::nil:#0:#s:#neg:#pos -> c20:c21:c22:c23
c4 :: c20:c21:c22:c23 -> c:c1:c2:c3:c4 -> c:c1:c2:c3:c4
c5 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c6 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c7 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c8 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c9 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
#NATMULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c14:c15
c10 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c11 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c12 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c13 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c14 :: c14:c15
c15 :: c:c1:c2:c3:c4 -> c14:c15 -> c14:c15
#natmult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19
c20 :: c20:c21:c22:c23
c21 :: c20:c21:c22:c23
c22 :: c20:c21:c22:c23
c23 :: c20:c21:c22:c23
#pred :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#succ :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#mult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
dyade :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
dyade#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
mult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
mult#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
hole_c24::::nil:#0:#s:#neg:#pos1_33 :: c24::::nil:#0:#s:#neg:#pos
hole_c5:c6:c7:c8:c9:c10:c11:c12:c132_33 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
hole_c253_33 :: c25
hole_c26:c27:c284_33 :: c26:c27:c28
hole_c295_33 :: c29
hole_c30:c31:c326_33 :: c30:c31:c32
hole_c:c1:c2:c3:c47_33 :: c:c1:c2:c3:c4
hole_c16:c17:c18:c198_33 :: c16:c17:c18:c19
hole_c20:c21:c22:c239_33 :: c20:c21:c22:c23
hole_c14:c1510_33 :: c14:c15
gen_c24::::nil:#0:#s:#neg:#pos11_33 :: Nat -> c24::::nil:#0:#s:#neg:#pos
gen_c:c1:c2:c3:c412_33 :: Nat -> c:c1:c2:c3:c4
gen_c14:c1513_33 :: Nat -> c14:c15


Generator Equations:
gen_c24::::nil:#0:#s:#neg:#pos11_33(0) <=> nil
gen_c24::::nil:#0:#s:#neg:#pos11_33(+(x, 1)) <=> ::(nil, gen_c24::::nil:#0:#s:#neg:#pos11_33(x))
gen_c:c1:c2:c3:c412_33(0) <=> c
gen_c:c1:c2:c3:c412_33(+(x, 1)) <=> c2(c16, gen_c:c1:c2:c3:c412_33(x))
gen_c14:c1513_33(0) <=> c14
gen_c14:c1513_33(+(x, 1)) <=> c15(c, gen_c14:c1513_33(x))


The following defined symbols remain to be analysed:
#add, DYADE, DYADE#1, MULT, MULT#1, #ADD, #NATMULT, #natmult, dyade, dyade#1, mult, mult#1

They will be analysed ascendingly in the following order:
DYADE = DYADE#1
MULT < DYADE#1
MULT = MULT#1
#add < #ADD
#ADD < #NATMULT
#add < #natmult
#natmult < #NATMULT
dyade = dyade#1
mult < dyade#1
mult = mult#1

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
mult#1(gen_c24::::nil:#0:#s:#neg:#pos11_33(+(1, n231_33)), gen_c24::::nil:#0:#s:#neg:#pos11_33(b)) -> *14_33, rt in Omega(n231_33)

Induction Base:
mult#1(gen_c24::::nil:#0:#s:#neg:#pos11_33(+(1, 0)), gen_c24::::nil:#0:#s:#neg:#pos11_33(b))

Induction Step:
mult#1(gen_c24::::nil:#0:#s:#neg:#pos11_33(+(1, +(n231_33, 1))), gen_c24::::nil:#0:#s:#neg:#pos11_33(b)) ->_R^Omega(0)
::(*'(gen_c24::::nil:#0:#s:#neg:#pos11_33(b), nil), mult(gen_c24::::nil:#0:#s:#neg:#pos11_33(b), gen_c24::::nil:#0:#s:#neg:#pos11_33(+(1, n231_33)))) ->_R^Omega(1)
::(c24(#MULT(gen_c24::::nil:#0:#s:#neg:#pos11_33(b), nil)), mult(gen_c24::::nil:#0:#s:#neg:#pos11_33(b), gen_c24::::nil:#0:#s:#neg:#pos11_33(+(1, n231_33)))) ->_R^Omega(0)
::(c24(#MULT(gen_c24::::nil:#0:#s:#neg:#pos11_33(b), nil)), mult#1(gen_c24::::nil:#0:#s:#neg:#pos11_33(+(1, n231_33)), gen_c24::::nil:#0:#s:#neg:#pos11_33(b))) ->_IH
::(c24(#MULT(gen_c24::::nil:#0:#s:#neg:#pos11_33(b), nil)), *14_33)

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

(36)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
*'(z0, z1) -> c24(#MULT(z0, z1))
DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
DYADE#1(nil, z0) -> c28
MULT(z0, z1) -> c29(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
MULT#1(nil, z0) -> c32
#ADD(#0, z0) -> c
#ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
#ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
#ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#MULT(#0, #0) -> c5
#MULT(#0, #neg(z0)) -> c6
#MULT(#0, #pos(z0)) -> c7
#MULT(#neg(z0), #0) -> c8
#MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
#MULT(#pos(z0), #0) -> c11
#MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
#NATMULT(#0, z0) -> c14
#NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#PRED(#0) -> c16
#PRED(#neg(#s(z0))) -> c17
#PRED(#pos(#s(#0))) -> c18
#PRED(#pos(#s(#s(z0)))) -> c19
#SUCC(#0) -> c20
#SUCC(#neg(#s(#0))) -> c21
#SUCC(#neg(#s(#s(z0)))) -> c22
#SUCC(#pos(#s(z0))) -> c23
#add(#0, z0) -> z0
#add(#neg(#s(#0)), z0) -> #pred(z0)
#add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) -> #succ(z0)
#add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
#mult(#0, #0) -> #0
#mult(#0, #neg(z0)) -> #0
#mult(#0, #pos(z0)) -> #0
#mult(#neg(z0), #0) -> #0
#mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) -> #0
#mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
#natmult(#0, z0) -> #0
#natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
#pred(#0) -> #neg(#s(#0))
#pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) -> #0
#pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
#succ(#0) -> #pos(#s(#0))
#succ(#neg(#s(#0))) -> #0
#succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
#succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
*'(z0, z1) -> #mult(z0, z1)
dyade(z0, z1) -> dyade#1(z0, z1)
dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
dyade#1(nil, z0) -> nil
mult(z0, z1) -> mult#1(z1, z0)
mult#1(::(z0, z1), z2) -> ::(*'(z2, z0), mult(z2, z1))
mult#1(nil, z0) -> nil

Types:
*' :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c24 :: c5:c6:c7:c8:c9:c10:c11:c12:c13 -> c24::::nil:#0:#s:#neg:#pos
#MULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c5:c6:c7:c8:c9:c10:c11:c12:c13
DYADE :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c25
c25 :: c26:c27:c28 -> c25
DYADE#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c26:c27:c28
:: :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c26 :: c29 -> c26:c27:c28
MULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c29
c27 :: c25 -> c26:c27:c28
nil :: c24::::nil:#0:#s:#neg:#pos
c28 :: c26:c27:c28
c29 :: c30:c31:c32 -> c29
MULT#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c30:c31:c32
c30 :: c24::::nil:#0:#s:#neg:#pos -> c30:c31:c32
c31 :: c29 -> c30:c31:c32
c32 :: c30:c31:c32
#ADD :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c:c1:c2:c3:c4
#0 :: c24::::nil:#0:#s:#neg:#pos
c :: c:c1:c2:c3:c4
#neg :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#s :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c1 :: c16:c17:c18:c19 -> c:c1:c2:c3:c4
#PRED :: c24::::nil:#0:#s:#neg:#pos -> c16:c17:c18:c19
c2 :: c16:c17:c18:c19 -> c:c1:c2:c3:c4 -> c:c1:c2:c3:c4
#add :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#pos :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c3 :: c20:c21:c22:c23 -> c:c1:c2:c3:c4
#SUCC :: c24::::nil:#0:#s:#neg:#pos -> c20:c21:c22:c23
c4 :: c20:c21:c22:c23 -> c:c1:c2:c3:c4 -> c:c1:c2:c3:c4
c5 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c6 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c7 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c8 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c9 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
#NATMULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c14:c15
c10 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c11 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c12 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c13 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c14 :: c14:c15
c15 :: c:c1:c2:c3:c4 -> c14:c15 -> c14:c15
#natmult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19
c20 :: c20:c21:c22:c23
c21 :: c20:c21:c22:c23
c22 :: c20:c21:c22:c23
c23 :: c20:c21:c22:c23
#pred :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#succ :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#mult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
dyade :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
dyade#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
mult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
mult#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
hole_c24::::nil:#0:#s:#neg:#pos1_33 :: c24::::nil:#0:#s:#neg:#pos
hole_c5:c6:c7:c8:c9:c10:c11:c12:c132_33 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
hole_c253_33 :: c25
hole_c26:c27:c284_33 :: c26:c27:c28
hole_c295_33 :: c29
hole_c30:c31:c326_33 :: c30:c31:c32
hole_c:c1:c2:c3:c47_33 :: c:c1:c2:c3:c4
hole_c16:c17:c18:c198_33 :: c16:c17:c18:c19
hole_c20:c21:c22:c239_33 :: c20:c21:c22:c23
hole_c14:c1510_33 :: c14:c15
gen_c24::::nil:#0:#s:#neg:#pos11_33 :: Nat -> c24::::nil:#0:#s:#neg:#pos
gen_c:c1:c2:c3:c412_33 :: Nat -> c:c1:c2:c3:c4
gen_c14:c1513_33 :: Nat -> c14:c15


Generator Equations:
gen_c24::::nil:#0:#s:#neg:#pos11_33(0) <=> nil
gen_c24::::nil:#0:#s:#neg:#pos11_33(+(x, 1)) <=> ::(nil, gen_c24::::nil:#0:#s:#neg:#pos11_33(x))
gen_c:c1:c2:c3:c412_33(0) <=> c
gen_c:c1:c2:c3:c412_33(+(x, 1)) <=> c2(c16, gen_c:c1:c2:c3:c412_33(x))
gen_c14:c1513_33(0) <=> c14
gen_c14:c1513_33(+(x, 1)) <=> c15(c, gen_c14:c1513_33(x))


The following defined symbols remain to be analysed:
mult#1, DYADE, DYADE#1, MULT, MULT#1, dyade, dyade#1, mult

They will be analysed ascendingly in the following order:
DYADE = DYADE#1
MULT < DYADE#1
MULT = MULT#1
dyade = dyade#1
mult < dyade#1
mult = mult#1

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

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

(39)
BOUNDS(n^1, INF)

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

(40)
Obligation:
Innermost TRS:
Rules:
*'(z0, z1) -> c24(#MULT(z0, z1))
DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
DYADE#1(nil, z0) -> c28
MULT(z0, z1) -> c29(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
MULT#1(nil, z0) -> c32
#ADD(#0, z0) -> c
#ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
#ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
#ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1))
#MULT(#0, #0) -> c5
#MULT(#0, #neg(z0)) -> c6
#MULT(#0, #pos(z0)) -> c7
#MULT(#neg(z0), #0) -> c8
#MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1))
#MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1))
#MULT(#pos(z0), #0) -> c11
#MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1))
#MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1))
#NATMULT(#0, z0) -> c14
#NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1))
#PRED(#0) -> c16
#PRED(#neg(#s(z0))) -> c17
#PRED(#pos(#s(#0))) -> c18
#PRED(#pos(#s(#s(z0)))) -> c19
#SUCC(#0) -> c20
#SUCC(#neg(#s(#0))) -> c21
#SUCC(#neg(#s(#s(z0)))) -> c22
#SUCC(#pos(#s(z0))) -> c23
#add(#0, z0) -> z0
#add(#neg(#s(#0)), z0) -> #pred(z0)
#add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1))
#add(#pos(#s(#0)), z0) -> #succ(z0)
#add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1))
#mult(#0, #0) -> #0
#mult(#0, #neg(z0)) -> #0
#mult(#0, #pos(z0)) -> #0
#mult(#neg(z0), #0) -> #0
#mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1))
#mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1))
#mult(#pos(z0), #0) -> #0
#mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1))
#mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1))
#natmult(#0, z0) -> #0
#natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1))
#pred(#0) -> #neg(#s(#0))
#pred(#neg(#s(z0))) -> #neg(#s(#s(z0)))
#pred(#pos(#s(#0))) -> #0
#pred(#pos(#s(#s(z0)))) -> #pos(#s(z0))
#succ(#0) -> #pos(#s(#0))
#succ(#neg(#s(#0))) -> #0
#succ(#neg(#s(#s(z0)))) -> #neg(#s(z0))
#succ(#pos(#s(z0))) -> #pos(#s(#s(z0)))
*'(z0, z1) -> #mult(z0, z1)
dyade(z0, z1) -> dyade#1(z0, z1)
dyade#1(::(z0, z1), z2) -> ::(mult(z0, z2), dyade(z1, z2))
dyade#1(nil, z0) -> nil
mult(z0, z1) -> mult#1(z1, z0)
mult#1(::(z0, z1), z2) -> ::(*'(z2, z0), mult(z2, z1))
mult#1(nil, z0) -> nil

Types:
*' :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c24 :: c5:c6:c7:c8:c9:c10:c11:c12:c13 -> c24::::nil:#0:#s:#neg:#pos
#MULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c5:c6:c7:c8:c9:c10:c11:c12:c13
DYADE :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c25
c25 :: c26:c27:c28 -> c25
DYADE#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c26:c27:c28
:: :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c26 :: c29 -> c26:c27:c28
MULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c29
c27 :: c25 -> c26:c27:c28
nil :: c24::::nil:#0:#s:#neg:#pos
c28 :: c26:c27:c28
c29 :: c30:c31:c32 -> c29
MULT#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c30:c31:c32
c30 :: c24::::nil:#0:#s:#neg:#pos -> c30:c31:c32
c31 :: c29 -> c30:c31:c32
c32 :: c30:c31:c32
#ADD :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c:c1:c2:c3:c4
#0 :: c24::::nil:#0:#s:#neg:#pos
c :: c:c1:c2:c3:c4
#neg :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#s :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c1 :: c16:c17:c18:c19 -> c:c1:c2:c3:c4
#PRED :: c24::::nil:#0:#s:#neg:#pos -> c16:c17:c18:c19
c2 :: c16:c17:c18:c19 -> c:c1:c2:c3:c4 -> c:c1:c2:c3:c4
#add :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#pos :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c3 :: c20:c21:c22:c23 -> c:c1:c2:c3:c4
#SUCC :: c24::::nil:#0:#s:#neg:#pos -> c20:c21:c22:c23
c4 :: c20:c21:c22:c23 -> c:c1:c2:c3:c4 -> c:c1:c2:c3:c4
c5 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c6 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c7 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c8 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c9 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
#NATMULT :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c14:c15
c10 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c11 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
c12 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c13 :: c14:c15 -> c5:c6:c7:c8:c9:c10:c11:c12:c13
c14 :: c14:c15
c15 :: c:c1:c2:c3:c4 -> c14:c15 -> c14:c15
#natmult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
c16 :: c16:c17:c18:c19
c17 :: c16:c17:c18:c19
c18 :: c16:c17:c18:c19
c19 :: c16:c17:c18:c19
c20 :: c20:c21:c22:c23
c21 :: c20:c21:c22:c23
c22 :: c20:c21:c22:c23
c23 :: c20:c21:c22:c23
#pred :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#succ :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
#mult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
dyade :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
dyade#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
mult :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
mult#1 :: c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos -> c24::::nil:#0:#s:#neg:#pos
hole_c24::::nil:#0:#s:#neg:#pos1_33 :: c24::::nil:#0:#s:#neg:#pos
hole_c5:c6:c7:c8:c9:c10:c11:c12:c132_33 :: c5:c6:c7:c8:c9:c10:c11:c12:c13
hole_c253_33 :: c25
hole_c26:c27:c284_33 :: c26:c27:c28
hole_c295_33 :: c29
hole_c30:c31:c326_33 :: c30:c31:c32
hole_c:c1:c2:c3:c47_33 :: c:c1:c2:c3:c4
hole_c16:c17:c18:c198_33 :: c16:c17:c18:c19
hole_c20:c21:c22:c239_33 :: c20:c21:c22:c23
hole_c14:c1510_33 :: c14:c15
gen_c24::::nil:#0:#s:#neg:#pos11_33 :: Nat -> c24::::nil:#0:#s:#neg:#pos
gen_c:c1:c2:c3:c412_33 :: Nat -> c:c1:c2:c3:c4
gen_c14:c1513_33 :: Nat -> c14:c15


Lemmas:
mult#1(gen_c24::::nil:#0:#s:#neg:#pos11_33(+(1, n231_33)), gen_c24::::nil:#0:#s:#neg:#pos11_33(b)) -> *14_33, rt in Omega(n231_33)


Generator Equations:
gen_c24::::nil:#0:#s:#neg:#pos11_33(0) <=> nil
gen_c24::::nil:#0:#s:#neg:#pos11_33(+(x, 1)) <=> ::(nil, gen_c24::::nil:#0:#s:#neg:#pos11_33(x))
gen_c:c1:c2:c3:c412_33(0) <=> c
gen_c:c1:c2:c3:c412_33(+(x, 1)) <=> c2(c16, gen_c:c1:c2:c3:c412_33(x))
gen_c14:c1513_33(0) <=> c14
gen_c14:c1513_33(+(x, 1)) <=> c15(c, gen_c14:c1513_33(x))


The following defined symbols remain to be analysed:
mult, DYADE, DYADE#1, MULT, MULT#1, dyade, dyade#1

They will be analysed ascendingly in the following order:
DYADE = DYADE#1
MULT < DYADE#1
MULT = MULT#1
dyade = dyade#1
mult < dyade#1
mult = mult#1