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

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

(0) Obligation:

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

bin(x, 0) → s(0) 15.09/6.23
bin(0, s(y)) → 0 15.09/6.23
bin(s(x), s(y)) → +(bin(x, s(y)), bin(x, y))

Rewrite Strategy: INNERMOST
15.09/6.23
15.09/6.23

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

Converted CpxTRS to CDT
15.09/6.23
15.09/6.23

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

bin(z0, 0) → s(0) 15.09/6.23
bin(0, s(z0)) → 0 15.09/6.23
bin(s(z0), s(z1)) → +(bin(z0, s(z1)), bin(z0, z1))
Tuples:

BIN(s(z0), s(z1)) → c2(BIN(z0, s(z1)), BIN(z0, z1))
S tuples:

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

bin

Defined Pair Symbols:

BIN

Compound Symbols:

c2

15.09/6.23
15.09/6.23

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

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

BIN(s(s(y0)), s(z1)) → c2(BIN(s(y0), s(z1)), BIN(s(y0), z1)) 15.09/6.23
BIN(s(s(y0)), s(s(y1))) → c2(BIN(s(y0), s(s(y1))), BIN(s(y0), s(y1)))
15.09/6.23
15.09/6.23

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

bin(z0, 0) → s(0) 15.09/6.23
bin(0, s(z0)) → 0 15.09/6.23
bin(s(z0), s(z1)) → +(bin(z0, s(z1)), bin(z0, z1))
Tuples:

BIN(s(s(y0)), s(z1)) → c2(BIN(s(y0), s(z1)), BIN(s(y0), z1)) 15.09/6.23
BIN(s(s(y0)), s(s(y1))) → c2(BIN(s(y0), s(s(y1))), BIN(s(y0), s(y1)))
S tuples:

BIN(s(s(y0)), s(z1)) → c2(BIN(s(y0), s(z1)), BIN(s(y0), z1)) 15.09/6.23
BIN(s(s(y0)), s(s(y1))) → c2(BIN(s(y0), s(s(y1))), BIN(s(y0), s(y1)))
K tuples:none
Defined Rule Symbols:

bin

Defined Pair Symbols:

BIN

Compound Symbols:

c2

15.09/6.23
15.09/6.23

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

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

BIN(s(s(s(y0))), s(z1)) → c2(BIN(s(s(y0)), s(z1)), BIN(s(s(y0)), z1)) 15.09/6.23
BIN(s(s(s(y0))), s(s(y1))) → c2(BIN(s(s(y0)), s(s(y1))), BIN(s(s(y0)), s(y1))) 15.09/6.23
BIN(s(s(s(y0))), s(s(s(y1)))) → c2(BIN(s(s(y0)), s(s(s(y1)))), BIN(s(s(y0)), s(s(y1))))
15.09/6.23
15.09/6.23

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

bin(z0, 0) → s(0) 15.09/6.23
bin(0, s(z0)) → 0 15.09/6.23
bin(s(z0), s(z1)) → +(bin(z0, s(z1)), bin(z0, z1))
Tuples:

BIN(s(s(y0)), s(s(y1))) → c2(BIN(s(y0), s(s(y1))), BIN(s(y0), s(y1))) 15.09/6.23
BIN(s(s(s(y0))), s(z1)) → c2(BIN(s(s(y0)), s(z1)), BIN(s(s(y0)), z1)) 15.09/6.23
BIN(s(s(s(y0))), s(s(y1))) → c2(BIN(s(s(y0)), s(s(y1))), BIN(s(s(y0)), s(y1))) 15.09/6.23
BIN(s(s(s(y0))), s(s(s(y1)))) → c2(BIN(s(s(y0)), s(s(s(y1)))), BIN(s(s(y0)), s(s(y1))))
S tuples:

