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

0 CpxTRS
21.30/8.23 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
21.30/8.23 
↳2 CdtProblem
21.30/8.23 
↳3 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
21.30/8.23 
↳4 CdtProblem
21.30/8.23 
↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
21.30/8.23 
↳6 CdtProblem
21.30/8.23 
↳7 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
21.30/8.23 
↳8 CdtProblem
21.30/8.23 
↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
21.30/8.23 
↳10 CdtProblem
21.30/8.23 
↳11 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
21.30/8.23 
↳12 CdtProblem
21.30/8.23
21.30/8.23 21.30/8.23
21.30/8.23
21.30/8.23

(0) Obligation:

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

f(s(x), y) → f(x, s(s(x))) 21.30/8.23
f(x, s(s(y))) → f(y, x)

Rewrite Strategy: INNERMOST
21.30/8.23
21.30/8.23

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

Converted CpxTRS to CDT
21.30/8.23
21.30/8.23

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(s(z0))) 21.30/8.23
f(z0, s(s(z1))) → f(z1, z0)
Tuples:

F(s(z0), z1) → c(F(z0, s(s(z0)))) 21.30/8.23
F(z0, s(s(z1))) → c1(F(z1, z0))
S tuples:

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

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

21.30/8.23
21.30/8.23

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

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

F(z0, s(s(s(y0)))) → c1(F(s(y0), z0)) 21.30/8.23
F(s(s(y1)), s(s(z1))) → c1(F(z1, s(s(y1))))
21.30/8.23
21.30/8.23

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(s(z0))) 21.30/8.23
f(z0, s(s(z1))) → f(z1, z0)
Tuples:

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

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

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

21.30/8.23
21.30/8.23

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

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

F(s(s(y0)), z1) → c(F(s(y0), s(s(s(y0))))) 21.30/8.23
F(s(s(s(y0))), z1) → c(F(s(s(y0)), s(s(s(s(y0))))))
21.30/8.23
21.30/8.23

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(s(z0))) 21.30/8.23
f(z0, s(s(z1))) → f(z1, z0)
Tuples:

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

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

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

21.30/8.23
21.30/8.23

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

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

F(s(s(s(y1))), s(s(s(z1)))) → c1(F(s(z1), s(s(s(y1))))) 21.30/8.23
F(s(s(y1)), s(s(s(s(y0))))) → c1(F(s(s(y0)), s(s(y1)))) 21.30/8.23
F(z0, s(s(s(s(y0))))) → c1(F(s(s(y0)), z0)) 21.30/8.23
F(z0, s(s(s(s(s(y0)))))) → c1(F(s(s(s(y0))), z0))
21.30/8.23
21.30/8.23

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(s(z0))) 21.30/8.23
f(z0, s(s(z1))) → f(z1, z0)
Tuples:

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

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

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c

21.30/8.23
21.30/8.23

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

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

F(s(s(z0)), s(s(s(s(y0))))) → c1(F(s(s(y0)), s(s(z0)))) 21.30/8.23
F(s(s(z0)), s(s(s(s(s(y0)))))) → c1(F(s(s(s(y0))), s(s(z0)))) 21.30/8.23
F(s(s(s(y1))), s(s(s(s(s(y0)))))) → c1(F(s(s(s(y0))), s(s(s(y1))))) 21.30/8.23
F(s(s(s(s(y1)))), s(s(s(s(y0))))) → c1(F(s(s(y0)), s(s(s(s(y1)))))) 21.30/8.23
F(s(s(s(s(y1)))), s(s(z1))) → c1(F(z1, s(s(s(s(y1)))))) 21.30/8.23
F(s(s(s(s(s(y1))))), s(s(z1))) → c1(F(z1, s(s(s(s(s(y1)))))))
21.30/8.23
21.30/8.23

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(s(z0))) 21.30/8.23
f(z0, s(s(z1))) → f(z1, z0)
Tuples:

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

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

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

21.30/8.24
21.30/8.24

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

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

F(s(s(s(y0))), z1) → c(F(s(s(y0)), s(s(s(s(y0)))))) 21.30/8.24
F(s(s(s(s(y0)))), z1) → c(F(s(s(s(y0))), s(s(s(s(s(y0))))))) 21.30/8.24
F(s(s(s(s(s(y0))))), z1) → c(F(s(s(s(s(y0)))), s(s(s(s(s(s(y0)))))))) 21.30/8.24
F(s(s(s(s(s(s(y0)))))), z1) → c(F(s(s(s(s(s(y0))))), s(s(s(s(s(s(s(y0)))))))))
21.30/8.24
21.30/8.24

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1) → f(z0, s(s(z0))) 21.30/8.24
f(z0, s(s(z1))) → f(z1, z0)
Tuples:

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

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

f

Defined Pair Symbols:

F

Compound Symbols:

c, c1

21.30/8.24
21.30/8.24
21.30/8.27 EOF