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

0 CpxTRS
18.57/9.09 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
18.57/9.09 
↳2 CdtProblem
18.57/9.09 
↳3 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
18.57/9.09 
↳4 CdtProblem
18.57/9.09 
↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
18.57/9.09 
↳6 CdtProblem
18.57/9.09 
↳7 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
18.57/9.09 
↳8 CdtProblem
18.57/9.09
18.57/9.09 18.57/9.09
18.57/9.09
18.57/9.09

(0) Obligation:

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

fib(0) → 0 18.57/9.09
fib(s(0)) → s(0) 18.57/9.09
fib(s(s(x))) → +(fib(s(x)), fib(x))

Rewrite Strategy: INNERMOST
18.57/9.09
18.57/9.09

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

Converted CpxTRS to CDT
18.57/9.09
18.57/9.09

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(0) → 0 18.57/9.09
fib(s(0)) → s(0) 18.57/9.09
fib(s(s(z0))) → +(fib(s(z0)), fib(z0))
Tuples:

FIB(s(s(z0))) → c2(FIB(s(z0)), FIB(z0))
S tuples:

FIB(s(s(z0))) → c2(FIB(s(z0)), FIB(z0))
K tuples:none
Defined Rule Symbols:

fib

Defined Pair Symbols:

FIB

Compound Symbols:

c2

18.57/9.09
18.57/9.09

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

Use forward instantiation to replace FIB(s(s(z0))) → c2(FIB(s(z0)), FIB(z0)) by

FIB(s(s(s(y0)))) → c2(FIB(s(s(y0))), FIB(s(y0))) 18.57/9.09
FIB(s(s(s(s(y0))))) → c2(FIB(s(s(s(y0)))), FIB(s(s(y0))))
18.57/9.09
18.57/9.09

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(0) → 0 18.57/9.09
fib(s(0)) → s(0) 18.57/9.09
fib(s(s(z0))) → +(fib(s(z0)), fib(z0))
Tuples:

FIB(s(s(s(y0)))) → c2(FIB(s(s(y0))), FIB(s(y0))) 18.57/9.09
FIB(s(s(s(s(y0))))) → c2(FIB(s(s(s(y0)))), FIB(s(s(y0))))
S tuples:

FIB(s(s(s(y0)))) → c2(FIB(s(s(y0))), FIB(s(y0))) 18.57/9.10
FIB(s(s(s(s(y0))))) → c2(FIB(s(s(s(y0)))), FIB(s(s(y0))))
K tuples:none
Defined Rule Symbols:

fib

Defined Pair Symbols:

FIB

Compound Symbols:

c2

18.57/9.10
18.57/9.10

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

Use forward instantiation to replace FIB(s(s(s(y0)))) → c2(FIB(s(s(y0))), FIB(s(y0))) by

FIB(s(s(s(s(y0))))) → c2(FIB(s(s(s(y0)))), FIB(s(s(y0)))) 18.57/9.10
FIB(s(s(s(s(s(y0)))))) → c2(FIB(s(s(s(s(y0))))), FIB(s(s(s(y0))))) 18.57/9.10
FIB(s(s(s(s(s(s(y0))))))) → c2(FIB(s(s(s(s(s(y0)))))), FIB(s(s(s(s(y0))))))
18.57/9.10
18.57/9.10

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(0) → 0 18.57/9.10
fib(s(0)) → s(0) 18.57/9.10
fib(s(s(z0))) → +(fib(s(z0)), fib(z0))
Tuples:

FIB(s(s(s(s(y0))))) → c2(FIB(s(s(s(y0)))), FIB(s(s(y0)))) 18.57/9.10
FIB(s(s(s(s(s(y0)))))) → c2(FIB(s(s(s(s(y0))))), FIB(s(s(s(y0))))) 18.57/9.10
FIB(s(s(s(s(s(s(y0))))))) → c2(FIB(s(s(s(s(s(y0)))))), FIB(s(s(s(s(y0))))))
S tuples:

FIB(s(s(s(s(y0))))) → c2(FIB(s(s(s(y0)))), FIB(s(s(y0)))) 18.57/9.10
FIB(s(s(s(s(s(y0)))))) → c2(FIB(s(s(s(s(y0))))), FIB(s(s(s(y0))))) 18.57/9.10
FIB(s(s(s(s(s(s(y0))))))) → c2(FIB(s(s(s(s(s(y0)))))), FIB(s(s(s(s(y0))))))
K tuples:none
Defined Rule Symbols:

fib

Defined Pair Symbols:

FIB

Compound Symbols:

c2

18.57/9.10
18.57/9.10

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

Use forward instantiation to replace FIB(s(s(s(s(y0))))) → c2(FIB(s(s(s(y0)))), FIB(s(s(y0)))) by

FIB(s(s(s(s(s(y0)))))) → c2(FIB(s(s(s(s(y0))))), FIB(s(s(s(y0))))) 18.57/9.10
FIB(s(s(s(s(s(s(y0))))))) → c2(FIB(s(s(s(s(s(y0)))))), FIB(s(s(s(s(y0)))))) 18.57/9.10
FIB(s(s(s(s(s(s(s(y0)))))))) → c2(FIB(s(s(s(s(s(s(y0))))))), FIB(s(s(s(s(s(y0))))))) 18.57/9.10
FIB(s(s(s(s(s(s(s(s(y0))))))))) → c2(FIB(s(s(s(s(s(s(s(y0)))))))), FIB(s(s(s(s(s(s(y0))))))))
18.57/9.10
18.57/9.10

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(0) → 0 18.57/9.10
fib(s(0)) → s(0) 18.57/9.10
fib(s(s(z0))) → +(fib(s(z0)), fib(z0))
Tuples:

FIB(s(s(s(s(y0))))) → c2(FIB(s(s(s(y0)))), FIB(s(s(y0)))) 18.57/9.10
FIB(s(s(s(s(s(y0)))))) → c2(FIB(s(s(s(s(y0))))), FIB(s(s(s(y0))))) 18.57/9.10
FIB(s(s(s(s(s(s(y0))))))) → c2(FIB(s(s(s(s(s(y0)))))), FIB(s(s(s(s(y0)))))) 18.57/9.10
FIB(s(s(s(s(s(s(s(y0)))))))) → c2(FIB(s(s(s(s(s(s(y0))))))), FIB(s(s(s(s(s(y0))))))) 18.57/9.10
FIB(s(s(s(s(s(s(s(s(y0))))))))) → c2(FIB(s(s(s(s(s(s(s(y0)))))))), FIB(s(s(s(s(s(s(y0))))))))
S tuples:

FIB(s(s(s(s(s(y0)))))) → c2(FIB(s(s(s(s(y0))))), FIB(s(s(s(y0))))) 18.57/9.10
FIB(s(s(s(s(s(s(y0))))))) → c2(FIB(s(s(s(s(s(y0)))))), FIB(s(s(s(s(y0)))))) 18.57/9.10
FIB(s(s(s(s(s(s(s(y0)))))))) → c2(FIB(s(s(s(s(s(s(y0))))))), FIB(s(s(s(s(s(y0))))))) 18.57/9.10
FIB(s(s(s(s(s(s(s(s(y0))))))))) → c2(FIB(s(s(s(s(s(s(s(y0)))))))), FIB(s(s(s(s(s(s(y0))))))))
K tuples:none
Defined Rule Symbols:

fib

Defined Pair Symbols:

FIB

Compound Symbols:

c2

18.57/9.10
18.57/9.10
18.69/9.12 EOF