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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 423 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) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 69 ms]
(14) CdtProblem
(15) CdtKnowledgeProof [FINISHED, 0 ms]
(16) BOUNDS(1, 1)


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

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(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(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:
   #SUCC(#0) -> c20
   #MULT(#0, #neg(z0)) -> c6
   #PRED(#0) -> c16
   #MULT(#0, #pos(z0)) -> c7
   #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0))
   #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0))
   #MULT(#pos(z0), #0) -> c11
   MULT#1(nil, z0) -> c32
   #SUCC(#neg(#s(#s(z0)))) -> c22
   #PRED(#pos(#s(#s(z0)))) -> c19
   #SUCC(#neg(#s(#0))) -> c21
   #PRED(#pos(#s(#0))) -> c18
   #MULT(#neg(z0), #0) -> c8
   #MULT(#0, #0) -> c5
   #NATMULT(#0, z0) -> c14
   #ADD(#0, z0) -> c
   DYADE#1(nil, z0) -> c28
   #SUCC(#pos(#s(z0))) -> c23
   #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) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
We considered the (Usable) Rules:none
And the 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))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(#0) = [3]
   POL(#ADD(x_1, x_2)) = 0
   POL(#MULT(x_1, x_2)) = [1] + x_2
   POL(#NATMULT(x_1, x_2)) = [3]
   POL(#add(x_1, x_2)) = [3]
   POL(#natmult(x_1, x_2)) = [3] + [3]x_1 + [3]x_2
   POL(#neg(x_1)) = [3]
   POL(#pos(x_1)) = [3]
   POL(#s(x_1)) = 0
   POL(#succ(x_1)) = [3]
   POL(*'(x_1, x_2)) = [1] + x_2
   POL(::(x_1, x_2)) = [1] + x_1 + x_2
   POL(DYADE(x_1, x_2)) = [3] + x_1 + x_2
   POL(DYADE#1(x_1, x_2)) = [3] + x_1 + x_2
   POL(MULT(x_1, x_2)) = x_1 + x_2
   POL(MULT#1(x_1, x_2)) = x_1 + x_2
   POL(c10(x_1)) = x_1
   POL(c12(x_1)) = x_1
   POL(c13(x_1)) = x_1
   POL(c15(x_1, x_2)) = x_1 + x_2
   POL(c24(x_1)) = x_1
   POL(c25(x_1)) = x_1
   POL(c26(x_1)) = x_1
   POL(c27(x_1)) = x_1
   POL(c29(x_1)) = x_1
   POL(c30(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c9(x_1)) = x_1

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

(14)
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))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
K tuples:
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
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


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

(15) CdtKnowledgeProof (FINISHED)
The following tuples could be moved from S to K by knowledge propagation:
   DYADE(z0, z1) -> c25(DYADE#1(z0, z1))
   MULT(z0, z1) -> c29(MULT#1(z1, z0))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   DYADE#1(::(z0, z1), z2) -> c26(MULT(z0, z2))
   DYADE#1(::(z0, z1), z2) -> c27(DYADE(z1, z2))
   MULT#1(::(z0, z1), z2) -> c30(*'(z2, z0))
   MULT#1(::(z0, z1), z2) -> c31(MULT(z2, z1))
   *'(z0, z1) -> c24(#MULT(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))
Now S is empty
----------------------------------------

(16)
BOUNDS(1, 1)