BIN(s(s(y0)), s(s(y1))) → c2(BIN(s(y0), s(s(y1))), BIN(s(y0), s(y1))) 15.09/6.23
BIN(s(s(s(y0))), s(z1)) → c2(BIN(s(s(y0)), s(z1)), BIN(s(s(y0)), z1)) 15.09/6.23
BIN(s(s(s(y0))), s(s(y1))) → c2(BIN(s(s(y0)), s(s(y1))), BIN(s(s(y0)), s(y1))) 15.09/6.23
BIN(s(s(s(y0))), s(s(s(y1)))) → c2(BIN(s(s(y0)), s(s(s(y1)))), BIN(s(s(y0)), s(s(y1))))
K tuples:none
Defined Rule Symbols:

bin

Defined Pair Symbols:

BIN

Compound Symbols:

c2

15.09/6.23
15.09/6.23

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

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

BIN(s(s(s(y0))), s(s(z1))) → c2(BIN(s(s(y0)), s(s(z1))), BIN(s(s(y0)), s(z1))) 15.09/6.23
BIN(s(s(s(y0))), s(s(s(y1)))) → c2(BIN(s(s(y0)), s(s(s(y1)))), BIN(s(s(y0)), s(s(y1)))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(z1))) → c2(BIN(s(s(s(y0))), s(s(z1))), BIN(s(s(s(y0))), s(z1))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(s(y1)))) → c2(BIN(s(s(s(y0))), s(s(s(y1)))), BIN(s(s(s(y0))), s(s(y1)))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(s(s(y1))))) → c2(BIN(s(s(s(y0))), s(s(s(s(y1))))), BIN(s(s(s(y0))), s(s(s(y1)))))
15.09/6.23
15.09/6.23

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

bin(z0, 0) → s(0) 15.09/6.23
bin(0, s(z0)) → 0 15.09/6.23
bin(s(z0), s(z1)) → +(bin(z0, s(z1)), bin(z0, z1))
Tuples:

BIN(s(s(s(y0))), s(z1)) → c2(BIN(s(s(y0)), s(z1)), BIN(s(s(y0)), z1)) 15.09/6.23
BIN(s(s(s(y0))), s(s(y1))) → c2(BIN(s(s(y0)), s(s(y1))), BIN(s(s(y0)), s(y1))) 15.09/6.23
BIN(s(s(s(y0))), s(s(s(y1)))) → c2(BIN(s(s(y0)), s(s(s(y1)))), BIN(s(s(y0)), s(s(y1)))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(z1))) → c2(BIN(s(s(s(y0))), s(s(z1))), BIN(s(s(s(y0))), s(z1))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(s(y1)))) → c2(BIN(s(s(s(y0))), s(s(s(y1)))), BIN(s(s(s(y0))), s(s(y1)))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(s(s(y1))))) → c2(BIN(s(s(s(y0))), s(s(s(s(y1))))), BIN(s(s(s(y0))), s(s(s(y1)))))
S tuples:

BIN(s(s(s(y0))), s(z1)) → c2(BIN(s(s(y0)), s(z1)), BIN(s(s(y0)), z1)) 15.09/6.23
BIN(s(s(s(y0))), s(s(y1))) → c2(BIN(s(s(y0)), s(s(y1))), BIN(s(s(y0)), s(y1))) 15.09/6.23
BIN(s(s(s(y0))), s(s(s(y1)))) → c2(BIN(s(s(y0)), s(s(s(y1)))), BIN(s(s(y0)), s(s(y1)))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(z1))) → c2(BIN(s(s(s(y0))), s(s(z1))), BIN(s(s(s(y0))), s(z1))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(s(y1)))) → c2(BIN(s(s(s(y0))), s(s(s(y1)))), BIN(s(s(s(y0))), s(s(y1)))) 15.09/6.23
BIN(s(s(s(s(y0)))), s(s(s(s(y1))))) → c2(BIN(s(s(s(y0))), s(s(s(s(y1))))), BIN(s(s(s(y0))), s(s(s(y1)))))
K tuples:none
Defined Rule Symbols:

bin

Defined Pair Symbols:

BIN

Compound Symbols:

c2

15.09/6.23
15.09/6.23
15.09/6.26 EOF