YES(O(1), O(1)) 0.00/0.54 YES(O(1), O(1)) 0.00/0.55 0.00/0.55 0.00/0.55 0.00/0.55 0.00/0.55 0.00/0.55 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.55 0.00/0.55 0.00/0.55
0.00/0.55
0.00/0.55
0.00/0.55
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(1)).

0 CpxTRS
0.00/0.55 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
0.00/0.55 
↳2 CdtProblem
0.00/0.55 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
0.00/0.55 
↳4 CdtProblem
0.00/0.55 
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
0.00/0.55 
↳6 CdtProblem
0.00/0.55 
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))
0.00/0.55 
↳8 BOUNDS(O(1), O(1))
0.00/0.55
0.00/0.55 0.00/0.55
0.00/0.55
0.00/0.55

(0) Obligation:

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

app(nil, YS) → YS 0.00/0.55
app(cons(X), YS) → cons(X) 0.00/0.55
from(X) → cons(X) 0.00/0.55
zWadr(nil, YS) → nil 0.00/0.55
zWadr(XS, nil) → nil 0.00/0.55
zWadr(cons(X), cons(Y)) → cons(app(Y, cons(X))) 0.00/0.55
prefix(L) → cons(nil)

Rewrite Strategy: INNERMOST
0.00/0.55
0.00/0.55

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

Converted CpxTRS to CDT
0.00/0.55
0.00/0.55

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0 0.00/0.55
app(cons(z0), z1) → cons(z0) 0.00/0.55
from(z0) → cons(z0) 0.00/0.55
zWadr(nil, z0) → nil 0.00/0.55
zWadr(z0, nil) → nil 0.00/0.55
zWadr(cons(z0), cons(z1)) → cons(app(z1, cons(z0))) 0.00/0.55
prefix(z0) → cons(nil)
Tuples:

ZWADR(cons(z0), cons(z1)) → c5(APP(z1, cons(z0)))
S tuples:

ZWADR(cons(z0), cons(z1)) → c5(APP(z1, cons(z0)))
K tuples:none
Defined Rule Symbols:

app, from, zWadr, prefix

Defined Pair Symbols:

ZWADR

Compound Symbols:

c5

0.00/0.55
0.00/0.55

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

Removed 1 trailing tuple parts
0.00/0.55
0.00/0.55

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0 0.00/0.55
app(cons(z0), z1) → cons(z0) 0.00/0.55
from(z0) → cons(z0) 0.00/0.55
zWadr(nil, z0) → nil 0.00/0.55
zWadr(z0, nil) → nil 0.00/0.55
zWadr(cons(z0), cons(z1)) → cons(app(z1, cons(z0))) 0.00/0.55
prefix(z0) → cons(nil)
Tuples:

ZWADR(cons(z0), cons(z1)) → c5
S tuples:

ZWADR(cons(z0), cons(z1)) → c5
K tuples:none
Defined Rule Symbols:

app, from, zWadr, prefix

Defined Pair Symbols:

ZWADR

Compound Symbols:

c5

0.00/0.55
0.00/0.55

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

Removed 1 trailing nodes:

ZWADR(cons(z0), cons(z1)) → c5
0.00/0.55
0.00/0.55

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0 0.00/0.55
app(cons(z0), z1) → cons(z0) 0.00/0.55
from(z0) → cons(z0) 0.00/0.55
zWadr(nil, z0) → nil 0.00/0.55
zWadr(z0, nil) → nil 0.00/0.55
zWadr(cons(z0), cons(z1)) → cons(app(z1, cons(z0))) 0.00/0.55
prefix(z0) → cons(nil)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

app, from, zWadr, prefix

Defined Pair Symbols:none

Compound Symbols:none

0.00/0.55
0.00/0.55

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

The set S is empty
0.00/0.55
0.00/0.55

(8) BOUNDS(O(1), O(1))

0.00/0.55
0.00/0.55
0.00/0.58 EOF