The rewrite relation of the following TRS is considered.
from(X) |
→ |
cons(X,n__from(s(X))) |
(1) |
2ndspos(0,Z) |
→ |
rnil |
(2) |
2ndspos(s(N),cons(X,Z)) |
→ |
2ndspos(s(N),cons2(X,activate(Z))) |
(3) |
2ndspos(s(N),cons2(X,cons(Y,Z))) |
→ |
rcons(posrecip(Y),2ndsneg(N,activate(Z))) |
(4) |
2ndsneg(0,Z) |
→ |
rnil |
(5) |
2ndsneg(s(N),cons(X,Z)) |
→ |
2ndsneg(s(N),cons2(X,activate(Z))) |
(6) |
2ndsneg(s(N),cons2(X,cons(Y,Z))) |
→ |
rcons(negrecip(Y),2ndspos(N,activate(Z))) |
(7) |
pi(X) |
→ |
2ndspos(X,from(0)) |
(8) |
plus(0,Y) |
→ |
Y |
(9) |
plus(s(X),Y) |
→ |
s(plus(X,Y)) |
(10) |
times(0,Y) |
→ |
0 |
(11) |
times(s(X),Y) |
→ |
plus(Y,times(X,Y)) |
(12) |
square(X) |
→ |
times(X,X) |
(13) |
from(X) |
→ |
n__from(X) |
(14) |
activate(n__from(X)) |
→ |
from(X) |
(15) |
activate(X) |
→ |
X |
(16) |
The evaluation strategy is innermost.
|
originates from |
from(z0) |
→ |
cons(z0,n__from(s(z0))) |
(17) |
|
|
originates from |
from(z0) |
→ |
n__from(z0) |
(19) |
|
|
originates from |
2ndspos(0,z0) |
→ |
rnil |
(21) |
|
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
|
originates from |
2ndspos(s(z0),cons(z1,z2)) |
→ |
2ndspos(s(z0),cons2(z1,activate(z2))) |
(23) |
|
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
|
originates from |
2ndspos(s(z0),cons2(z1,cons(z2,z3))) |
→ |
rcons(posrecip(z2),2ndsneg(z0,activate(z3))) |
(25) |
|
|
originates from |
2ndsneg(0,z0) |
→ |
rnil |
(27) |
|
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
|
originates from |
2ndsneg(s(z0),cons(z1,z2)) |
→ |
2ndsneg(s(z0),cons2(z1,activate(z2))) |
(29) |
|
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
|
originates from |
2ndsneg(s(z0),cons2(z1,cons(z2,z3))) |
→ |
rcons(negrecip(z2),2ndspos(z0,activate(z3))) |
(31) |
|
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
|
originates from |
pi(z0) |
→ |
2ndspos(z0,from(0)) |
(33) |
|
|
originates from |
|
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
|
originates from |
plus(s(z0),z1) |
→ |
s(plus(z0,z1)) |
(37) |
|
|
originates from |
|
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
|
originates from |
times(s(z0),z1) |
→ |
plus(z1,times(z0,z1)) |
(41) |
|
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
|
originates from |
square(z0) |
→ |
times(z0,z0) |
(43) |
|
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
|
originates from |
activate(n__from(z0)) |
→ |
from(z0) |
(45) |
|
|
originates from |
|
Moreover, we add the following terms to the innermost strategy.
2ndspos(0,z0) |
→ |
rnil |
(21) |
2ndspos(s(z0),cons(z1,z2)) |
→ |
2ndspos(s(z0),cons2(z1,activate(z2))) |
(23) |
2ndspos(s(z0),cons2(z1,cons(z2,z3))) |
→ |
rcons(posrecip(z2),2ndsneg(z0,activate(z3))) |
(25) |
2ndsneg(0,z0) |
→ |
rnil |
(27) |
2ndsneg(s(z0),cons(z1,z2)) |
→ |
2ndsneg(s(z0),cons2(z1,activate(z2))) |
(29) |
2ndsneg(s(z0),cons2(z1,cons(z2,z3))) |
→ |
rcons(negrecip(z2),2ndspos(z0,activate(z3))) |
(31) |
pi(z0) |
→ |
2ndspos(z0,from(0)) |
(33) |
square(z0) |
→ |
times(z0,z0) |
(43) |
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
[square#(x1)] |
= |
+ · x1
|
[pi#(x1)] |
= |
+ · x1
|
[c] |
= |
|
[c1] |
= |
|
[c12(x1, x2)] |
= |
+ · x1 + · x2
|
[times#(x1, x2)] |
= |
+ · x1 + · x2
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1)] |
= |
+ · x1
|
[c5] |
= |
|
[c6(x1, x2)] |
= |
+ · x1 + · x2
|
[activate#(x1)] |
= |
+ · x1
|
[c2] |
= |
|
[c9] |
= |
|
[c10(x1)] |
= |
+ · x1
|
[c13(x1)] |
= |
+ · x1
|
[2ndspos#(x1, x2)] |
= |
+ · x1 + · x2
|
[c11] |
= |
|
[plus#(x1, x2)] |
= |
+ · x1 + · x2
|
[from#(x1)] |
= |
+ · x1
|
[c3(x1, x2)] |
= |
+ · x1 + · x2
|
[c4(x1, x2)] |
= |
+ · x1 + · x2
|
[2ndsneg#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[s(x1)] |
= |
+ · x1
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[n__from(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[activate(x1)] |
= |
+ · x1
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[cons2(x1, x2)] |
= |
+ · x1 + · x2
|
which has the intended complexity.
Here, only the following usable rules have been considered:
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from(z0) |
→ |
cons(z0,n__from(s(z0))) |
(17) |
from(z0) |
→ |
n__from(z0) |
(19) |
activate(n__from(z0)) |
→ |
from(z0) |
(45) |
activate(z0) |
→ |
z0 |
(47) |
[square#(x1)] |
= |
+ · x1
|
[pi#(x1)] |
= |
+ · x1
|
[c] |
= |
|
[c1] |
= |
|
[c12(x1, x2)] |
= |
+ · x1 + · x2
|
[times#(x1, x2)] |
= |
+ · x1 + · x2
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1)] |
= |
+ · x1
|
[c5] |
= |
|
[c6(x1, x2)] |
= |
+ · x1 + · x2
|
[activate#(x1)] |
= |
+ · x1
|
[c2] |
= |
|
[c9] |
= |
|
[c10(x1)] |
= |
+ · x1
|
[c13(x1)] |
= |
+ · x1
|
[2ndspos#(x1, x2)] |
= |
+ · x1 + · x2
|
[c11] |
= |
|
[plus#(x1, x2)] |
= |
+ · x1 + · x2
|
[from#(x1)] |
= |
+ · x1
|
[c3(x1, x2)] |
= |
+ · x1 + · x2
|
[c4(x1, x2)] |
= |
+ · x1 + · x2
|
[2ndsneg#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[s(x1)] |
= |
+ · x1
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[n__from(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[activate(x1)] |
= |
+ · x1
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[cons2(x1, x2)] |
= |
+ · x1 + · x2
|
which has the intended complexity.
Here, only the following usable rules have been considered:
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from(z0) |
→ |
cons(z0,n__from(s(z0))) |
(17) |
from(z0) |
→ |
n__from(z0) |
(19) |
activate(n__from(z0)) |
→ |
from(z0) |
(45) |
activate(z0) |
→ |
z0 |
(47) |
[square#(x1)] |
= |
+ · x1
|
[pi#(x1)] |
= |
+ · x1
|
[c] |
= |
|
[c1] |
= |
|
[c12(x1, x2)] |
= |
+ · x1 + · x2
|
[times#(x1, x2)] |
= |
+ · x1 + · x2
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1)] |
= |
+ · x1
|
[c5] |
= |
|
[c6(x1, x2)] |
= |
+ · x1 + · x2
|
[activate#(x1)] |
= |
+ · x1
|
[c2] |
= |
|
[c9] |
= |
|
[c10(x1)] |
= |
+ · x1
|
[c13(x1)] |
= |
+ · x1
|
[2ndspos#(x1, x2)] |
= |
+ · x1 + · x2
|
[c11] |
= |
|
[plus#(x1, x2)] |
= |
+ · x1 + · x2
|
[from#(x1)] |
= |
+ · x1
|
[c3(x1, x2)] |
= |
+ · x1 + · x2
|
[c4(x1, x2)] |
= |
+ · x1 + · x2
|
[2ndsneg#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[s(x1)] |
= |
+ · x1
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[n__from(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[activate(x1)] |
= |
+ · x1
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[cons2(x1, x2)] |
= |
+ · x1 + · x2
|
which has the intended complexity.
Here, only the following usable rules have been considered:
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from(z0) |
→ |
cons(z0,n__from(s(z0))) |
(17) |
from(z0) |
→ |
n__from(z0) |
(19) |
activate(n__from(z0)) |
→ |
from(z0) |
(45) |
activate(z0) |
→ |
z0 |
(47) |
[square#(x1)] |
= |
+ · x1
|
[pi#(x1)] |
= |
+ · x1
|
[c] |
= |
|
[c1] |
= |
|
[c12(x1, x2)] |
= |
+ · x1 + · x2
|
[times#(x1, x2)] |
= |
+ · x1 + · x2
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1)] |
= |
+ · x1
|
[c5] |
= |
|
[c6(x1, x2)] |
= |
+ · x1 + · x2
|
[activate#(x1)] |
= |
+ · x1
|
[c2] |
= |
|
[c9] |
= |
|
[c10(x1)] |
= |
+ · x1
|
[c13(x1)] |
= |
+ · x1
|
[2ndspos#(x1, x2)] |
= |
+ · x1 + · x2
|
[c11] |
= |
|
[plus#(x1, x2)] |
= |
+ · x1 + · x2
|
[from#(x1)] |
= |
+ · x1
|
[c3(x1, x2)] |
= |
+ · x1 + · x2
|
[c4(x1, x2)] |
= |
+ · x1 + · x2
|
[2ndsneg#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[s(x1)] |
= |
+ · x1
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[n__from(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[activate(x1)] |
= |
+ · x1
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[cons2(x1, x2)] |
= |
+ · x1 + · x2
|
which has the intended complexity.
Here, only the following usable rules have been considered:
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from(z0) |
→ |
cons(z0,n__from(s(z0))) |
(17) |
from(z0) |
→ |
n__from(z0) |
(19) |
activate(n__from(z0)) |
→ |
from(z0) |
(45) |
activate(z0) |
→ |
z0 |
(47) |
[square#(x1)] |
= |
+ · x1
|
[pi#(x1)] |
= |
+ · x1
|
[c] |
= |
|
[c1] |
= |
|
[c12(x1, x2)] |
= |
+ · x1 + · x2
|
[times#(x1, x2)] |
= |
+ · x1 + · x2
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1)] |
= |
+ · x1
|
[c5] |
= |
|
[c6(x1, x2)] |
= |
+ · x1 + · x2
|
[activate#(x1)] |
= |
+ · x1
|
[c2] |
= |
|
[c9] |
= |
|
[c10(x1)] |
= |
+ · x1
|
[c13(x1)] |
= |
+ · x1
|
[2ndspos#(x1, x2)] |
= |
+ · x1 + · x2
|
[c11] |
= |
|
[plus#(x1, x2)] |
= |
+ · x1 + · x2
|
[from#(x1)] |
= |
+ · x1
|
[c3(x1, x2)] |
= |
+ · x1 + · x2
|
[c4(x1, x2)] |
= |
+ · x1 + · x2
|
[2ndsneg#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[s(x1)] |
= |
+ · x1
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[n__from(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[activate(x1)] |
= |
+ · x1
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[cons2(x1, x2)] |
= |
+ · x1 + · x2
|
which has the intended complexity.
Here, only the following usable rules have been considered:
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from(z0) |
→ |
cons(z0,n__from(s(z0))) |
(17) |
from(z0) |
→ |
n__from(z0) |
(19) |
activate(n__from(z0)) |
→ |
from(z0) |
(45) |
activate(z0) |
→ |
z0 |
(47) |
[square#(x1)] |
= |
+ · x1
|
[pi#(x1)] |
= |
+ · x1
|
[c] |
= |
|
[c1] |
= |
|
[c12(x1, x2)] |
= |
+ · x1 + · x2
|
[times#(x1, x2)] |
= |
+ · x1 + · x2
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1)] |
= |
+ · x1
|
[c5] |
= |
|
[c6(x1, x2)] |
= |
+ · x1 + · x2
|
[activate#(x1)] |
= |
+ · x1
|
[c2] |
= |
|
[c9] |
= |
|
[c10(x1)] |
= |
+ · x1
|
[c13(x1)] |
= |
+ · x1
|
[2ndspos#(x1, x2)] |
= |
+ · x1 + · x2
|
[c11] |
= |
|
[plus#(x1, x2)] |
= |
+ · x1 + · x2
|
[from#(x1)] |
= |
+ · x1
|
[c3(x1, x2)] |
= |
+ · x1 + · x2
|
[c4(x1, x2)] |
= |
+ · x1 + · x2
|
[2ndsneg#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[s(x1)] |
= |
+ · x1
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[n__from(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[activate(x1)] |
= |
+ · x1
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[cons2(x1, x2)] |
= |
+ · x1 + · x2
|
which has the intended complexity.
Here, only the following usable rules have been considered:
from#(z0) |
→ |
c |
(18) |
from#(z0) |
→ |
c1 |
(20) |
2ndspos#(0,z0) |
→ |
c2 |
(22) |
2ndspos#(s(z0),cons(z1,z2)) |
→ |
c3(2ndspos#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(24) |
2ndspos#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c4(2ndsneg#(z0,activate(z3)),activate#(z3)) |
(26) |
2ndsneg#(0,z0) |
→ |
c5 |
(28) |
2ndsneg#(s(z0),cons(z1,z2)) |
→ |
c6(2ndsneg#(s(z0),cons2(z1,activate(z2))),activate#(z2)) |
(30) |
2ndsneg#(s(z0),cons2(z1,cons(z2,z3))) |
→ |
c7(2ndspos#(z0,activate(z3)),activate#(z3)) |
(32) |
pi#(z0) |
→ |
c8(2ndspos#(z0,from(0)),from#(0)) |
(34) |
plus#(0,z0) |
→ |
c9 |
(36) |
plus#(s(z0),z1) |
→ |
c10(plus#(z0,z1)) |
(38) |
times#(0,z0) |
→ |
c11 |
(40) |
times#(s(z0),z1) |
→ |
c12(plus#(z1,times(z0,z1)),times#(z0,z1)) |
(42) |
square#(z0) |
→ |
c13(times#(z0,z0)) |
(44) |
activate#(n__from(z0)) |
→ |
c14(from#(z0)) |
(46) |
activate#(z0) |
→ |
c15 |
(48) |
from(z0) |
→ |
cons(z0,n__from(s(z0))) |
(17) |
from(z0) |
→ |
n__from(z0) |
(19) |
activate(n__from(z0)) |
→ |
from(z0) |
(45) |
activate(z0) |
→ |
z0 |
(47) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).