YES(O(1), O(n^2)) 9.02/2.78 YES(O(1), O(n^2)) 9.42/2.88 9.42/2.88 9.42/2.88 9.42/2.88 9.42/2.88 9.42/2.88 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 9.42/2.88 9.42/2.88 9.42/2.88
9.42/2.88 9.42/2.88 9.42/2.88
9.42/2.88
9.42/2.88

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

*(@x, @y) → #mult(@x, @y) 9.42/2.88
dyade(@l1, @l2) → dyade#1(@l1, @l2) 9.42/2.88
dyade#1(::(@x, @xs), @l2) → ::(mult(@x, @l2), dyade(@xs, @l2)) 9.42/2.88
dyade#1(nil, @l2) → nil 9.42/2.88
mult(@n, @l) → mult#1(@l, @n) 9.42/2.88
mult#1(::(@x, @xs), @n) → ::(*(@n, @x), mult(@n, @xs)) 9.42/2.88
mult#1(nil, @n) → nil

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

#add(#0, @y) → @y 9.42/2.88
#add(#neg(#s(#0)), @y) → #pred(@y) 9.42/2.88
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) 9.42/2.88
#add(#pos(#s(#0)), @y) → #succ(@y) 9.42/2.88
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) 9.42/2.88
#mult(#0, #0) → #0 9.42/2.88
#mult(#0, #neg(@y)) → #0 9.42/2.88
#mult(#0, #pos(@y)) → #0 9.42/2.88
#mult(#neg(@x), #0) → #0 9.42/2.88
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) 9.42/2.88
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) 9.42/2.88
#mult(#pos(@x), #0) → #0 9.42/2.88
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) 9.42/2.88
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) 9.42/2.88
#natmult(#0, @y) → #0 9.42/2.88
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) 9.42/2.88
#pred(#0) → #neg(#s(#0)) 9.42/2.88
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) 9.42/2.88
#pred(#pos(#s(#0))) → #0 9.42/2.88
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) 9.42/2.88
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST
9.42/2.88
9.42/2.88

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
9.42/2.88
9.42/2.88

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 9.42/2.88
#add(#neg(#s(#0)), z0) → #pred(z0) 9.42/2.88
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 9.42/2.88
#add(#pos(#s(#0)), z0) → #succ(z0) 9.42/2.88
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 9.42/2.88
#mult(#0, #0) → #0 9.42/2.88
#mult(#0, #neg(z0)) → #0 9.42/2.88
#mult(#0, #pos(z0)) → #0 9.42/2.88
#mult(#neg(z0), #0) → #0 9.42/2.88
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #0) → #0 9.42/2.88
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#natmult(#0, z0) → #0 9.42/2.88
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 9.42/2.88
#pred(#0) → #neg(#s(#0)) 9.42/2.88
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 9.42/2.88
#pred(#pos(#s(#0))) → #0 9.42/2.88
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 9.42/2.88
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 9.42/2.88
*(z0, z1) → #mult(z0, z1) 9.42/2.88
dyade(z0, z1) → dyade#1(z0, z1) 9.42/2.88
dyade#1(::(z0, z1), z2) → ::(mult(z0, z2), dyade(z1, z2)) 9.42/2.88
dyade#1(nil, z0) → nil 9.42/2.88
mult(z0, z1) → mult#1(z1, z0) 9.42/2.88
mult#1(::(z0, z1), z2) → ::(*(z2, z0), mult(z2, z1)) 9.42/2.88
mult#1(nil, z0) → nil
Tuples:

#ADD(#neg(#s(#0)), z0) → c1(#PRED(z0)) 9.42/2.88
#ADD(#neg(#s(#s(z0))), z1) → c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) 9.42/2.88
#ADD(#pos(#s(#0)), z0) → c3(#SUCC(z0)) 9.42/2.88
#ADD(#pos(#s(#s(z0))), z1) → c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) 9.42/2.88
#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 9.42/2.88
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1))
S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
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:

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

9.42/2.88
9.42/2.88

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

