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

(0) Obligation:

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

a__ca__f(g(c)) 0.00/0.56
a__f(g(X)) → g(X) 0.00/0.56
mark(c) → a__c 0.00/0.56
mark(f(X)) → a__f(X) 0.00/0.56
mark(g(X)) → g(X) 0.00/0.56
a__cc 0.00/0.56
a__f(X) → f(X)

Rewrite Strategy: INNERMOST
0.00/0.56
0.00/0.56

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

Converted CpxTRS to CDT
0.00/0.56
0.00/0.56

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__ca__f(g(c)) 0.00/0.56
a__cc 0.00/0.56
a__f(g(z0)) → g(z0) 0.00/0.56
a__f(z0) → f(z0) 0.00/0.56
mark(c) → a__c 0.00/0.56
mark(f(z0)) → a__f(z0) 0.00/0.56
mark(g(z0)) → g(z0)
Tuples:

A__Cc1(A__F(g(c))) 0.00/0.56
MARK(c) → c5(A__C) 0.00/0.56
MARK(f(z0)) → c6(A__F(z0))
S tuples:

A__Cc1(A__F(g(c))) 0.00/0.56
MARK(c) → c5(A__C) 0.00/0.56
MARK(f(z0)) → c6(A__F(z0))
K tuples:none
Defined Rule Symbols:

a__c, a__f, mark

Defined Pair Symbols:

A__C, MARK

Compound Symbols:

c1, c5, c6

0.00/0.56
0.00/0.56

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

Removed 2 trailing tuple parts
0.00/0.56
0.00/0.56

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__ca__f(g(c)) 0.00/0.56
a__cc 0.00/0.56
a__f(g(z0)) → g(z0) 0.00/0.56
a__f(z0) → f(z0) 0.00/0.56
mark(c) → a__c 0.00/0.56
mark(f(z0)) → a__f(z0) 0.00/0.56
mark(g(z0)) → g(z0)
Tuples:

MARK(c) → c5(A__C) 0.00/0.56
A__Cc1 0.00/0.56
MARK(f(z0)) → c6
S tuples:

MARK(c) → c5(A__C) 0.00/0.56
A__Cc1 0.00/0.56
MARK(f(z0)) → c6
K tuples:none
Defined Rule Symbols:

a__c, a__f, mark

Defined Pair Symbols:

MARK, A__C

Compound Symbols:

c5, c1, c6

0.00/0.56
0.00/0.56

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

Removed 3 trailing nodes:

MARK(f(z0)) → c6 0.00/0.56
A__Cc1 0.00/0.56
MARK(c) → c5(A__C)
0.00/0.56
0.00/0.56

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__ca__f(g(c)) 0.00/0.56
a__cc 0.00/0.56
a__f(g(z0)) → g(z0) 0.00/0.56
a__f(z0) → f(z0) 0.00/0.56
mark(c) → a__c 0.00/0.56
mark(f(z0)) → a__f(z0) 0.00/0.56
mark(g(z0)) → g(z0)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

a__c, a__f, mark

Defined Pair Symbols:none

Compound Symbols:none

0.00/0.56
0.00/0.56

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

The set S is empty
0.00/0.56
0.00/0.56

(8) BOUNDS(O(1), O(1))

0.00/0.56
0.00/0.56
0.00/0.58 EOF