The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳4 CdtProblem
↳5 CdtUsableRulesProof (⇔, 0 ms)
↳6 CdtProblem
↳7 CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))), 35 ms)
↳8 CdtProblem
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 BOUNDS(O(1), O(1))

(0) Obligation:

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

revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r))
deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest))
deeprevapp(V(n), rest) → revconsapp(rest, V(n))
deeprevapp(N, rest) → rest
revconsapp(V(n), r) → r
revconsapp(N, r) → r
deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N)
deeprev(V(n)) → V(n)
deeprev(N) → N
second(V(n)) → N
second(C(x1, x2)) → x2
isVal(C(x1, x2)) → False
isVal(V(n)) → True
isVal(N) → False
isNotEmptyT(C(x1, x2)) → True
isNotEmptyT(V(n)) → False
isNotEmptyT(N) → False
isEmptyT(C(x1, x2)) → False
isEmptyT(V(n)) → False
isEmptyT(N) → True
first(V(n)) → N
first(C(x1, x2)) → x1
goal(x) → deeprev(x)

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

revconsapp(C(z0, z1), z2) → revconsapp(z1, C(z0, z2))
revconsapp(V(z0), z1) → z1
revconsapp(N, z0) → z0
deeprevapp(C(z0, z1), z2) → deeprevapp(z1, C(z0, z2))
deeprevapp(V(z0), z1) → revconsapp(z1, V(z0))
deeprevapp(N, z0) → z0
deeprev(C(z0, z1)) → deeprevapp(C(z0, z1), N)
deeprev(V(z0)) → V(z0)
deeprev(N) → N
second(V(z0)) → N
second(C(z0, z1)) → z1
isVal(C(z0, z1)) → False
isVal(V(z0)) → True
isVal(N) → False
isNotEmptyT(C(z0, z1)) → True
isNotEmptyT(V(z0)) → False
isNotEmptyT(N) → False
isEmptyT(C(z0, z1)) → False
isEmptyT(V(z0)) → False
isEmptyT(N) → True
first(V(z0)) → N
first(C(z0, z1)) → z0
goal(z0) → deeprev(z0)
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
REVCONSAPP(V(z0), z1) → c1
REVCONSAPP(N, z0) → c2
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
DEEPREVAPP(N, z0) → c5
DEEPREV(C(z0, z1)) → c6(DEEPREVAPP(C(z0, z1), N))
DEEPREV(V(z0)) → c7
DEEPREV(N) → c8
SECOND(V(z0)) → c9
SECOND(C(z0, z1)) → c10
ISVAL(C(z0, z1)) → c11
ISVAL(V(z0)) → c12
ISVAL(N) → c13
ISNOTEMPTYT(C(z0, z1)) → c14
ISNOTEMPTYT(V(z0)) → c15
ISNOTEMPTYT(N) → c16
ISEMPTYT(C(z0, z1)) → c17
ISEMPTYT(V(z0)) → c18
ISEMPTYT(N) → c19
FIRST(V(z0)) → c20
FIRST(C(z0, z1)) → c21
GOAL(z0) → c22(DEEPREV(z0))
S tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
REVCONSAPP(V(z0), z1) → c1
REVCONSAPP(N, z0) → c2
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
DEEPREVAPP(N, z0) → c5
DEEPREV(C(z0, z1)) → c6(DEEPREVAPP(C(z0, z1), N))
DEEPREV(V(z0)) → c7
DEEPREV(N) → c8
SECOND(V(z0)) → c9
SECOND(C(z0, z1)) → c10
ISVAL(C(z0, z1)) → c11
ISVAL(V(z0)) → c12
ISVAL(N) → c13
ISNOTEMPTYT(C(z0, z1)) → c14
ISNOTEMPTYT(V(z0)) → c15
ISNOTEMPTYT(N) → c16
ISEMPTYT(C(z0, z1)) → c17
ISEMPTYT(V(z0)) → c18
ISEMPTYT(N) → c19
FIRST(V(z0)) → c20
FIRST(C(z0, z1)) → c21
GOAL(z0) → c22(DEEPREV(z0))
K tuples:none
Defined Rule Symbols:

