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

(0) Obligation:

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

f(C(x1, x2)) → C(f(x1), f(x2))
f(Z) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
g(x) → x

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
f(C(z0, z1)) → C(f(z0), f(z1))
f(Z) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
g(z0) → z0

Tuples:

AND(False, False) → c
AND(True, False) → c1
AND(False, True) → c2
AND(True, True) → c3
F(C(z0, z1)) → c4(F(z0), F(z1))
F(Z) → c5
EQZLIST(C(z0, z1), C(z2, z3)) → c6(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
EQZLIST(C(z0, z1), Z) → c7
EQZLIST(Z, C(z0, z1)) → c8
EQZLIST(Z, Z) → c9
SECOND(C(z0, z1)) → c10
FIRST(C(z0, z1)) → c11
G(z0) → c12

S tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
F(Z) → c5
EQZLIST(C(z0, z1), C(z2, z3)) → c6(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
EQZLIST(C(z0, z1), Z) → c7
EQZLIST(Z, C(z0, z1)) → c8
EQZLIST(Z, Z) → c9
SECOND(C(z0, z1)) → c10
FIRST(C(z0, z1)) → c11
G(z0) → c12

K tuples:none
Defined Rule Symbols:

f, eqZList, second, first, g, and

Defined Pair Symbols:

AND, F, EQZLIST, SECOND, FIRST, G

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12

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

Removed 11 trailing nodes:

SECOND(C(z0, z1)) → c10
F(Z) → c5
EQZLIST(Z, C(z0, z1)) → c8
AND(False, False) → c
EQZLIST(Z, Z) → c9
AND(True, False) → c1
AND(False, True) → c2
G(z0) → c12
FIRST(C(z0, z1)) → c11
EQZLIST(C(z0, z1), Z) → c7
AND(True, True) → c3

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
f(C(z0, z1)) → C(f(z0), f(z1))
f(Z) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
g(z0) → z0

Tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))

S tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))

K tuples:none
Defined Rule Symbols:

f, eqZList, second, first, g, and

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c4, c6

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

Removed 1 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
f(C(z0, z1)) → C(f(z0), f(z1))
f(Z) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
g(z0) → z0

Tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))

S tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))

K tuples:none
Defined Rule Symbols:

f, eqZList, second, first, g, and

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c4, c6

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
f(C(z0, z1)) → C(f(z0), f(z1))
f(Z) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
g(z0) → z0

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))

S tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))

K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c4, c6

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))

We considered the (Usable) Rules:none
And the Tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁, x₂)) = [1] + x₁ + x₂   
POL(EQZLIST(x₁, x₂)) = [5] + [4]x₁ + [4]x₂   
POL(F(x₁)) = [4]x₁   
POL(c4(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁, x₂)) = x₁ + x₂   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))

S tuples:none
K tuples:

F(C(z0, z1)) → c4(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c6(EQZLIST(z0, z2), EQZLIST(z1, z3))

Defined Rule Symbols:none

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c4, c6

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

The set S is empty

(12) BOUNDS(1, 1)