Removed 4 trailing tuple parts
9.42/2.88
9.42/2.88

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 9.42/2.88
#add(#neg(#s(#0)), z0) → #pred(z0) 9.42/2.88
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 9.42/2.88
#add(#pos(#s(#0)), z0) → #succ(z0) 9.42/2.88
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 9.42/2.88
#mult(#0, #0) → #0 9.42/2.88
#mult(#0, #neg(z0)) → #0 9.42/2.88
#mult(#0, #pos(z0)) → #0 9.42/2.88
#mult(#neg(z0), #0) → #0 9.42/2.88
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #0) → #0 9.42/2.88
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#natmult(#0, z0) → #0 9.42/2.88
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 9.42/2.88
#pred(#0) → #neg(#s(#0)) 9.42/2.88
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 9.42/2.88
#pred(#pos(#s(#0))) → #0 9.42/2.88
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 9.42/2.88
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 9.42/2.88
*(z0, z1) → #mult(z0, z1) 9.42/2.88
dyade(z0, z1) → dyade#1(z0, z1) 9.42/2.88
dyade#1(::(z0, z1), z2) → ::(mult(z0, z2), dyade(z1, z2)) 9.42/2.88
dyade#1(nil, z0) → nil 9.42/2.88
mult(z0, z1) → mult#1(z1, z0) 9.42/2.88
mult#1(::(z0, z1), z2) → ::(*(z2, z0), mult(z2, z1)) 9.42/2.88
mult#1(nil, z0) → nil
Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 9.42/2.88
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1)) 9.42/2.88
#ADD(#neg(#s(#0)), z0) → c1 9.42/2.88
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 9.42/2.88
#ADD(#pos(#s(#0)), z0) → c3 9.42/2.88
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))
S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
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, c1, c2, c3, c4

9.42/2.88
9.42/2.88

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1))
Removed 2 trailing nodes:

#ADD(#pos(#s(#0)), z0) → c3 9.42/2.88
#ADD(#neg(#s(#0)), z0) → c1
9.42/2.88
9.42/2.88

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 9.42/2.88
#add(#neg(#s(#0)), z0) → #pred(z0) 9.42/2.88
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 9.42/2.88
#add(#pos(#s(#0)), z0) → #succ(z0) 9.42/2.88
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 9.42/2.88
#mult(#0, #0) → #0 9.42/2.88
#mult(#0, #neg(z0)) → #0 9.42/2.88
#mult(#0, #pos(z0)) → #0 9.42/2.88
#mult(#neg(z0), #0) → #0 9.42/2.88
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #0) → #0 9.42/2.88
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#natmult(#0, z0) → #0 9.42/2.88
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 9.42/2.88
#pred(#0) → #neg(#s(#0)) 9.42/2.88
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 9.42/2.88
#pred(#pos(#s(#0))) → #0 9.42/2.88
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 9.42/2.88
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 9.42/2.88
*(z0, z1) → #mult(z0, z1) 9.42/2.88
dyade(z0, z1) → dyade#1(z0, z1) 9.42/2.88
dyade#1(::(z0, z1), z2) → ::(mult(z0, z2), dyade(z1, z2)) 9.42/2.88
dyade#1(nil, z0) → nil 9.42/2.88
mult(z0, z1) → mult#1(z1, z0) 9.42/2.88
mult#1(::(z0, z1), z2) → ::(*(z2, z0), mult(z2, z1)) 9.42/2.88
mult#1(nil, z0) → nil
Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 9.42/2.88
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1)) 9.42/2.88
#ADD(#pos(#s(#0)), z0) → c3 9.42/2.88
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))
S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
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, c3, c4

9.42/2.88
9.42/2.88

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(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:

#natmult(#0, z0) → #0 9.42/2.88
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 9.42/2.88
#add(#pos(#s(#0)), z0) → #succ(z0) 9.42/2.88
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 9.42/2.88
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
And the Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 9.42/2.88
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1)) 9.42/2.88
#ADD(#pos(#s(#0)), z0) → c3 9.42/2.88
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.42/2.88

