YES(O(1), O(n^1)) 0.00/0.78 YES(O(1), O(n^1)) 0.00/0.80 0.00/0.80 0.00/0.80 0.00/0.80 0.00/0.80 0.00/0.80 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.80 0.00/0.80 0.00/0.80
0.00/0.80 0.00/0.80 0.00/0.80
0.00/0.80
0.00/0.80

(0) Obligation:

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

f(f(X)) → c(n__f(n__g(n__f(X)))) 0.00/0.80
c(X) → d(activate(X)) 0.00/0.80
h(X) → c(n__d(X)) 0.00/0.80
f(X) → n__f(X) 0.00/0.80
g(X) → n__g(X) 0.00/0.80
d(X) → n__d(X) 0.00/0.80
activate(n__f(X)) → f(activate(X)) 0.00/0.80
activate(n__g(X)) → g(X) 0.00/0.80
activate(n__d(X)) → d(X) 0.00/0.80
activate(X) → X

Rewrite Strategy: INNERMOST
0.00/0.80
0.00/0.80

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

Converted CpxTRS to CDT
0.00/0.80
0.00/0.80

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
Tuples:

F(f(z0)) → c1(C(n__f(n__g(n__f(z0))))) 0.00/0.80
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.80
H(z0) → c4(C(n__d(z0))) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(F(activate(z0)), ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8(G(z0)) 0.00/0.80
ACTIVATE(n__d(z0)) → c9(D(z0))
S tuples:

F(f(z0)) → c1(C(n__f(n__g(n__f(z0))))) 0.00/0.80
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.80
H(z0) → c4(C(n__d(z0))) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(F(activate(z0)), ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8(G(z0)) 0.00/0.80
ACTIVATE(n__d(z0)) → c9(D(z0))
K tuples:none
Defined Rule Symbols:

f, c, h, g, d, activate

Defined Pair Symbols:

F, C, H, ACTIVATE

Compound Symbols:

c1, c3, c4, c7, c8, c9

0.00/0.80
0.00/0.80

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

F(f(z0)) → c1(C(n__f(n__g(n__f(z0)))))
0.00/0.80
0.00/0.80

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
Tuples:

C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.80
H(z0) → c4(C(n__d(z0))) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(F(activate(z0)), ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8(G(z0)) 0.00/0.80
ACTIVATE(n__d(z0)) → c9(D(z0))
S tuples:

C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.80
H(z0) → c4(C(n__d(z0))) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(F(activate(z0)), ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8(G(z0)) 0.00/0.80
ACTIVATE(n__d(z0)) → c9(D(z0))
K tuples:none
Defined Rule Symbols:

f, c, h, g, d, activate

Defined Pair Symbols:

C, H, ACTIVATE

Compound Symbols:

c3, c4, c7, c8, c9

0.00/0.80
0.00/0.80

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

Removed 4 trailing tuple parts
0.00/0.80
0.00/0.80

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
Tuples:

H(z0) → c4(C(n__d(z0))) 0.00/0.80
C(z0) → c3(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
S tuples:

H(z0) → c4(C(n__d(z0))) 0.00/0.80
C(z0) → c3(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
K tuples:none
Defined Rule Symbols:

f, c, h, g, d, activate

Defined Pair Symbols:

H, C, ACTIVATE

Compound Symbols:

c4, c3, c7, c8, c9

0.00/0.80
0.00/0.80

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

H(z0) → c4(C(n__d(z0))) 0.00/0.80
C(z0) → c3(ACTIVATE(z0))
Removed 2 trailing nodes:

ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
0.00/0.80
0.00/0.80

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
Tuples:

ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
S tuples:

ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
K tuples:none
Defined Rule Symbols:

f, c, h, g, d, activate

Defined Pair Symbols:

ACTIVATE

Compound Symbols:

c7, c8, c9

0.00/0.80
0.00/0.80

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

ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
We considered the (Usable) Rules:none
And the Tuples:

ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
The order we found is given by the following interpretation:
Polynomial interpretation : 0.00/0.80

POL(ACTIVATE(x1)) = [1]    0.00/0.80
POL(c7(x1)) = x1    0.00/0.80
POL(c8) = 0    0.00/0.80
POL(c9) = 0    0.00/0.80
POL(n__d(x1)) = [1]    0.00/0.80
POL(n__f(x1)) = [1] + x1    0.00/0.80
POL(n__g(x1)) = [1]   
0.00/0.80
0.00/0.80

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
Tuples:

ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
S tuples:

ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0))
K tuples:

ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
Defined Rule Symbols:

f, c, h, g, d, activate

Defined Pair Symbols:

ACTIVATE

Compound Symbols:

c7, c8, c9

0.00/0.80
0.00/0.80

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

ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0))
We considered the (Usable) Rules:none
And the Tuples:

ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
The order we found is given by the following interpretation:
Polynomial interpretation : 0.00/0.80

POL(ACTIVATE(x1)) = [3]x1    0.00/0.80
POL(c7(x1)) = x1    0.00/0.80
POL(c8) = 0    0.00/0.80
POL(c9) = 0    0.00/0.80
POL(n__d(x1)) = 0    0.00/0.80
POL(n__f(x1)) = [1] + x1    0.00/0.80
POL(n__g(x1)) = 0   
0.00/0.80
0.00/0.80

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
Tuples:

ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
S tuples:none
K tuples:

ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9 0.00/0.80
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0))
Defined Rule Symbols:

f, c, h, g, d, activate

Defined Pair Symbols:

ACTIVATE

Compound Symbols:

c7, c8, c9

0.00/0.80
0.00/0.80

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

The set S is empty
0.00/0.80
0.00/0.80

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

0.00/0.80
0.00/0.80
0.00/0.83 EOF