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

0 CpxTRS
2.81/1.20 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
2.81/1.20 
↳2 CdtProblem
2.81/1.20 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
2.81/1.20 
↳4 CdtProblem
2.81/1.20 
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
2.81/1.20 
↳6 CdtProblem
2.81/1.20 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
2.81/1.20 
↳8 CdtProblem
2.81/1.20 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
2.81/1.20 
↳10 CdtProblem
2.81/1.20 
↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
2.81/1.20 
↳12 CdtProblem
2.81/1.20 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
2.81/1.20 
↳14 CdtProblem
2.81/1.20 
↳15 SIsEmptyProof (BOTH BOUNDS(ID, ID))
2.81/1.20 
↳16 BOUNDS(O(1), O(1))
2.81/1.20
2.81/1.20 2.81/1.20
2.81/1.20
2.81/1.20

(0) Obligation:

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

f(X) → if(X, c, n__f(n__true)) 2.81/1.20
if(true, X, Y) → X 2.81/1.20
if(false, X, Y) → activate(Y) 2.81/1.20
f(X) → n__f(X) 2.81/1.20
true → n__true 2.81/1.20
activate(n__f(X)) → f(activate(X)) 2.81/1.20
activate(n__true) → true 2.81/1.20
activate(X) → X

Rewrite Strategy: INNERMOST
2.81/1.20
2.81/1.20

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

Converted CpxTRS to CDT
2.81/1.20
2.81/1.20

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(n__true)) 2.81/1.20
f(z0) → n__f(z0) 2.81/1.20
if(true, z0, z1) → z0 2.81/1.20
if(false, z0, z1) → activate(z1) 2.81/1.20
true → n__true 2.81/1.20
activate(n__f(z0)) → f(activate(z0)) 2.81/1.20
activate(n__true) → true 2.81/1.20
activate(z0) → z0
Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 2.81/1.20
IF(false, z0, z1) → c4(ACTIVATE(z1)) 2.81/1.20
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 2.81/1.20
ACTIVATE(n__true) → c7(TRUE)
S tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 2.81/1.20
IF(false, z0, z1) → c4(ACTIVATE(z1)) 2.81/1.20
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7(TRUE)
K tuples:none
Defined Rule Symbols:

f, if, true, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c6, c7

3.15/1.21
3.15/1.21

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

Removed 1 trailing tuple parts
3.15/1.21
3.15/1.21

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
S tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
K tuples:none
Defined Rule Symbols:

f, if, true, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c6, c7

3.15/1.21
3.15/1.21

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

Removed 1 trailing nodes:

ACTIVATE(n__true) → c7
3.15/1.21
3.15/1.21

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
S tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
K tuples:none
Defined Rule Symbols:

f, if, true, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c6, c7

3.15/1.21
3.15/1.21

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

ACTIVATE(n__true) → c7
We considered the (Usable) Rules:

if(false, z0, z1) → activate(z1) 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0 3.15/1.21
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
true → n__true
And the Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
The order we found is given by the following interpretation:
Polynomial interpretation : 3.15/1.21

POL(ACTIVATE(x1)) = [1] + x12    3.15/1.21
POL(F(x1)) = [1] + [2]x1    3.15/1.21
POL(IF(x1, x2, x3)) = x1 + [3]x2 + x32 + [3]x1·x2 + [3]x22    3.15/1.21
POL(activate(x1)) = x1    3.15/1.21
POL(c) = 0    3.15/1.21
POL(c1(x1)) = x1    3.15/1.21
POL(c4(x1)) = x1    3.15/1.21
POL(c6(x1, x2)) = x1 + x2    3.15/1.21
POL(c7) = 0    3.15/1.21
POL(f(x1)) = [1] + x1    3.15/1.21
POL(false) = [1]    3.15/1.21
POL(if(x1, x2, x3)) = [3]x2 + x3 + [3]x1·x2    3.15/1.21
POL(n__f(x1)) = [1] + x1    3.15/1.21
POL(n__true) = 0    3.15/1.21
POL(true) = 0   
3.15/1.21
3.15/1.21

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
S tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
K tuples:

ACTIVATE(n__true) → c7
Defined Rule Symbols:

f, if, true, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c6, c7

3.15/1.21
3.15/1.21

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

F(z0) → c1(IF(z0, c, n__f(n__true)))
We considered the (Usable) Rules:

