Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Others/disj2_typed)

The relative rewrite relation R/S is considered where R is the following TRS

f(C(x1,x2)) → C(f(x1),f(x2)) (1)
f(Z) → Z (2)
eqZList(C(x1,x2),C(y1,y2)) → and(eqZList(x1,y1),eqZList(x2,y2)) (3)
eqZList(C(x1,x2),Z) → False (4)
eqZList(Z,C(y1,y2)) → False (5)
eqZList(Z,Z) → True (6)
second(C(x1,x2)) → x2 (7)
first(C(x1,x2)) → x1 (8)
g(x) → x (9)

and S is the following TRS.

and(False,False) → False (10)
and(True,False) → False (11)
and(False,True) → False (12)
and(True,True) → True (13)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
f#(C(z0,z1)) → c4(f#(z0),f#(z1)) (15)
originates from
f(C(z0,z1)) → C(f(z0),f(z1)) (14)
f#(Z) → c5 (16)
originates from
f(Z) → Z (2)
eqZList#(C(z0,z1),C(z2,z3)) → c6(and#(eqZList(z0,z2),eqZList(z1,z3)),eqZList#(z0,z2),eqZList#(z1,z3)) (18)
originates from
eqZList(C(z0,z1),C(z2,z3)) → and(eqZList(z0,z2),eqZList(z1,z3)) (17)
eqZList#(C(z0,z1),Z) → c7 (20)
originates from
eqZList(C(z0,z1),Z) → False (19)
eqZList#(Z,C(z0,z1)) → c8 (22)
originates from
eqZList(Z,C(z0,z1)) → False (21)
eqZList#(Z,Z) → c9 (23)
originates from
eqZList(Z,Z) → True (6)
second#(C(z0,z1)) → c10 (25)
originates from
second(C(z0,z1)) → z1 (24)
first#(C(z0,z1)) → c11 (27)
originates from
first(C(z0,z1)) → z0 (26)
g#(z0) → c12 (29)
originates from
g(z0) → z0 (28)
and#(False,False) → c (30)
originates from
and(False,False) → False (10)
and#(True,False) → c1 (31)
originates from
and(True,False) → False (11)
and#(False,True) → c2 (32)
originates from
and(False,True) → False (12)
and#(True,True) → c3 (33)
originates from
and(True,True) → True (13)
Moreover, we add the following terms to the innermost strategy.
and#(False,False)
and#(True,False)
and#(False,True)
and#(True,True)
f#(C(z0,z1))
f#(Z)
eqZList#(C(z0,z1),C(z2,z3))
eqZList#(C(z0,z1),Z)
eqZList#(Z,C(z0,z1))
eqZList#(Z,Z)
second#(C(z0,z1))
first#(C(z0,z1))
g#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.
f(C(z0,z1)) → C(f(z0),f(z1)) (14)
f(Z) → Z (2)
second(C(z0,z1)) → z1 (24)
first(C(z0,z1)) → z0 (26)
g(z0) → z0 (28)

1.1.1 Rule Shifting

The rules
f#(C(z0,z1)) → c4(f#(z0),f#(z1)) (15)
f#(Z) → c5 (16)
eqZList#(C(z0,z1),C(z2,z3)) → c6(and#(eqZList(z0,z2),eqZList(z1,z3)),eqZList#(z0,z2),eqZList#(z1,z3)) (18)
eqZList#(C(z0,z1),Z) → c7 (20)
eqZList#(Z,C(z0,z1)) → c8 (22)
eqZList#(Z,Z) → c9 (23)
second#(C(z0,z1)) → c10 (25)
first#(C(z0,z1)) → c11 (27)
g#(z0) → c12 (29)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3] = 0
[c4(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c5] = 0
[c6(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[c7] = 0
[c8] = 0
[c9] = 0
[c10] = 0
[c11] = 0
[c12] = 0
[eqZList(x1, x2)] = 1 + 1 · x1 + 1 · x2
[and(x1, x2)] = 1 + 1 · x1
[and#(x1, x2)] = 0
[f#(x1)] = 1 · x1 + 0
[eqZList#(x1, x2)] = 1 + 1 · x1 + 1 · x2
[second#(x1)] = 1 · x1 + 0
[first#(x1)] = 1 + 1 · x1
[g#(x1)] = 1
[C(x1, x2)] = 1 + 1 · x1 + 1 · x2
[Z] = 1
[False] = 1
[True] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
and#(False,False) → c (30)
and#(True,False) → c1 (31)
and#(False,True) → c2 (32)
and#(True,True) → c3 (33)
f#(C(z0,z1)) → c4(f#(z0),f#(z1)) (15)
f#(Z) → c5 (16)
eqZList#(C(z0,z1),C(z2,z3)) → c6(and#(eqZList(z0,z2),eqZList(z1,z3)),eqZList#(z0,z2),eqZList#(z1,z3)) (18)
eqZList#(C(z0,z1),Z) → c7 (20)
eqZList#(Z,C(z0,z1)) → c8 (22)
eqZList#(Z,Z) → c9 (23)
second#(C(z0,z1)) → c10 (25)
first#(C(z0,z1)) → c11 (27)
g#(z0) → c12 (29)

1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).