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

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

(0) Obligation:

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

D(t) → 1 2.33/1.04
D(constant) → 0 2.33/1.04
D(+(x, y)) → +(D(x), D(y)) 2.33/1.04
D(*(x, y)) → +(*(y, D(x)), *(x, D(y))) 2.33/1.04
D(-(x, y)) → -(D(x), D(y)) 2.33/1.04
D(minus(x)) → minus(D(x)) 2.33/1.04
D(div(x, y)) → -(div(D(x), y), div(*(x, D(y)), pow(y, 2))) 2.33/1.04
D(ln(x)) → div(D(x), x) 2.33/1.04
D(pow(x, y)) → +(*(*(y, pow(x, -(y, 1))), D(x)), *(*(pow(x, y), ln(x)), D(y)))

Rewrite Strategy: INNERMOST
2.33/1.04
2.33/1.04

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

Converted CpxTRS to CDT
2.33/1.04
2.33/1.04

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

D(t) → 1 2.33/1.04
D(constant) → 0 2.33/1.04
D(+(z0, z1)) → +(D(z0), D(z1)) 2.33/1.04
D(*(z0, z1)) → +(*(z1, D(z0)), *(z0, D(z1))) 2.33/1.04
D(-(z0, z1)) → -(D(z0), D(z1)) 2.33/1.04
D(minus(z0)) → minus(D(z0)) 2.33/1.04
D(div(z0, z1)) → -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) 2.33/1.04
D(ln(z0)) → div(D(z0), z0) 2.33/1.04
D(pow(z0, z1)) → +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1)))
Tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.04
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.04
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.04
D'(minus(z0)) → c5(D'(z0)) 2.33/1.04
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.04
D'(ln(z0)) → c7(D'(z0)) 2.33/1.04
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
S tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.04
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.04
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.04
D'(minus(z0)) → c5(D'(z0)) 2.33/1.04
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.04
D'(ln(z0)) → c7(D'(z0)) 2.33/1.04
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
K tuples:none
Defined Rule Symbols:

D

Defined Pair Symbols:

D'

Compound Symbols:

c2, c3, c4, c5, c6, c7, c8

2.33/1.04
2.33/1.04

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

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.04
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.04
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.04
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
We considered the (Usable) Rules:none
And the Tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.04
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.04
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.04
D'(minus(z0)) → c5(D'(z0)) 2.33/1.04
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.04
D'(ln(z0)) → c7(D'(z0)) 2.33/1.04
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 2.33/1.04

POL(*(x1, x2)) = [3] + x1 + x2    2.33/1.04
POL(+(x1, x2)) = [3] + x1 + x2    2.33/1.04
POL(-(x1, x2)) = [3] + x1 + x2    2.33/1.04
POL(D'(x1)) = [2]x1    2.33/1.04
POL(c2(x1, x2)) = x1 + x2    2.33/1.04
POL(c3(x1, x2)) = x1 + x2    2.33/1.04
POL(c4(x1, x2)) = x1 + x2    2.33/1.04
POL(c5(x1)) = x1    2.33/1.04
POL(c6(x1, x2)) = x1 + x2    2.33/1.04
POL(c7(x1)) = x1    2.33/1.04
POL(c8(x1, x2)) = x1 + x2    2.33/1.04
POL(div(x1, x2)) = x1 + x2    2.33/1.04
POL(ln(x1)) = x1    2.33/1.04
POL(minus(x1)) = x1    2.33/1.04
POL(pow(x1, x2)) = [3] + x1 + x2   
2.33/1.04
2.33/1.04

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

D(t) → 1 2.33/1.04
D(constant) → 0 2.33/1.04
D(+(z0, z1)) → +(D(z0), D(z1)) 2.33/1.04
D(*(z0, z1)) → +(*(z1, D(z0)), *(z0, D(z1))) 2.33/1.04
D(-(z0, z1)) → -(D(z0), D(z1)) 2.33/1.04
D(minus(z0)) → minus(D(z0)) 2.33/1.04
D(div(z0, z1)) → -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) 2.33/1.04
D(ln(z0)) → div(D(z0), z0) 2.33/1.04
D(pow(z0, z1)) → +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1)))
Tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.04
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.04
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.04
D'(minus(z0)) → c5(D'(z0)) 2.33/1.04
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.04
D'(ln(z0)) → c7(D'(z0)) 2.33/1.04
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
S tuples:

D'(minus(z0)) → c5(D'(z0)) 2.33/1.04
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.04
D'(ln(z0)) → c7(D'(z0))
K tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.04
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.04
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.04
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
Defined Rule Symbols:

D

Defined Pair Symbols:

D'

Compound Symbols:

c2, c3, c4, c5, c6, c7, c8

2.33/1.04
2.33/1.04

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

D'(minus(z0)) → c5(D'(z0)) 2.33/1.04
D'(div(z0, z1)) → c6(D'(z0), D'(z1))
We considered the (Usable) Rules:none
And the Tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.04
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.04
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.04
D'(minus(z0)) → c5(D'(z0)) 2.33/1.04
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.04
D'(ln(z0)) → c7(D'(z0)) 2.33/1.04
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 2.33/1.04

