MAYBE 8.04/2.83 MAYBE 8.04/2.84 8.04/2.84 8.04/2.84 8.04/2.84 8.04/2.84 8.04/2.84 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 8.04/2.84 8.04/2.84 8.04/2.84
8.04/2.84
8.04/2.84
8.04/2.84
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
8.04/2.84 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
8.04/2.84 
↳2 CdtProblem
8.04/2.84 
↳3 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
8.04/2.84 
↳4 CdtProblem
8.04/2.84 
↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
8.04/2.84 
↳6 CdtProblem
8.04/2.84 
↳7 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
8.04/2.84 
↳8 CdtProblem
8.04/2.84 
↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
8.04/2.84 
↳10 CdtProblem
8.04/2.84
8.04/2.84 8.04/2.84
8.04/2.84
8.04/2.84

(0) Obligation:

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

f(s(x), y) → f(x, s(x)) 8.04/2.84
f(x, s(y)) → f(y, x)

Rewrite Strategy: INNERMOST
8.04/2.84
8.04/2.84

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

Converted CpxTRS to CDT
8.04/2.84
8.04/2.84

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(z0)) 8.04/2.84
f(z0, s(z1)) → f(z1, z0)
Tuples:

F(s(z0), z1) → c(F(z0, s(z0))) 8.04/2.84
F(z0, s(z1)) → c1(F(z1, z0))
S tuples:

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

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

8.04/2.84
8.04/2.84

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

Use forward instantiation to replace F(z0, s(z1)) → c1(F(z1, z0)) by

F(z0, s(s(y0))) → c1(F(s(y0), z0)) 8.04/2.84
F(s(y1), s(z1)) → c1(F(z1, s(y1)))
8.04/2.84
8.04/2.84

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(z0)) 8.04/2.84
f(z0, s(z1)) → f(z1, z0)
Tuples:

F(s(z0), z1) → c(F(z0, s(z0))) 8.04/2.84
F(z0, s(s(y0))) → c1(F(s(y0), z0)) 8.04/2.85
F(s(y1), s(z1)) → c1(F(z1, s(y1)))
S tuples:

F(s(z0), z1) → c(F(z0, s(z0))) 8.04/2.85
F(z0, s(s(y0))) → c1(F(s(y0), z0)) 8.04/2.85
F(s(y1), s(z1)) → c1(F(z1, s(y1)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

8.04/2.85
8.04/2.85

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

Use forward instantiation to replace F(s(z0), z1) → c(F(z0, s(z0))) by

F(s(s(y0)), z1) → c(F(s(y0), s(s(y0))))
8.04/2.85
8.04/2.85

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(z0)) 8.04/2.85
f(z0, s(z1)) → f(z1, z0)
Tuples:

F(z0, s(s(y0))) → c1(F(s(y0), z0)) 8.04/2.85
F(s(y1), s(z1)) → c1(F(z1, s(y1))) 8.04/2.85
F(s(s(y0)), z1) → c(F(s(y0), s(s(y0))))
S tuples:

F(z0, s(s(y0))) → c1(F(s(y0), z0)) 8.04/2.85
F(s(y1), s(z1)) → c1(F(z1, s(y1))) 8.04/2.85
F(s(s(y0)), z1) → c(F(s(y0), s(s(y0))))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

8.04/2.85
8.04/2.85

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

Use forward instantiation to replace F(z0, s(s(y0))) → c1(F(s(y0), z0)) by

F(s(s(y1)), s(s(z1))) → c1(F(s(z1), s(s(y1)))) 8.04/2.85
F(s(y1), s(s(z1))) → c1(F(s(z1), s(y1))) 8.04/2.85
F(z0, s(s(s(y0)))) → c1(F(s(s(y0)), z0))
8.04/2.85
8.04/2.85

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(z0)) 8.04/2.85
f(z0, s(z1)) → f(z1, z0)
Tuples:

F(s(y1), s(z1)) → c1(F(z1, s(y1))) 8.04/2.85
F(s(s(y0)), z1) → c(F(s(y0), s(s(y0)))) 8.04/2.85
F(s(s(y1)), s(s(z1))) → c1(F(s(z1), s(s(y1)))) 8.04/2.85
F(s(y1), s(s(z1))) → c1(F(s(z1), s(y1))) 8.04/2.85
F(z0, s(s(s(y0)))) → c1(F(s(s(y0)), z0))
S tuples:

F(s(y1), s(z1)) → c1(F(z1, s(y1))) 8.04/2.85
F(s(s(y0)), z1) → c(F(s(y0), s(s(y0)))) 8.04/2.85
F(s(s(y1)), s(s(z1))) → c1(F(s(z1), s(s(y1)))) 8.04/2.85
F(s(y1), s(s(z1))) → c1(F(s(z1), s(y1))) 8.04/2.85
F(z0, s(s(s(y0)))) → c1(F(s(s(y0)), z0))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

8.04/2.85
8.04/2.85

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

Use forward instantiation to replace F(s(y1), s(z1)) → c1(F(z1, s(y1))) by

F(s(z0), s(s(y0))) → c1(F(s(y0), s(z0))) 8.04/2.85
F(s(z0), s(s(s(y0)))) → c1(F(s(s(y0)), s(z0))) 8.04/2.85
F(s(s(y1)), s(s(s(y0)))) → c1(F(s(s(y0)), s(s(y1)))) 8.04/2.85
F(s(s(y1)), s(s(y0))) → c1(F(s(y0), s(s(y1)))) 8.04/2.85
F(s(s(s(y1))), s(z1)) → c1(F(z1, s(s(s(y1)))))
8.04/2.85
8.04/2.85

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(z0)) 8.04/2.85
f(z0, s(z1)) → f(z1, z0)
Tuples:

F(s(s(y0)), z1) → c(F(s(y0), s(s(y0)))) 8.04/2.85
F(s(s(y1)), s(s(z1))) → c1(F(s(z1), s(s(y1)))) 8.04/2.85
F(s(y1), s(s(z1))) → c1(F(s(z1), s(y1))) 8.04/2.85
F(z0, s(s(s(y0)))) → c1(F(s(s(y0)), z0)) 8.04/2.85
F(s(z0), s(s(s(y0)))) → c1(F(s(s(y0)), s(z0))) 8.04/2.85
F(s(s(y1)), s(s(s(y0)))) → c1(F(s(s(y0)), s(s(y1)))) 8.04/2.85
F(s(s(s(y1))), s(z1)) → c1(F(z1, s(s(s(y1)))))
S tuples:

F(s(s(y0)), z1) → c(F(s(y0), s(s(y0)))) 8.04/2.85
F(s(s(y1)), s(s(z1))) → c1(F(s(z1), s(s(y1)))) 8.04/2.85
F(s(y1), s(s(z1))) → c1(F(s(z1), s(y1))) 8.04/2.85
F(z0, s(s(s(y0)))) → c1(F(s(s(y0)), z0)) 8.04/2.85
F(s(z0), s(s(s(y0)))) → c1(F(s(s(y0)), s(z0))) 8.04/2.85
F(s(s(y1)), s(s(s(y0)))) → c1(F(s(s(y0)), s(s(y1)))) 8.04/2.85
F(s(s(s(y1))), s(z1)) → c1(F(z1, s(s(s(y1)))))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

8.04/2.85
8.04/2.85
8.65/2.90 EOF