YES(O(1), O(1)) 0.00/0.55 YES(O(1), O(1)) 0.00/0.57 0.00/0.57 0.00/0.57 0.00/0.57 0.00/0.58 0.00/0.58 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.58 0.00/0.58 0.00/0.58
0.00/0.58 0.00/0.58 0.00/0.58
0.00/0.58
0.00/0.58

(0) Obligation:

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

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

Rewrite Strategy: INNERMOST
0.00/0.58
0.00/0.58

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

Converted CpxTRS to CDT
0.00/0.58
0.00/0.58

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

F(f(z0)) → c1(C(n__f(g(n__f(z0))))) 0.00/0.58
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
ACTIVATE(n__f(z0)) → c6(F(z0)) 0.00/0.58
ACTIVATE(n__d(z0)) → c7(D(z0))
S tuples:

F(f(z0)) → c1(C(n__f(g(n__f(z0))))) 0.00/0.58
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
ACTIVATE(n__f(z0)) → c6(F(z0)) 0.00/0.58
ACTIVATE(n__d(z0)) → c7(D(z0))
K tuples:none
Defined Rule Symbols:

f, c, h, d, activate

Defined Pair Symbols:

F, C, H, ACTIVATE

Compound Symbols:

c1, c3, c4, c6, c7

0.00/0.58
0.00/0.58

(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(g(n__f(z0)))))
0.00/0.58
0.00/0.58

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
ACTIVATE(n__f(z0)) → c6(F(z0)) 0.00/0.58
ACTIVATE(n__d(z0)) → c7(D(z0))
S tuples:

C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
ACTIVATE(n__f(z0)) → c6(F(z0)) 0.00/0.58
ACTIVATE(n__d(z0)) → c7(D(z0))
K tuples:none
Defined Rule Symbols:

f, c, h, d, activate

Defined Pair Symbols:

C, H, ACTIVATE

Compound Symbols:

c3, c4, c6, c7

0.00/0.58
0.00/0.58

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

Removed 3 trailing tuple parts
0.00/0.58
0.00/0.58

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

H(z0) → c4(C(n__d(z0))) 0.00/0.58
C(z0) → c3(ACTIVATE(z0)) 0.00/0.58
ACTIVATE(n__f(z0)) → c6 0.00/0.58
ACTIVATE(n__d(z0)) → c7
S tuples:

H(z0) → c4(C(n__d(z0))) 0.00/0.58
C(z0) → c3(ACTIVATE(z0)) 0.00/0.58
ACTIVATE(n__f(z0)) → c6 0.00/0.58
ACTIVATE(n__d(z0)) → c7
K tuples:none
Defined Rule Symbols:

f, c, h, d, activate

Defined Pair Symbols:

H, C, ACTIVATE

Compound Symbols:

c4, c3, c6, c7

0.00/0.58
0.00/0.58

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

Removed 4 trailing nodes:

ACTIVATE(n__f(z0)) → c6 0.00/0.58
ACTIVATE(n__d(z0)) → c7 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
C(z0) → c3(ACTIVATE(z0))
0.00/0.58
0.00/0.58

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(f(z0)) → c(n__f(g(n__f(z0)))) 0.00/0.58
f(z0) → n__f(z0) 0.00/0.58
c(z0) → d(activate(z0)) 0.00/0.58
h(z0) → c(n__d(z0)) 0.00/0.58
d(z0) → n__d(z0) 0.00/0.58
activate(n__f(z0)) → f(z0) 0.00/0.58
activate(n__d(z0)) → d(z0) 0.00/0.58
activate(z0) → z0
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

f, c, h, d, activate

Defined Pair Symbols:none

Compound Symbols:none

0.00/0.58
0.00/0.58

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

The set S is empty
0.00/0.58
0.00/0.58

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

0.00/0.58
0.00/0.58
0.00/0.59 EOF