The rewrite relation of the following TRS is considered.
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
|
originates from |
U11(tt,z0,z1) |
→ |
U12(tt,activate(z0),activate(z1)) |
(10) |
|
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
|
originates from |
U12(tt,z0,z1) |
→ |
s(plus(activate(z1),activate(z0))) |
(12) |
|
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
|
originates from |
U21(tt,z0,z1) |
→ |
U22(tt,activate(z0),activate(z1)) |
(14) |
|
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
|
originates from |
U22(tt,z0,z1) |
→ |
plus(x(activate(z1),activate(z0)),activate(z1)) |
(16) |
|
|
originates from |
|
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
|
originates from |
plus(z0,s(z1)) |
→ |
U11(tt,z1,z0) |
(20) |
|
|
originates from |
|
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
|
originates from |
x(z0,s(z1)) |
→ |
U21(tt,z1,z0) |
(24) |
|
|
originates from |
|
Moreover, we add the following terms to the innermost strategy.
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
plus#(z0,0) |
→ |
c4 |
(19) |
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
x#(z0,0) |
→ |
c6 |
(23) |
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
activate#(z0) |
→ |
c8 |
(27) |
activate(z0) |
→ |
z0 |
(26) |
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
plus#(z0,0) |
→ |
c4 |
(19) |
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
x#(z0,0) |
→ |
c6 |
(23) |
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
activate#(z0) |
→ |
c8 |
(27) |
activate(z0) |
→ |
z0 |
(26) |
[c(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c1(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c2(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c3(x1,...,x5)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
|
[c4] |
= |
0 |
[c5(x1)] |
= |
1 · x1 + 0 |
[c6] |
= |
0 |
[c7(x1)] |
= |
1 · x1 + 0 |
[c8] |
= |
0 |
[U11(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3
|
[U12(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3
|
[U21(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3
|
[U22(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3
|
[plus(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[x(x1, x2)] |
= |
1 |
[activate(x1)] |
= |
1 · x1 + 0 |
[U11#(x1, x2, x3)] |
= |
0 |
[U12#(x1, x2, x3)] |
= |
0 |
[U21#(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[U22#(x1, x2, x3)] |
= |
1 · x2 + 0 + 1 · x3
|
[plus#(x1, x2)] |
= |
0 |
[x#(x1, x2)] |
= |
1 · x1 + 0 + 1 · x2
|
[activate#(x1)] |
= |
0 |
[0] |
= |
1 |
[s(x1)] |
= |
1 + 1 · x1
|
[tt] |
= |
1 |
which has the intended complexity.
Here, only the following usable rules have been considered:
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
plus#(z0,0) |
→ |
c4 |
(19) |
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
x#(z0,0) |
→ |
c6 |
(23) |
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
activate#(z0) |
→ |
c8 |
(27) |
activate(z0) |
→ |
z0 |
(26) |
[c(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c1(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c2(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c3(x1,...,x5)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
|
[c4] |
= |
0 |
[c5(x1)] |
= |
1 · x1 + 0 |
[c6] |
= |
0 |
[c7(x1)] |
= |
1 · x1 + 0 |
[c8] |
= |
0 |
[U11(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3
|
[U12(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3
|
[U21(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3
|
[U22(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3
|
[plus(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[x(x1, x2)] |
= |
1 + 1 · x1
|
[activate(x1)] |
= |
1 · x1 + 0 |
[U11#(x1, x2, x3)] |
= |
0 |
[U12#(x1, x2, x3)] |
= |
0 |
[U21#(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[U22#(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[plus#(x1, x2)] |
= |
0 |
[x#(x1, x2)] |
= |
1 · x1 + 0 + 1 · x2
|
[activate#(x1)] |
= |
0 |
[0] |
= |
1 |
[s(x1)] |
= |
1 + 1 · x1
|
[tt] |
= |
1 |
which has the intended complexity.
Here, only the following usable rules have been considered:
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
plus#(z0,0) |
→ |
c4 |
(19) |
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
x#(z0,0) |
→ |
c6 |
(23) |
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
activate#(z0) |
→ |
c8 |
(27) |
activate(z0) |
→ |
z0 |
(26) |
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
plus#(z0,0) |
→ |
c4 |
(19) |
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
x#(z0,0) |
→ |
c6 |
(23) |
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
activate#(z0) |
→ |
c8 |
(27) |
activate(z0) |
→ |
z0 |
(26) |
[c(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c1(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c2(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c3(x1,...,x5)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
|
[c4] |
= |
0 |
[c5(x1)] |
= |
1 · x1 + 0 |
[c6] |
= |
0 |
[c7(x1)] |
= |
1 · x1 + 0 |
[c8] |
= |
0 |
[U11(x1, x2, x3)] |
= |
1 + 2 · x1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x1 · x3 + 1 · x1 · x1 + 2 · x2 · x1 + 1 · x2 · x2
|
[U12(x1, x2, x3)] |
= |
1 + 2 · x1 + 2 · x1 · x1
|
[U21(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x1 · x3 + 2 · x1 · x1 + 2 · x2 · x1 + 1 · x2 · x2
|
[U22(x1, x2, x3)] |
= |
1 + 2 · x1 + 1 · x1 · x1
|
[plus(x1, x2)] |
= |
1 |
[x(x1, x2)] |
= |
0 |
[activate(x1)] |
= |
1 · x1 + 0 |
[U11#(x1, x2, x3)] |
= |
2 + 1 · x1 + 1 · x2 + 2 · x1 · x3 + 2 · x1 · x1 + 1 · x2 · x1
|
[U12#(x1, x2, x3)] |
= |
1 + 2 · x1 + 1 · x2 + 2 · x1 · x1
|
[U21#(x1, x2, x3)] |
= |
2 · x1 + 0 + 1 · x3 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x1 + 1 · x2 · x1
|
[U22#(x1, x2, x3)] |
= |
2 · x1 + 0 + 1 · x3 + 1 · x2 · x3 + 1 · x1 · x1
|
[plus#(x1, x2)] |
= |
1 · x2 + 0 |
[x#(x1, x2)] |
= |
1 · x1 · x2 + 0 |
[activate#(x1)] |
= |
0 |
[0] |
= |
2 |
[s(x1)] |
= |
2 + 1 · x1
|
[tt] |
= |
0 |
which has the intended complexity.
Here, only the following usable rules have been considered:
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
plus#(z0,0) |
→ |
c4 |
(19) |
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
x#(z0,0) |
→ |
c6 |
(23) |
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
activate#(z0) |
→ |
c8 |
(27) |
activate(z0) |
→ |
z0 |
(26) |
[c(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c1(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c2(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c3(x1,...,x5)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
|
[c4] |
= |
0 |
[c5(x1)] |
= |
1 · x1 + 0 |
[c6] |
= |
0 |
[c7(x1)] |
= |
1 · x1 + 0 |
[c8] |
= |
0 |
[U11(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 2 · x1 · x3 + 1 · x1 · x1 + 2 · x2 · x1 + 1 · x2 · x2
|
[U12(x1, x2, x3)] |
= |
1 + 2 · x1 + 1 · x1 · x1
|
[U21(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 2 · x1 · x3 + 1 · x1 · x1 + 1 · x2 · x1 + 1 · x2 · x2
|
[U22(x1, x2, x3)] |
= |
1 + 1 · x1 + 2 · x1 · x1
|
[plus(x1, x2)] |
= |
1 |
[x(x1, x2)] |
= |
0 |
[activate(x1)] |
= |
1 · x1 + 0 |
[U11#(x1, x2, x3)] |
= |
2 · x1 + 0 + 1 · x2 + 2 · x1 · x3 + 2 · x1 · x1 + 1 · x2 · x1
|
[U12#(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x1 · x1
|
[U21#(x1, x2, x3)] |
= |
2 · x1 + 0 + 1 · x3 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x1 + 1 · x2 · x1
|
[U22#(x1, x2, x3)] |
= |
2 · x1 + 0 + 1 · x3 + 1 · x2 · x3 + 2 · x1 · x1
|
[plus#(x1, x2)] |
= |
1 · x2 + 0 |
[x#(x1, x2)] |
= |
1 · x1 · x2 + 0 |
[activate#(x1)] |
= |
0 |
[0] |
= |
2 |
[s(x1)] |
= |
2 + 1 · x1
|
[tt] |
= |
0 |
which has the intended complexity.
Here, only the following usable rules have been considered:
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
plus#(z0,0) |
→ |
c4 |
(19) |
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
x#(z0,0) |
→ |
c6 |
(23) |
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
activate#(z0) |
→ |
c8 |
(27) |
activate(z0) |
→ |
z0 |
(26) |
[c(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c1(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c2(x1, x2, x3)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3
|
[c3(x1,...,x5)] |
= |
1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
|
[c4] |
= |
0 |
[c5(x1)] |
= |
1 · x1 + 0 |
[c6] |
= |
0 |
[c7(x1)] |
= |
1 · x1 + 0 |
[c8] |
= |
0 |
[U11(x1, x2, x3)] |
= |
1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x1 · x3 + 1 · x1 · x1 + 1 · x2 · x1 + 1 · x2 · x2
|
[U12(x1, x2, x3)] |
= |
1 + 1 · x1 + 2 · x1 · x1
|
[U21(x1, x2, x3)] |
= |
1 + 2 · x1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x1 · x3 + 1 · x1 · x1 + 2 · x2 · x1 + 1 · x2 · x2
|
[U22(x1, x2, x3)] |
= |
1 + 2 · x1 + 2 · x1 · x1
|
[plus(x1, x2)] |
= |
2 |
[x(x1, x2)] |
= |
0 |
[activate(x1)] |
= |
1 · x1 + 0 |
[U11#(x1, x2, x3)] |
= |
2 + 2 · x1 + 2 · x2
|
[U12#(x1, x2, x3)] |
= |
1 + 1 · x1 · x1 + 2 · x2 · x1
|
[U21#(x1, x2, x3)] |
= |
2 + 2 · x1 + 1 · x2 + 2 · x3 + 2 · x2 · x3 + 2 · x1 · x1 + 1 · x2 · x1 + 1 · x2 · x2
|
[U22#(x1, x2, x3)] |
= |
2 + 2 · x1 + 1 · x2 + 2 · x2 · x3 + 2 · x1 · x3 + 1 · x2 · x2
|
[plus#(x1, x2)] |
= |
2 · x2 + 0 |
[x#(x1, x2)] |
= |
1 + 1 · x2 + 1 · x2 · x2 + 2 · x1 · x2
|
[activate#(x1)] |
= |
1 |
[0] |
= |
2 |
[s(x1)] |
= |
2 + 1 · x1
|
[tt] |
= |
1 |
which has the intended complexity.
Here, only the following usable rules have been considered:
U11#(tt,z0,z1) |
→ |
c(U12#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(11) |
U12#(tt,z0,z1) |
→ |
c1(plus#(activate(z1),activate(z0)),activate#(z1),activate#(z0)) |
(13) |
U21#(tt,z0,z1) |
→ |
c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) |
(15) |
U22#(tt,z0,z1) |
→ |
c3(plus#(x(activate(z1),activate(z0)),activate(z1)),x#(activate(z1),activate(z0)),activate#(z1),activate#(z0),activate#(z1)) |
(17) |
plus#(z0,0) |
→ |
c4 |
(19) |
plus#(z0,s(z1)) |
→ |
c5(U11#(tt,z1,z0)) |
(21) |
x#(z0,0) |
→ |
c6 |
(23) |
x#(z0,s(z1)) |
→ |
c7(U21#(tt,z1,z0)) |
(25) |
activate#(z0) |
→ |
c8 |
(27) |
activate(z0) |
→ |
z0 |
(26) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).