revconsapp, deeprevapp, deeprev, second, isVal, isNotEmptyT, isEmptyT, first, goal

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP, DEEPREV, SECOND, ISVAL, ISNOTEMPTYT, ISEMPTYT, FIRST, GOAL

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0) → c22(DEEPREV(z0))
DEEPREV(C(z0, z1)) → c6(DEEPREVAPP(C(z0, z1), N))
Removed 18 trailing nodes:

ISEMPTYT(C(z0, z1)) → c17
ISNOTEMPTYT(C(z0, z1)) → c14
ISVAL(N) → c13
ISEMPTYT(V(z0)) → c18
REVCONSAPP(V(z0), z1) → c1
DEEPREV(N) → c8
DEEPREVAPP(N, z0) → c5
ISEMPTYT(N) → c19
SECOND(V(z0)) → c9
ISNOTEMPTYT(N) → c16
FIRST(V(z0)) → c20
REVCONSAPP(N, z0) → c2
ISVAL(C(z0, z1)) → c11
DEEPREV(V(z0)) → c7
FIRST(C(z0, z1)) → c21
SECOND(C(z0, z1)) → c10
ISVAL(V(z0)) → c12
ISNOTEMPTYT(V(z0)) → c15

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

revconsapp(C(z0, z1), z2) → revconsapp(z1, C(z0, z2))
revconsapp(V(z0), z1) → z1
revconsapp(N, z0) → z0
deeprevapp(C(z0, z1), z2) → deeprevapp(z1, C(z0, z2))
deeprevapp(V(z0), z1) → revconsapp(z1, V(z0))
deeprevapp(N, z0) → z0
deeprev(C(z0, z1)) → deeprevapp(C(z0, z1), N)
deeprev(V(z0)) → V(z0)
deeprev(N) → N
second(V(z0)) → N
second(C(z0, z1)) → z1
isVal(C(z0, z1)) → False
isVal(V(z0)) → True
isVal(N) → False
isNotEmptyT(C(z0, z1)) → True
isNotEmptyT(V(z0)) → False
isNotEmptyT(N) → False
isEmptyT(C(z0, z1)) → False
isEmptyT(V(z0)) → False
isEmptyT(N) → True
first(V(z0)) → N
first(C(z0, z1)) → z0
goal(z0) → deeprev(z0)
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
S tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
K tuples:none
Defined Rule Symbols:

revconsapp, deeprevapp, deeprev, second, isVal, isNotEmptyT, isEmptyT, first, goal

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP

Compound Symbols:

c, c3, c4

(5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

revconsapp(C(z0, z1), z2) → revconsapp(z1, C(z0, z2))
revconsapp(V(z0), z1) → z1
revconsapp(N, z0) → z0
deeprevapp(C(z0, z1), z2) → deeprevapp(z1, C(z0, z2))
deeprevapp(V(z0), z1) → revconsapp(z1, V(z0))
deeprevapp(N, z0) → z0
deeprev(C(z0, z1)) → deeprevapp(C(z0, z1), N)
deeprev(V(z0)) → V(z0)
deeprev(N) → N
second(V(z0)) → N
second(C(z0, z1)) → z1
isVal(C(z0, z1)) → False
isVal(V(z0)) → True
isVal(N) → False
isNotEmptyT(C(z0, z1)) → True
isNotEmptyT(V(z0)) → False
isNotEmptyT(N) → False
isEmptyT(C(z0, z1)) → False
isEmptyT(V(z0)) → False
isEmptyT(N) → True
first(V(z0)) → N
first(C(z0, z1)) → z0
goal(z0) → deeprev(z0)

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
S tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP

Compound Symbols:

c, c3, c4

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

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

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
We considered the (Usable) Rules:none
And the Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x1, x2)) = [2] + x2   
POL(DEEPREVAPP(x1, x2)) = [4] + [4]x1 + [3]x2   
POL(REVCONSAPP(x1, x2)) = [5] + [2]x1   
POL(V(x1)) = [3]   
POL(c(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
S tuples:none
K tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
Defined Rule Symbols:none

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP

Compound Symbols:

c, c3, c4

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

The set S is empty

(10) BOUNDS(O(1), O(1))