MAYBE 0.00/0.81 MAYBE 0.00/0.82 0.00/0.82 0.00/0.82 0.00/0.82 0.00/0.82 0.00/0.82 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.82 0.00/0.82 0.00/0.82
0.00/0.82 0.00/0.82 0.00/0.82
0.00/0.82
0.00/0.82

(0) Obligation:

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

f(x, y) → f(x, x) 0.00/0.82
f(s(x), y) → f(y, x)

Rewrite Strategy: INNERMOST
0.00/0.82
0.00/0.82

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

Converted CpxTRS to CDT
0.00/0.82
0.00/0.82

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1) → f(z0, z0) 0.00/0.82
f(s(z0), z1) → f(z1, z0)
Tuples:

F(z0, z1) → c(F(z0, z0)) 0.00/0.82
F(s(z0), z1) → c1(F(z1, z0))
S tuples:

F(z0, z1) → c(F(z0, z0)) 0.00/0.82
F(s(z0), z1) → c1(F(z1, z0))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

0.00/0.82
0.00/0.82
0.00/0.85 EOF