POL(*(x1, x2)) = [1] + x1 + x2    2.33/1.04
POL(+(x1, x2)) = [1] + x1 + x2    2.33/1.04
POL(-(x1, x2)) = [1] + x1 + x2    2.33/1.04
POL(D'(x1)) = [2] + [4]x1    2.33/1.04
POL(c2(x1, x2)) = x1 + x2    2.33/1.04
POL(c3(x1, x2)) = x1 + x2    2.33/1.04
POL(c4(x1, x2)) = x1 + x2    2.33/1.04
POL(c5(x1)) = x1    2.33/1.04
POL(c6(x1, x2)) = x1 + x2    2.33/1.04
POL(c7(x1)) = x1    2.33/1.04
POL(c8(x1, x2)) = x1 + x2    2.33/1.04
POL(div(x1, x2)) = [2] + x1 + x2    2.33/1.04
POL(ln(x1)) = x1    2.33/1.04
POL(minus(x1)) = [1] + x1    2.33/1.04
POL(pow(x1, x2)) = [1] + x1 + x2   
2.33/1.04
2.33/1.04

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

D(t) → 1 2.33/1.04
D(constant) → 0 2.33/1.04
D(+(z0, z1)) → +(D(z0), D(z1)) 2.33/1.04
D(*(z0, z1)) → +(*(z1, D(z0)), *(z0, D(z1))) 2.33/1.05
D(-(z0, z1)) → -(D(z0), D(z1)) 2.33/1.05
D(minus(z0)) → minus(D(z0)) 2.33/1.05
D(div(z0, z1)) → -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) 2.33/1.05
D(ln(z0)) → div(D(z0), z0) 2.33/1.05
D(pow(z0, z1)) → +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1)))
Tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.05
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.05
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.05
D'(minus(z0)) → c5(D'(z0)) 2.33/1.05
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.05
D'(ln(z0)) → c7(D'(z0)) 2.33/1.05
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
S tuples:

D'(ln(z0)) → c7(D'(z0))
K tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.05
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.05
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.05
D'(pow(z0, z1)) → c8(D'(z0), D'(z1)) 2.33/1.05
D'(minus(z0)) → c5(D'(z0)) 2.33/1.05
D'(div(z0, z1)) → c6(D'(z0), D'(z1))
Defined Rule Symbols:

D

Defined Pair Symbols:

D'

Compound Symbols:

c2, c3, c4, c5, c6, c7, c8

2.33/1.05
2.33/1.05

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

D'(ln(z0)) → c7(D'(z0))
We considered the (Usable) Rules:none
And the Tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.05
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.05
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.05
D'(minus(z0)) → c5(D'(z0)) 2.33/1.05
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.05
D'(ln(z0)) → c7(D'(z0)) 2.33/1.05
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 2.33/1.05

POL(*(x1, x2)) = [1] + x1 + x2    2.33/1.05
POL(+(x1, x2)) = [1] + x1 + x2    2.33/1.05
POL(-(x1, x2)) = [1] + x1 + x2    2.33/1.05
POL(D'(x1)) = [3] + [4]x1    2.33/1.05
POL(c2(x1, x2)) = x1 + x2    2.33/1.05
POL(c3(x1, x2)) = x1 + x2    2.33/1.05
POL(c4(x1, x2)) = x1 + x2    2.33/1.05
POL(c5(x1)) = x1    2.33/1.05
POL(c6(x1, x2)) = x1 + x2    2.33/1.05
POL(c7(x1)) = x1    2.33/1.05
POL(c8(x1, x2)) = x1 + x2    2.33/1.05
POL(div(x1, x2)) = [1] + x1 + x2    2.33/1.05
POL(ln(x1)) = [1] + x1    2.33/1.05
POL(minus(x1)) = x1    2.33/1.05
POL(pow(x1, x2)) = [1] + x1 + x2   
2.33/1.05
2.33/1.05

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

D(t) → 1 2.33/1.05
D(constant) → 0 2.33/1.05
D(+(z0, z1)) → +(D(z0), D(z1)) 2.33/1.05
D(*(z0, z1)) → +(*(z1, D(z0)), *(z0, D(z1))) 2.33/1.05
D(-(z0, z1)) → -(D(z0), D(z1)) 2.33/1.05
D(minus(z0)) → minus(D(z0)) 2.33/1.05
D(div(z0, z1)) → -(div(D(z0), z1), div(*(z0, D(z1)), pow(z1, 2))) 2.33/1.05
D(ln(z0)) → div(D(z0), z0) 2.33/1.05
D(pow(z0, z1)) → +(*(*(z1, pow(z0, -(z1, 1))), D(z0)), *(*(pow(z0, z1), ln(z0)), D(z1)))
Tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.05
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.05
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.05
D'(minus(z0)) → c5(D'(z0)) 2.33/1.05
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.05
D'(ln(z0)) → c7(D'(z0)) 2.33/1.05
D'(pow(z0, z1)) → c8(D'(z0), D'(z1))
S tuples:none
K tuples:

D'(+(z0, z1)) → c2(D'(z0), D'(z1)) 2.33/1.05
D'(*(z0, z1)) → c3(D'(z0), D'(z1)) 2.33/1.05
D'(-(z0, z1)) → c4(D'(z0), D'(z1)) 2.33/1.05
D'(pow(z0, z1)) → c8(D'(z0), D'(z1)) 2.33/1.05
D'(minus(z0)) → c5(D'(z0)) 2.33/1.05
D'(div(z0, z1)) → c6(D'(z0), D'(z1)) 2.33/1.05
D'(ln(z0)) → c7(D'(z0))
Defined Rule Symbols:

D

Defined Pair Symbols:

D'

Compound Symbols:

c2, c3, c4, c5, c6, c7, c8

2.33/1.05
2.33/1.05

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

The set S is empty
2.33/1.05
2.33/1.05

(10) BOUNDS(O(1), O(1))

2.33/1.05
2.33/1.05
2.58/1.11 EOF