The rewrite relation of the following TRS is considered.
U11(tt,M,N) | → | U12(tt,activate(M),activate(N)) | (1) |
U12(tt,M,N) | → | s(plus(activate(N),activate(M))) | (2) |
U21(tt,M,N) | → | U22(tt,activate(M),activate(N)) | (3) |
U22(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
plus(N,0) | → | N | (5) |
plus(N,s(M)) | → | U11(tt,M,N) | (6) |
x(N,0) | → | 0 | (7) |
x(N,s(M)) | → | U21(tt,M,N) | (8) |
activate(X) | → | X | (9) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
U11#(tt,z0,z1) |
U12#(tt,z0,z1) |
U21#(tt,z0,z1) |
U22#(tt,z0,z1) |
plus#(z0,0) |
plus#(z0,s(z1)) |
x#(z0,0) |
x#(z0,s(z1)) |
activate#(z0) |
x#(z0,0) | → | c6 | (23) |
[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 · x2 + 0 + 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 · x1 + 0 |
[tt] | = | 1 |
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) |
x#(z0,s(z1)) | → | c7(U21#(tt,z1,z0)) | (25) |
[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 · x2 + 0 |
[U22#(x1, x2, x3)] | = | 1 · x2 + 0 |
[plus#(x1, x2)] | = | 0 |
[x#(x1, x2)] | = | 1 · x2 + 0 |
[activate#(x1)] | = | 0 |
[0] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[tt] | = | 1 |
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) |
U21#(tt,z0,z1) | → | c2(U22#(tt,activate(z0),activate(z1)),activate#(z0),activate#(z1)) | (15) |
[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 |
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) |
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) |
[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 |
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) |
plus#(z0,0) | → | c4 | (19) |
[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)] | = | 1 · x1 + 0 |
[U12#(x1, x2, x3)] | = | 1 · x1 + 0 |
[U21#(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 |
[U22#(x1, x2, x3)] | = | 1 · x1 + 0 + 1 · x2 |
[plus#(x1, x2)] | = | 1 |
[x#(x1, x2)] | = | 1 · x2 + 0 |
[activate#(x1)] | = | 0 |
[0] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[tt] | = | 1 |
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) |
[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 |
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) |
plus#(z0,s(z1)) | → | c5(U11#(tt,z1,z0)) | (21) |
[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 |
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) |
activate#(z0) | → | c8 | (27) |
[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 |
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).