YES(O(1), O(n^1)) 0.00/0.79 YES(O(1), O(n^1)) 0.00/0.81 0.00/0.81 0.00/0.81 0.00/0.81 0.00/0.81 0.00/0.81 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.81 0.00/0.81 0.00/0.81
0.00/0.81 0.00/0.81 0.00/0.81
0.00/0.81
0.00/0.81

(0) Obligation:

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

first(0, X) → nil 0.00/0.81
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) 0.00/0.81
from(X) → cons(X, n__from(s(X))) 0.00/0.81
first(X1, X2) → n__first(X1, X2) 0.00/0.81
from(X) → n__from(X) 0.00/0.81
activate(n__first(X1, X2)) → first(X1, X2) 0.00/0.81
activate(n__from(X)) → from(X) 0.00/0.81
activate(X) → X

Rewrite Strategy: INNERMOST
0.00/0.81
0.00/0.81

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

Converted CpxTRS to CDT
0.00/0.81
0.00/0.81

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
Tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6(FROM(z0))
S tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6(FROM(z0))
K tuples:none
Defined Rule Symbols:

first, from, activate

Defined Pair Symbols:

FIRST, ACTIVATE

Compound Symbols:

c1, c5, c6

0.00/0.81
0.00/0.81

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

Removed 1 trailing tuple parts
0.00/0.81
0.00/0.81

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
Tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
S tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
K tuples:none
Defined Rule Symbols:

first, from, activate

Defined Pair Symbols:

FIRST, ACTIVATE

Compound Symbols:

c1, c5, c6

0.00/0.81
0.00/0.81

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

Removed 1 trailing nodes:

ACTIVATE(n__from(z0)) → c6
0.00/0.81
0.00/0.81

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
Tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
S tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
K tuples:none
Defined Rule Symbols:

first, from, activate

Defined Pair Symbols:

FIRST, ACTIVATE

Compound Symbols:

c1, c5, c6

0.00/0.81
0.00/0.81

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVATE(n__from(z0)) → c6
We considered the (Usable) Rules:none
And the Tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
The order we found is given by the following interpretation:
Polynomial interpretation : 0.00/0.81

POL(ACTIVATE(x1)) = [2]    0.00/0.81
POL(FIRST(x1, x2)) = [2]    0.00/0.81
POL(c1(x1)) = x1    0.00/0.81
POL(c5(x1)) = x1    0.00/0.81
POL(c6) = 0    0.00/0.81
POL(cons(x1, x2)) = 0    0.00/0.81
POL(n__first(x1, x2)) = 0    0.00/0.81
POL(n__from(x1)) = 0    0.00/0.81
POL(s(x1)) = 0   
0.00/0.81
0.00/0.81

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
Tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
S tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1))
K tuples:

ACTIVATE(n__from(z0)) → c6
Defined Rule Symbols:

first, from, activate

Defined Pair Symbols:

FIRST, ACTIVATE

Compound Symbols:

c1, c5, c6

0.00/0.81
0.00/0.81

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
The order we found is given by the following interpretation:
Polynomial interpretation : 0.00/0.81

POL(ACTIVATE(x1)) = [2] + [4]x1    0.00/0.81
POL(FIRST(x1, x2)) = [4]x2    0.00/0.81
POL(c1(x1)) = x1    0.00/0.81
POL(c5(x1)) = x1    0.00/0.81
POL(c6) = 0    0.00/0.81
POL(cons(x1, x2)) = [1] + x2    0.00/0.81
POL(n__first(x1, x2)) = [1] + x2    0.00/0.81
POL(n__from(x1)) = 0    0.00/0.81
POL(s(x1)) = [1]   
0.00/0.81
0.00/0.81

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
Tuples:

FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
S tuples:none
K tuples:

ACTIVATE(n__from(z0)) → c6 0.00/0.81
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1))
Defined Rule Symbols:

first, from, activate

Defined Pair Symbols:

FIRST, ACTIVATE

Compound Symbols:

c1, c5, c6

0.00/0.81
0.00/0.81

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

The set S is empty
0.00/0.81
0.00/0.81

(12) BOUNDS(O(1), O(1))

0.00/0.81
0.00/0.81
0.00/0.83 EOF