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

0 CpxTRS
4.18/2.11 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
4.18/2.11 
↳2 CdtProblem
4.18/2.11 
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)
4.18/2.11 
↳4 CdtProblem
4.18/2.11
4.18/2.11 4.18/2.11
4.18/2.11
4.18/2.11

(0) Obligation:

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

g(Cons(x, xs), y) → Cons(x, xs) 4.18/2.11
h(Nil, y) → h(Nil, y) 4.18/2.11
h(Cons(x, xs), y) → f(Cons(x, xs), y) 4.18/2.11
g(Nil, y) → h(Nil, y) 4.18/2.11
f(Nil, y) → g(Nil, y) 4.18/2.11
f(Cons(x, xs), y) → h(Cons(x, xs), y) 4.18/2.11
sp1(x, y) → f(x, y) 4.18/2.11
r(x, y) → x

Rewrite Strategy: INNERMOST
4.18/2.11
4.18/2.11

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

Converted CpxTRS to CDT
4.18/2.11
4.18/2.11

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(Cons(z0, z1), z2) → Cons(z0, z1) 4.18/2.11
g(Nil, z0) → h(Nil, z0) 4.18/2.11
h(Nil, z0) → h(Nil, z0) 4.18/2.11
h(Cons(z0, z1), z2) → f(Cons(z0, z1), z2) 4.18/2.11
f(Nil, z0) → g(Nil, z0) 4.18/2.11
f(Cons(z0, z1), z2) → h(Cons(z0, z1), z2) 4.18/2.11
sp1(z0, z1) → f(z0, z1) 4.18/2.11
r(z0, z1) → z0
Tuples:

G(Nil, z0) → c1(H(Nil, z0)) 4.18/2.11
H(Nil, z0) → c2(H(Nil, z0)) 4.18/2.11
H(Cons(z0, z1), z2) → c3(F(Cons(z0, z1), z2)) 4.18/2.11
F(Nil, z0) → c4(G(Nil, z0)) 4.18/2.11
F(Cons(z0, z1), z2) → c5(H(Cons(z0, z1), z2)) 4.18/2.11
SP1(z0, z1) → c6(F(z0, z1))
S tuples:

G(Nil, z0) → c1(H(Nil, z0)) 4.18/2.11
H(Nil, z0) → c2(H(Nil, z0)) 4.18/2.11
H(Cons(z0, z1), z2) → c3(F(Cons(z0, z1), z2)) 4.18/2.11
F(Nil, z0) → c4(G(Nil, z0)) 4.18/2.11
F(Cons(z0, z1), z2) → c5(H(Cons(z0, z1), z2)) 4.18/2.11
SP1(z0, z1) → c6(F(z0, z1))
K tuples:none
Defined Rule Symbols:

g, h, f, sp1, r

Defined Pair Symbols:

G, H, F, SP1

Compound Symbols:

c1, c2, c3, c4, c5, c6

4.18/2.11
4.18/2.11

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 3 leading nodes:

SP1(z0, z1) → c6(F(z0, z1)) 4.18/2.11
F(Nil, z0) → c4(G(Nil, z0)) 4.18/2.11
G(Nil, z0) → c1(H(Nil, z0))
4.18/2.11
4.18/2.11

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(Cons(z0, z1), z2) → Cons(z0, z1) 4.18/2.11
g(Nil, z0) → h(Nil, z0) 4.18/2.11
h(Nil, z0) → h(Nil, z0) 4.18/2.11
h(Cons(z0, z1), z2) → f(Cons(z0, z1), z2) 4.18/2.11
f(Nil, z0) → g(Nil, z0) 4.18/2.11
f(Cons(z0, z1), z2) → h(Cons(z0, z1), z2) 4.18/2.11
sp1(z0, z1) → f(z0, z1) 4.18/2.11
r(z0, z1) → z0
Tuples:

H(Nil, z0) → c2(H(Nil, z0)) 4.18/2.11
H(Cons(z0, z1), z2) → c3(F(Cons(z0, z1), z2)) 4.18/2.11
F(Cons(z0, z1), z2) → c5(H(Cons(z0, z1), z2))
S tuples:

H(Nil, z0) → c2(H(Nil, z0)) 4.18/2.11
H(Cons(z0, z1), z2) → c3(F(Cons(z0, z1), z2)) 4.18/2.11
F(Cons(z0, z1), z2) → c5(H(Cons(z0, z1), z2))
K tuples:none
Defined Rule Symbols:

g, h, f, sp1, r

Defined Pair Symbols:

H, F

Compound Symbols:

c2, c3, c5

4.18/2.11
4.18/2.11
4.18/2.14 EOF