if(false, z0, z1) → activate(z1) 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0 3.15/1.21
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
true → n__true
And the Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
The order we found is given by the following interpretation:
Polynomial interpretation : 3.15/1.21

POL(ACTIVATE(x1)) = x1 + x12    3.15/1.21
POL(F(x1)) = [2] + [2]x1    3.15/1.21
POL(IF(x1, x2, x3)) = [3]x2 + x32 + [2]x1·x3 + [3]x1·x2 + [3]x22    3.15/1.21
POL(activate(x1)) = x1    3.15/1.21
POL(c) = 0    3.15/1.21
POL(c1(x1)) = x1    3.15/1.21
POL(c4(x1)) = x1    3.15/1.21
POL(c6(x1, x2)) = x1 + x2    3.15/1.21
POL(c7) = 0    3.15/1.21
POL(f(x1)) = [1] + x1    3.15/1.21
POL(false) = [2]    3.15/1.21
POL(if(x1, x2, x3)) = [3]x2 + x1·x3 + [3]x1·x2    3.15/1.21
POL(n__f(x1)) = [1] + x1    3.15/1.21
POL(n__true) = 0    3.15/1.21
POL(true) = 0   
3.15/1.21
3.15/1.21

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
S tuples:

IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
K tuples:

ACTIVATE(n__true) → c7 3.15/1.21
F(z0) → c1(IF(z0, c, n__f(n__true)))
Defined Rule Symbols:

f, if, true, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c6, c7

3.15/1.21
3.15/1.21

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

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

IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__true) → c7
3.15/1.21
3.15/1.21

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
S tuples:

ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
K tuples:

ACTIVATE(n__true) → c7 3.15/1.21
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1))
Defined Rule Symbols:

f, if, true, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c6, c7

3.15/1.21
3.15/1.21

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

ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
We considered the (Usable) Rules:

if(false, z0, z1) → activate(z1) 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0 3.15/1.21
f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
true → n__true
And the Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
The order we found is given by the following interpretation:
Polynomial interpretation : 3.15/1.21

POL(ACTIVATE(x1)) = [2]x1 + x12    3.15/1.21
POL(F(x1)) = [1] + x1    3.15/1.21
POL(IF(x1, x2, x3)) = [3]x2 + x32 + x1·x3 + [3]x1·x2 + [3]x22    3.15/1.21
POL(activate(x1)) = [2]x1    3.15/1.21
POL(c) = 0    3.15/1.21
POL(c1(x1)) = x1    3.15/1.21
POL(c4(x1)) = x1    3.15/1.21
POL(c6(x1, x2)) = x1 + x2    3.15/1.21
POL(c7) = 0    3.15/1.21
POL(f(x1)) = [1] + x1    3.15/1.21
POL(false) = [2]    3.15/1.21
POL(if(x1, x2, x3)) = [3]x2 + x1·x3 + [3]x1·x2    3.15/1.21
POL(n__f(x1)) = [1] + x1    3.15/1.21
POL(n__true) = 0    3.15/1.21
POL(true) = 0   
3.15/1.21
3.15/1.21

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0) → if(z0, c, n__f(n__true)) 3.15/1.21
f(z0) → n__f(z0) 3.15/1.21
if(true, z0, z1) → z0 3.15/1.21
if(false, z0, z1) → activate(z1) 3.15/1.21
true → n__true 3.15/1.21
activate(n__f(z0)) → f(activate(z0)) 3.15/1.21
activate(n__true) → true 3.15/1.21
activate(z0) → z0
Tuples:

F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 3.15/1.21
ACTIVATE(n__true) → c7
S tuples:none
K tuples:

ACTIVATE(n__true) → c7 3.15/1.21
F(z0) → c1(IF(z0, c, n__f(n__true))) 3.15/1.21
IF(false, z0, z1) → c4(ACTIVATE(z1)) 3.15/1.21
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0))
Defined Rule Symbols:

f, if, true, activate

Defined Pair Symbols:

F, IF, ACTIVATE

Compound Symbols:

c1, c4, c6, c7

3.15/1.21
3.15/1.21

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

The set S is empty
3.15/1.21
3.15/1.21

(16) BOUNDS(O(1), O(1))

3.15/1.21
3.15/1.21
3.15/1.29 EOF