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) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
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) |
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) |
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) |
[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 |
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) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).