POL(#0) = 0    9.42/2.88
POL(#ADD(x1, x2)) = 0    9.42/2.88
POL(#MULT(x1, x2)) = 0    9.42/2.88
POL(#NATMULT(x1, x2)) = 0    9.42/2.88
POL(#add(x1, x2)) = [3] + [3]x1 + [3]x2    9.42/2.88
POL(#natmult(x1, x2)) = 0    9.42/2.88
POL(#neg(x1)) = 0    9.42/2.88
POL(#pos(x1)) = 0    9.42/2.88
POL(#s(x1)) = 0    9.42/2.88
POL(#succ(x1)) = [3]    9.42/2.88
POL(*'(x1, x2)) = 0    9.42/2.88
POL(::(x1, x2)) = [1] + x2    9.42/2.88
POL(DYADE(x1, x2)) = x1    9.42/2.88
POL(DYADE#1(x1, x2)) = x1    9.42/2.88
POL(MULT(x1, x2)) = 0    9.42/2.88
POL(MULT#1(x1, x2)) = 0    9.42/2.88
POL(c10(x1)) = x1    9.42/2.88
POL(c12(x1)) = x1    9.42/2.88
POL(c13(x1)) = x1    9.42/2.88
POL(c15(x1, x2)) = x1 + x2    9.42/2.88
POL(c24(x1)) = x1    9.42/2.88
POL(c25(x1)) = x1    9.42/2.88
POL(c26(x1, x2)) = x1 + x2    9.42/2.88
POL(c28(x1)) = x1    9.42/2.88
POL(c29(x1, x2)) = x1 + x2    9.42/2.88
POL(c3) = 0    9.42/2.88
POL(c4(x1)) = x1    9.42/2.88
POL(c9(x1)) = x1   
9.42/2.88
9.42/2.88

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 9.42/2.88
#add(#neg(#s(#0)), z0) → #pred(z0) 9.42/2.88
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 9.42/2.88
#add(#pos(#s(#0)), z0) → #succ(z0) 9.42/2.88
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 9.42/2.88
#mult(#0, #0) → #0 9.42/2.88
#mult(#0, #neg(z0)) → #0 9.42/2.88
#mult(#0, #pos(z0)) → #0 9.42/2.88
#mult(#neg(z0), #0) → #0 9.42/2.88
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #0) → #0 9.42/2.88
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#natmult(#0, z0) → #0 9.42/2.88
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 9.42/2.88
#pred(#0) → #neg(#s(#0)) 9.42/2.88
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 9.42/2.88
#pred(#pos(#s(#0))) → #0 9.42/2.88
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 9.42/2.88
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 9.42/2.88
*(z0, z1) → #mult(z0, z1) 9.42/2.88
dyade(z0, z1) → dyade#1(z0, z1) 9.42/2.88
dyade#1(::(z0, z1), z2) → ::(mult(z0, z2), dyade(z1, z2)) 9.42/2.88
dyade#1(nil, z0) → nil 9.42/2.88
mult(z0, z1) → mult#1(z1, z0) 9.42/2.88
mult#1(::(z0, z1), z2) → ::(*(z2, z0), mult(z2, z1)) 9.42/2.88
mult#1(nil, z0) → nil
Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 9.42/2.88
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1)) 9.42/2.88
#ADD(#pos(#s(#0)), z0) → c3 9.42/2.88
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))
S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
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:

*, 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, c3, c4

9.42/2.88
9.42/2.88

(9) 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)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2))
9.42/2.88
9.42/2.88

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 9.42/2.88
#add(#neg(#s(#0)), z0) → #pred(z0) 9.42/2.88
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 9.42/2.88
#add(#pos(#s(#0)), z0) → #succ(z0) 9.42/2.88
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 9.42/2.88
#mult(#0, #0) → #0 9.42/2.88
#mult(#0, #neg(z0)) → #0 9.42/2.88
#mult(#0, #pos(z0)) → #0 9.42/2.88
#mult(#neg(z0), #0) → #0 9.42/2.88
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #0) → #0 9.42/2.88
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#natmult(#0, z0) → #0 9.42/2.88
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 9.42/2.88
#pred(#0) → #neg(#s(#0)) 9.42/2.88
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 9.42/2.88
#pred(#pos(#s(#0))) → #0 9.42/2.88
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 9.42/2.88
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 9.42/2.88
*(z0, z1) → #mult(z0, z1) 9.42/2.88
dyade(z0, z1) → dyade#1(z0, z1) 9.42/2.88
dyade#1(::(z0, z1), z2) → ::(mult(z0, z2), dyade(z1, z2)) 9.42/2.88
dyade#1(nil, z0) → nil 9.42/2.88
mult(z0, z1) → mult#1(z1, z0) 9.42/2.88
mult#1(::(z0, z1), z2) → ::(*(z2, z0), mult(z2, z1)) 9.42/2.88
mult#1(nil, z0) → nil
Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 9.42/2.88
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1)) 9.42/2.88
#ADD(#pos(#s(#0)), z0) → c3 9.42/2.88
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))
S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
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)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1))
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, c3, c4

9.42/2.88
9.42/2.88

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(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:

#natmult(#0, z0) → #0 9.42/2.88
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 9.42/2.88
#add(#pos(#s(#0)), z0) → #succ(z0) 9.42/2.88
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 9.42/2.88
#succ(#pos(#s(z0))) → #pos(#s(#s(z0)))
And the Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 9.42/2.88
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1)) 9.42/2.88
#ADD(#pos(#s(#0)), z0) → c3 9.42/2.88
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.42/2.88

