and S is the following TRS.
a#(C(z0,z1),z2,z3) |
→ |
c4(a#(z0,z2,z3),a#(z1,z2,z2)) |
(14) |
|
originates from |
a(C(z0,z1),z2,z3) |
→ |
C(a(z0,z2,z3),a(z1,z2,z2)) |
(13) |
|
|
originates from |
|
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) |
|
|
originates from |
|
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) |
|
and#(False,False) |
→ |
c |
(28) |
|
originates from |
and(False,False) |
→ |
False |
(9) |
|
and#(True,False) |
→ |
c1 |
(29) |
|
originates from |
and(True,False) |
→ |
False |
(10) |
|
and#(False,True) |
→ |
c2 |
(30) |
|
originates from |
and(False,True) |
→ |
False |
(11) |
|
and#(True,True) |
→ |
c3 |
(31) |
|
originates from |
and(True,True) |
→ |
True |
(12) |
|
Moreover, we add the following terms to the innermost strategy.
a#(C(z0,z1),z2,z3) |
→ |
c4(a#(z0,z2,z3),a#(z1,z2,z2)) |
(14) |
a#(Z,z0,z1) |
→ |
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) |
are strictly oriented by the following
linear polynomial interpretation over the naturals
and#(False,False) |
→ |
c |
(28) |
and#(True,False) |
→ |
c1 |
(29) |
and#(False,True) |
→ |
c2 |
(30) |
and#(True,True) |
→ |
c3 |
(31) |
a#(C(z0,z1),z2,z3) |
→ |
c4(a#(z0,z2,z3),a#(z1,z2,z2)) |
(14) |
a#(Z,z0,z1) |
→ |
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) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).