YES(O(1), O(n^3)) 13.90/4.41 YES(O(1), O(n^3)) 13.90/4.44 13.90/4.44 13.90/4.44 13.90/4.44 13.90/4.44 13.90/4.44 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 13.90/4.44 13.90/4.44 13.90/4.44
13.90/4.44
13.90/4.44
13.90/4.44
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^3)).

0 CpxTRS
13.90/4.44 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
13.90/4.44 
↳2 CdtProblem
13.90/4.44 
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
13.90/4.44 
↳4 CdtProblem
13.90/4.44 
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
13.90/4.44 
↳6 CdtProblem
13.90/4.44 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
13.90/4.44 
↳8 CdtProblem
13.90/4.44 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))
13.90/4.44 
↳10 CdtProblem
13.90/4.44 
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))
13.90/4.44 
↳12 BOUNDS(O(1), O(1))
13.90/4.44
13.90/4.44 13.90/4.44
13.90/4.44
13.90/4.44

(0) Obligation:

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

+(0, y) → y 13.90/4.44
+(s(x), y) → s(+(x, y)) 13.90/4.44
+(p(x), y) → p(+(x, y)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(x)) → p(minus(x)) 13.90/4.44
minus(p(x)) → s(minus(x)) 13.90/4.44
*(0, y) → 0 13.90/4.44
*(s(x), y) → +(*(x, y), y) 13.90/4.44
*(p(x), y) → +(*(x, y), minus(y))

Rewrite Strategy: INNERMOST
13.90/4.44
13.90/4.44

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
13.90/4.44
13.90/4.44

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:none
Defined Rule Symbols:

+, minus, *

Defined Pair Symbols:

+', MINUS, *'

Compound Symbols:

c1, c2, c4, c5, c7, c8

13.90/4.44
13.90/4.44

(3) 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.

*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
We considered the (Usable) Rules:

*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1))
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 13.90/4.44

POL(*(x1, x2)) = 0    13.90/4.44
POL(*'(x1, x2)) = [4]x1    13.90/4.44
POL(+(x1, x2)) = [3]    13.90/4.44
POL(+'(x1, x2)) = 0    13.90/4.44
POL(0) = [3]    13.90/4.44
POL(MINUS(x1)) = 0    13.90/4.44
POL(c1(x1)) = x1    13.90/4.44
POL(c2(x1)) = x1    13.90/4.44
POL(c4(x1)) = x1    13.90/4.44
POL(c5(x1)) = x1    13.90/4.44
POL(c7(x1, x2)) = x1 + x2    13.90/4.44
POL(c8(x1, x2, x3)) = x1 + x2 + x3    13.90/4.44
POL(minus(x1)) = 0    13.90/4.44
POL(p(x1)) = x1    13.90/4.44
POL(s(x1)) = [1] + x1   
13.90/4.44
13.90/4.44

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:

*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
Defined Rule Symbols:

+, minus, *

Defined Pair Symbols:

+', MINUS, *'

Compound Symbols:

c1, c2, c4, c5, c7, c8

13.90/4.44
13.90/4.44

(5) 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.

*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
We considered the (Usable) Rules:

*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1))
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 13.90/4.44

POL(*(x1, x2)) = 0    13.90/4.44
POL(*'(x1, x2)) = x1    13.90/4.44
POL(+(x1, x2)) = [3]    13.90/4.44
POL(+'(x1, x2)) = [1]    13.90/4.44
POL(0) = 0    13.90/4.44
POL(MINUS(x1)) = 0    13.90/4.44
POL(c1(x1)) = x1    13.90/4.44
POL(c2(x1)) = x1    13.90/4.44
POL(c4(x1)) = x1    13.90/4.44
POL(c5(x1)) = x1    13.90/4.44
POL(c7(x1, x2)) = x1 + x2    13.90/4.44
POL(c8(x1, x2, x3)) = x1 + x2 + x3    13.90/4.44
POL(minus(x1)) = [4] + [5]x1    13.90/4.44
POL(p(x1)) = [4] + x1    13.90/4.44
POL(s(x1)) = [1] + x1   
13.90/4.44
13.90/4.44

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0))
K tuples:

*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
Defined Rule Symbols:

+, minus, *

Defined Pair Symbols:

+', MINUS, *'

Compound Symbols:

c1, c2, c4, c5, c7, c8

13.90/4.44
13.90/4.44

(7) 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.

MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0))
We considered the (Usable) Rules:

*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1))
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 13.90/4.44

POL(*(x1, x2)) = [3]x22    13.90/4.44
POL(*'(x1, x2)) = [3]x1 + x1·x2 + x12    13.90/4.44
POL(+(x1, x2)) = [3]    13.90/4.44
POL(+'(x1, x2)) = [2]    13.90/4.44
POL(0) = 0    13.90/4.44
POL(MINUS(x1)) = [2] + [2]x1    13.90/4.44
POL(c1(x1)) = x1    13.90/4.44
POL(c2(x1)) = x1    13.90/4.44
POL(c4(x1)) = x1    13.90/4.44
POL(c5(x1)) = x1    13.90/4.44
POL(c7(x1, x2)) = x1 + x2    13.90/4.44
POL(c8(x1, x2, x3)) = x1 + x2 + x3    13.90/4.44
POL(minus(x1)) = 0    13.90/4.44
POL(p(x1)) = [2] + x1    13.90/4.44
POL(s(x1)) = [1] + x1   
13.90/4.44
13.90/4.44

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
S tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1))
K tuples:

*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0))
Defined Rule Symbols:

+, minus, *

Defined Pair Symbols:

+', MINUS, *'

Compound Symbols:

c1, c2, c4, c5, c7, c8

13.90/4.44
13.90/4.44

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

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

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1))
We considered the (Usable) Rules:

*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1))
And the Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 13.90/4.44

POL(*(x1, x2)) = x1·x2    13.90/4.44
POL(*'(x1, x2)) = x12·x2    13.90/4.44
POL(+(x1, x2)) = x1 + x2    13.90/4.44
POL(+'(x1, x2)) = x1    13.90/4.44
POL(0) = 0    13.90/4.44
POL(MINUS(x1)) = 0    13.90/4.44
POL(c1(x1)) = x1    13.90/4.44
POL(c2(x1)) = x1    13.90/4.44
POL(c4(x1)) = x1    13.90/4.44
POL(c5(x1)) = x1    13.90/4.44
POL(c7(x1, x2)) = x1 + x2    13.90/4.44
POL(c8(x1, x2, x3)) = x1 + x2 + x3    13.90/4.44
POL(minus(x1)) = x1    13.90/4.44
POL(p(x1)) = [1] + x1    13.90/4.44
POL(s(x1)) = [1] + x1   
13.90/4.44
13.90/4.44

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(0, z0) → z0 13.90/4.44
+(s(z0), z1) → s(+(z0, z1)) 13.90/4.44
+(p(z0), z1) → p(+(z0, z1)) 13.90/4.44
minus(0) → 0 13.90/4.44
minus(s(z0)) → p(minus(z0)) 13.90/4.44
minus(p(z0)) → s(minus(z0)) 13.90/4.44
*(0, z0) → 0 13.90/4.44
*(s(z0), z1) → +(*(z0, z1), z1) 13.90/4.44
*(p(z0), z1) → +(*(z0, z1), minus(z1))
Tuples:

+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
S tuples:none
K tuples:

*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1)) 13.90/4.44
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1)) 13.90/4.44
MINUS(s(z0)) → c4(MINUS(z0)) 13.90/4.44
MINUS(p(z0)) → c5(MINUS(z0)) 13.90/4.44
+'(s(z0), z1) → c1(+'(z0, z1)) 13.90/4.44
+'(p(z0), z1) → c2(+'(z0, z1))
Defined Rule Symbols:

+, minus, *

Defined Pair Symbols:

+', MINUS, *'

Compound Symbols:

c1, c2, c4, c5, c7, c8

13.90/4.44
13.90/4.44

(11) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty
13.90/4.44
13.90/4.44

(12) BOUNDS(O(1), O(1))

13.90/4.44
13.90/4.44
13.90/4.49 EOF