POL(#0) = 0    9.42/2.88
POL(#ADD(x1, x2)) = [3]x1    9.42/2.88
POL(#MULT(x1, x2)) = x2    9.42/2.88
POL(#NATMULT(x1, x2)) = 0    9.42/2.88
POL(#add(x1, x2)) = [3]    9.42/2.88
POL(#natmult(x1, x2)) = 0    9.42/2.88
POL(#neg(x1)) = 0    9.42/2.88
POL(#pos(x1)) = 0    9.42/2.88
POL(#s(x1)) = 0    9.42/2.88
POL(#succ(x1)) = [3] + [3]x1    9.42/2.88
POL(*'(x1, x2)) = x2 + [2]x1·x2    9.42/2.88
POL(::(x1, x2)) = [1] + x1 + x2    9.42/2.88
POL(DYADE(x1, x2)) = [1] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2    9.42/2.88
POL(DYADE#1(x1, x2)) = [1] + [3]x1 + [3]x2 + [3]x22 + [3]x1·x2    9.42/2.88
POL(MULT(x1, x2)) = [1] + x2 + [2]x1·x2    9.42/2.88
POL(MULT#1(x1, x2)) = x1 + [2]x1·x2    9.42/2.88
POL(c10(x1)) = x1    9.42/2.88
POL(c12(x1)) = x1    9.42/2.88
POL(c13(x1)) = x1    9.42/2.88
POL(c15(x1, x2)) = x1 + x2    9.42/2.88
POL(c24(x1)) = x1    9.42/2.88
POL(c25(x1)) = x1    9.42/2.88
POL(c26(x1, x2)) = x1 + x2    9.42/2.88
POL(c28(x1)) = x1    9.42/2.88
POL(c29(x1, x2)) = x1 + x2    9.42/2.88
POL(c3) = 0    9.42/2.88
POL(c4(x1)) = x1    9.42/2.88
POL(c9(x1)) = x1   
9.42/2.88
9.42/2.88

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 9.42/2.88
#add(#neg(#s(#0)), z0) → #pred(z0) 9.42/2.88
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 9.42/2.88
#add(#pos(#s(#0)), z0) → #succ(z0) 9.42/2.88
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 9.42/2.88
#mult(#0, #0) → #0 9.42/2.88
#mult(#0, #neg(z0)) → #0 9.42/2.88
#mult(#0, #pos(z0)) → #0 9.42/2.88
#mult(#neg(z0), #0) → #0 9.42/2.88
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #0) → #0 9.42/2.88
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 9.42/2.88
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 9.42/2.88
#natmult(#0, z0) → #0 9.42/2.88
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 9.42/2.88
#pred(#0) → #neg(#s(#0)) 9.42/2.88
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 9.42/2.88
#pred(#pos(#s(#0))) → #0 9.42/2.88
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 9.42/2.88
#succ(#0) → #pos(#s(#0)) 9.42/2.88
#succ(#neg(#s(#0))) → #0 9.42/2.88
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 9.42/2.88
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 9.42/2.88
*(z0, z1) → #mult(z0, z1) 9.42/2.88
dyade(z0, z1) → dyade#1(z0, z1) 9.42/2.88
dyade#1(::(z0, z1), z2) → ::(mult(z0, z2), dyade(z1, z2)) 9.42/2.88
dyade#1(nil, z0) → nil 9.42/2.88
mult(z0, z1) → mult#1(z1, z0) 9.42/2.88
mult#1(::(z0, z1), z2) → ::(*(z2, z0), mult(z2, z1)) 9.42/2.88
mult#1(nil, z0) → nil
Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 9.42/2.88
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
DYADE#1(::(z0, z1), z2) → c26(MULT(z0, z2), DYADE(z1, z2)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
MULT#1(::(z0, z1), z2) → c29(*'(z2, z0), MULT(z2, z1)) 9.42/2.88
#ADD(#pos(#s(#0)), z0) → c3 9.42/2.88
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))
S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
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)) 9.42/2.88
DYADE(z0, z1) → c25(DYADE#1(z0, z1)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0))
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, c3, c4

9.42/2.88
9.42/2.88

(13) 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)) 9.42/2.88
*'(z0, z1) → c24(#MULT(z0, z1)) 9.42/2.88
MULT(z0, z1) → c28(MULT#1(z1, z0)) 9.42/2.88
#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 9.42/2.88
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1))
Now S is empty
9.42/2.88
9.42/2.88

(14) BOUNDS(O(1), O(1))

9.42/2.88
9.42/2.88
9.79/2.91 EOF