Runtime Complexity (innermost) proof of /tmp/tmp8QPZDf/dyade.raml.xml

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

0 CpxRelTRS

↳1 CpxTrsToCdtProof (UPPER BOUND(ID), 0 ms)

↳2 CdtProblem

↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳8 CdtProblem

↳9 CdtUsableRulesProof (⇔, 0 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 247 ms)

↳12 CdtProblem

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 265 ms)

↳16 CdtProblem

↳17 CdtKnowledgeProof (⇔, 0 ms)

↳18 BOUNDS(1, 1)

(0) Obligation:

Runtime Complexity Relative TRS:
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: INNERMOST

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) 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(z1, z2))
DYADE#1(nil, z0) → c27
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))
MULT#1(nil, z0) → c30

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(z1, z2))
DYADE#1(nil, z0) → c27
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))
MULT#1(nil, z0) → c30

K tuples:none
Defined Rule Symbols:

*, dyade, dyade#1, mult, mult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#ADD, #MULT, #NATMULT, #PRED, #SUCC, *', DYADE, DYADE#1, MULT, MULT#1

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 19 trailing nodes:

#SUCC(#0) → c20
#MULT(#0, #0) → c5
#MULT(#neg(z0), #0) → c8
#MULT(#pos(z0), #0) → c11
#MULT(#0, #neg(z0)) → c6
#PRED(#neg(#s(z0))) → c17
#MULT(#0, #pos(z0)) → c7
#ADD(#pos(#s(#0)), z0) → c3(#SUCC(z0))
MULT#1(nil, z0) → c30
#PRED(#0) → c16
#PRED(#pos(#s(#s(z0)))) → c19
#PRED(#pos(#s(#0))) → c18
#ADD(#neg(#s(#0)), z0) → c1(#PRED(z0))
DYADE#1(nil, z0) → c27
#SUCC(#pos(#s(z0))) → c23
#SUCC(#neg(#s(#0))) → c21
#ADD(#0, z0) → c
#NATMULT(#0, z0) → c14
#SUCC(#neg(#s(#s(z0)))) → c22

(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(#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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), 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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))

K tuples:none
Defined Rule Symbols:

*, dyade, dyade#1, mult, mult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#ADD, #MULT, #NATMULT, *', DYADE, DYADE#1, MULT, MULT#1

Compound Symbols:

c2, c4, c9, c10, c12, c13, c15, c24, c25, c26, c28, c29

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

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

#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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), 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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))

K tuples:none
Defined Rule Symbols:

*, dyade, dyade#1, mult, mult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', DYADE, DYADE#1, MULT, MULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c28, c29, c2, c4

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1))

(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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), 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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))

K tuples:none
Defined Rule Symbols:

*, dyade, dyade#1, mult, mult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', DYADE, DYADE#1, MULT, MULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c28, c29, c4

(9) CdtUsableRulesProof (EQUIVALENT transformation)

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

(10) 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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), 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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))

K tuples:none
Defined Rule Symbols:

#natmult, #add, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', DYADE, DYADE#1, MULT, MULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c28, c29, c4

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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(z1, z2))

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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), 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) = [4]
POL(#ADD(x₁, x₂)) = 0
POL(#MULT(x₁, x₂)) = 0
POL(#NATMULT(x₁, x₂)) = 0
POL(#add(x₁, x₂)) = [4]
POL(#natmult(x₁, x₂)) = [2] + [2]x₁ + [5]x₂
POL(#neg(x₁)) = [3]
POL(#pos(x₁)) = [4]
POL(#s(x₁)) = [3] + x₁
POL(#succ(x₁)) = [4]
POL(*'(x₁, x₂)) = 0
POL(::(x₁, x₂)) = [3] + x₂
POL(DYADE(x₁, x₂)) = [2]x₁ + [4]x₂
POL(DYADE#1(x₁, x₂)) = [2]x₁ + [4]x₂
POL(MULT(x₁, x₂)) = [4]
POL(MULT#1(x₁, x₂)) = [4]
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c26(x₁, x₂)) = x₁ + x₂
POL(c28(x₁)) = x₁
POL(c29(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c9(x₁)) = x₁

(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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), 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) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))

K tuples:

DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2))

Defined Rule Symbols:

#natmult, #add, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', DYADE, DYADE#1, MULT, MULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c28, c29, c4

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

DYADE(z0, z1) → c25(DYADE#1(z0, z1))
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2))

(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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))

K tuples:

DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2))
DYADE(z0, z1) → c25(DYADE#1(z0, z1))

Defined Rule Symbols:

#natmult, #add, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', DYADE, DYADE#1, MULT, MULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c28, c29, c4

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MULT(z0, z1) → c28(MULT#1(z1, z0))

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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), 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) = 0
POL(#ADD(x₁, x₂)) = 0
POL(#MULT(x₁, x₂)) = 0
POL(#NATMULT(x₁, x₂)) = 0
POL(#add(x₁, x₂)) = 0
POL(#natmult(x₁, x₂)) = 0
POL(#neg(x₁)) = 0
POL(#pos(x₁)) = 0
POL(#s(x₁)) = 0
POL(#succ(x₁)) = 0
POL(*'(x₁, x₂)) = 0
POL(::(x₁, x₂)) = [1] + x₂
POL(DYADE(x₁, x₂)) = [2] + [3]x₁ + x₁·x₂ + [2]x₁²
POL(DYADE#1(x₁, x₂)) = [1] + x₁·x₂ + [2]x₁²
POL(MULT(x₁, x₂)) = [1] + x₂
POL(MULT#1(x₁, x₂)) = x₁
POL(c10(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c15(x₁, x₂)) = x₁ + x₂
POL(c24(x₁)) = x₁
POL(c25(x₁)) = x₁
POL(c26(x₁, x₂)) = x₁ + x₂
POL(c28(x₁)) = x₁
POL(c29(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c9(x₁)) = x₁

(16) 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(z1, z2))
MULT(z0, z1) → c28(MULT#1(z1, z0))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1))
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))

K tuples:

DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2))
DYADE(z0, z1) → c25(DYADE#1(z0, z1))
MULT(z0, z1) → c28(MULT#1(z1, z0))

Defined Rule Symbols:

#natmult, #add, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', DYADE, DYADE#1, MULT, MULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c28, c29, c4

(17) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))
*'(z0, z1) → c24(#MULT(z0, z1))
MULT(z0, z1) → c28(MULT#1(z1, z0))
#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

(0) Obligation:

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

(2) Obligation:

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(8) Obligation:

(9) CdtUsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(12) Obligation:

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(16) Obligation:

(17) CdtKnowledgeProof (EQUIVALENT transformation)

(18) BOUNDS(1, 1)