The rewrite relation of the following TRS is considered.
natsFrom(N) | → | cons(N,n__natsFrom(s(N))) | (1) |
fst(pair(XS,YS)) | → | XS | (2) |
snd(pair(XS,YS)) | → | YS | (3) |
splitAt(0,XS) | → | pair(nil,XS) | (4) |
splitAt(s(N),cons(X,XS)) | → | u(splitAt(N,activate(XS)),N,X,activate(XS)) | (5) |
u(pair(YS,ZS),N,X,XS) | → | pair(cons(activate(X),YS),ZS) | (6) |
head(cons(N,XS)) | → | N | (7) |
tail(cons(N,XS)) | → | activate(XS) | (8) |
sel(N,XS) | → | head(afterNth(N,XS)) | (9) |
take(N,XS) | → | fst(splitAt(N,XS)) | (10) |
afterNth(N,XS) | → | snd(splitAt(N,XS)) | (11) |
natsFrom(X) | → | n__natsFrom(X) | (12) |
activate(n__natsFrom(X)) | → | natsFrom(X) | (13) |
activate(X) | → | X | (14) |
|
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 |
|
||||||||
|
originates from |
|
natsFrom#(z0) |
natsFrom#(z0) |
fst#(pair(z0,z1)) |
snd#(pair(z0,z1)) |
splitAt#(0,z0) |
splitAt#(s(z0),cons(z1,z2)) |
u#(pair(z0,z1),z2,z3,z4) |
head#(cons(z0,z1)) |
tail#(cons(z0,z1)) |
sel#(z0,z1) |
take#(z0,z1) |
afterNth#(z0,z1) |
activate#(n__natsFrom(z0)) |
activate#(z0) |
fst(pair(z0,z1)) | → | z0 | (19) |
head(cons(z0,z1)) | → | z0 | (29) |
tail(cons(z0,z1)) | → | activate(z1) | (31) |
sel(z0,z1) | → | head(afterNth(z0,z1)) | (33) |
take(z0,z1) | → | fst(splitAt(z0,z1)) | (35) |
fst#(pair(z0,z1)) | → | c2 | (20) |
head#(cons(z0,z1)) | → | c7 | (30) |
tail#(cons(z0,z1)) | → | c8(activate#(z1)) | (32) |
[c] | = | 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8(x1)] | = | 1 · x1 + 0 |
[c9(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c10(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c11(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13] | = | 0 |
[splitAt(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[activate(x1)] | = | 1 · x1 + 0 |
[natsFrom(x1)] | = | 1 + 1 · x1 |
[u(x1,...,x4)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x4 |
[afterNth(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[snd(x1)] | = | 1 + 1 · x1 |
[natsFrom#(x1)] | = | 0 |
[fst#(x1)] | = | 1 |
[snd#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 0 |
[u#(x1,...,x4)] | = | 0 |
[head#(x1)] | = | 1 |
[tail#(x1)] | = | 1 + 1 · x1 |
[sel#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[take#(x1, x2)] | = | 1 |
[afterNth#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[activate#(x1)] | = | 0 |
[0] | = | 1 |
[pair(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[cons(x1, x2)] | = | 1 · x1 + 0 |
[n__natsFrom(x1)] | = | 1 + 1 · x1 |
natsFrom#(z0) | → | c | (16) |
natsFrom#(z0) | → | c1 | (18) |
fst#(pair(z0,z1)) | → | c2 | (20) |
snd#(pair(z0,z1)) | → | c3 | (22) |
splitAt#(0,z0) | → | c4 | (24) |
splitAt#(s(z0),cons(z1,z2)) | → | c5(u#(splitAt(z0,activate(z2)),z0,z1,activate(z2)),splitAt#(z0,activate(z2)),activate#(z2),activate#(z2)) | (26) |
u#(pair(z0,z1),z2,z3,z4) | → | c6(activate#(z3)) | (28) |
head#(cons(z0,z1)) | → | c7 | (30) |
tail#(cons(z0,z1)) | → | c8(activate#(z1)) | (32) |
sel#(z0,z1) | → | c9(head#(afterNth(z0,z1)),afterNth#(z0,z1)) | (34) |
take#(z0,z1) | → | c10(fst#(splitAt(z0,z1)),splitAt#(z0,z1)) | (36) |
afterNth#(z0,z1) | → | c11(snd#(splitAt(z0,z1)),splitAt#(z0,z1)) | (38) |
activate#(n__natsFrom(z0)) | → | c12(natsFrom#(z0)) | (40) |
activate#(z0) | → | c13 | (42) |
snd#(pair(z0,z1)) | → | c3 | (22) |
splitAt#(0,z0) | → | c4 | (24) |
splitAt#(s(z0),cons(z1,z2)) | → | c5(u#(splitAt(z0,activate(z2)),z0,z1,activate(z2)),splitAt#(z0,activate(z2)),activate#(z2),activate#(z2)) | (26) |
[c] | = | 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8(x1)] | = | 1 · x1 + 0 |
[c9(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c10(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c11(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13] | = | 0 |
[splitAt(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[activate(x1)] | = | 1 · x1 + 0 |
[natsFrom(x1)] | = | 1 + 1 · x1 |
[u(x1,...,x4)] | = | 1 + 1 · x2 + 1 · x3 + 1 · x4 |
[afterNth(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[snd(x1)] | = | 1 + 1 · x1 |
[natsFrom#(x1)] | = | 0 |
[fst#(x1)] | = | 1 |
[snd#(x1)] | = | 1 |
[splitAt#(x1, x2)] | = | 1 · x1 + 0 |
[u#(x1,...,x4)] | = | 0 |
[head#(x1)] | = | 0 |
[tail#(x1)] | = | 1 · x1 + 0 |
[sel#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[take#(x1, x2)] | = | 1 + 1 · x1 |
[afterNth#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[activate#(x1)] | = | 0 |
[0] | = | 1 |
[pair(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[cons(x1, x2)] | = | 1 · x1 + 0 |
[n__natsFrom(x1)] | = | 1 + 1 · x1 |
natsFrom#(z0) | → | c | (16) |
natsFrom#(z0) | → | c1 | (18) |
fst#(pair(z0,z1)) | → | c2 | (20) |
snd#(pair(z0,z1)) | → | c3 | (22) |
splitAt#(0,z0) | → | c4 | (24) |
splitAt#(s(z0),cons(z1,z2)) | → | c5(u#(splitAt(z0,activate(z2)),z0,z1,activate(z2)),splitAt#(z0,activate(z2)),activate#(z2),activate#(z2)) | (26) |
u#(pair(z0,z1),z2,z3,z4) | → | c6(activate#(z3)) | (28) |
head#(cons(z0,z1)) | → | c7 | (30) |
tail#(cons(z0,z1)) | → | c8(activate#(z1)) | (32) |
sel#(z0,z1) | → | c9(head#(afterNth(z0,z1)),afterNth#(z0,z1)) | (34) |
take#(z0,z1) | → | c10(fst#(splitAt(z0,z1)),splitAt#(z0,z1)) | (36) |
afterNth#(z0,z1) | → | c11(snd#(splitAt(z0,z1)),splitAt#(z0,z1)) | (38) |
activate#(n__natsFrom(z0)) | → | c12(natsFrom#(z0)) | (40) |
activate#(z0) | → | c13 | (42) |
u#(pair(z0,z1),z2,z3,z4) | → | c6(activate#(z3)) | (28) |
sel#(z0,z1) | → | c9(head#(afterNth(z0,z1)),afterNth#(z0,z1)) | (34) |
take#(z0,z1) | → | c10(fst#(splitAt(z0,z1)),splitAt#(z0,z1)) | (36) |
[c] | = | 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8(x1)] | = | 1 · x1 + 0 |
[c9(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c10(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c11(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13] | = | 0 |
[splitAt(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[activate(x1)] | = | 1 + 1 · x1 |
[natsFrom(x1)] | = | 1 |
[u(x1,...,x4)] | = | 1 + 1 · x1 |
[afterNth(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[snd(x1)] | = | 1 · x1 + 0 |
[natsFrom#(x1)] | = | 0 |
[fst#(x1)] | = | 0 |
[snd#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[u#(x1,...,x4)] | = | 1 |
[head#(x1)] | = | 0 |
[tail#(x1)] | = | 1 + 1 · x1 |
[sel#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[take#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[afterNth#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[activate#(x1)] | = | 0 |
[0] | = | 1 |
[pair(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[nil] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[cons(x1, x2)] | = | 1 + 1 · x2 |
[n__natsFrom(x1)] | = | 0 |
natsFrom#(z0) | → | c | (16) |
natsFrom#(z0) | → | c1 | (18) |
fst#(pair(z0,z1)) | → | c2 | (20) |
snd#(pair(z0,z1)) | → | c3 | (22) |
splitAt#(0,z0) | → | c4 | (24) |
splitAt#(s(z0),cons(z1,z2)) | → | c5(u#(splitAt(z0,activate(z2)),z0,z1,activate(z2)),splitAt#(z0,activate(z2)),activate#(z2),activate#(z2)) | (26) |
u#(pair(z0,z1),z2,z3,z4) | → | c6(activate#(z3)) | (28) |
head#(cons(z0,z1)) | → | c7 | (30) |
tail#(cons(z0,z1)) | → | c8(activate#(z1)) | (32) |
sel#(z0,z1) | → | c9(head#(afterNth(z0,z1)),afterNth#(z0,z1)) | (34) |
take#(z0,z1) | → | c10(fst#(splitAt(z0,z1)),splitAt#(z0,z1)) | (36) |
afterNth#(z0,z1) | → | c11(snd#(splitAt(z0,z1)),splitAt#(z0,z1)) | (38) |
activate#(n__natsFrom(z0)) | → | c12(natsFrom#(z0)) | (40) |
activate#(z0) | → | c13 | (42) |
natsFrom(z0) | → | cons(z0,n__natsFrom(s(z0))) | (15) |
activate(n__natsFrom(z0)) | → | natsFrom(z0) | (39) |
activate(z0) | → | z0 | (41) |
natsFrom(z0) | → | n__natsFrom(z0) | (17) |
afterNth#(z0,z1) | → | c11(snd#(splitAt(z0,z1)),splitAt#(z0,z1)) | (38) |
[c] | = | 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8(x1)] | = | 1 · x1 + 0 |
[c9(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c10(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c11(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13] | = | 0 |
[splitAt(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[activate(x1)] | = | 1 + 1 · x1 |
[natsFrom(x1)] | = | 1 + 1 · x1 |
[u(x1,...,x4)] | = | 1 · x1 + 0 |
[afterNth(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[snd(x1)] | = | 1 · x1 + 0 |
[natsFrom#(x1)] | = | 0 |
[fst#(x1)] | = | 1 |
[snd#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[u#(x1,...,x4)] | = | 0 |
[head#(x1)] | = | 0 |
[tail#(x1)] | = | 1 + 1 · x1 |
[sel#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[take#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[afterNth#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[activate#(x1)] | = | 0 |
[0] | = | 0 |
[pair(x1, x2)] | = | 1 + 1 · x2 |
[nil] | = | 1 |
[s(x1)] | = | 1 · x1 + 0 |
[cons(x1, x2)] | = | 1 + 1 · x2 |
[n__natsFrom(x1)] | = | 1 · x1 + 0 |
natsFrom#(z0) | → | c | (16) |
natsFrom#(z0) | → | c1 | (18) |
fst#(pair(z0,z1)) | → | c2 | (20) |
snd#(pair(z0,z1)) | → | c3 | (22) |
splitAt#(0,z0) | → | c4 | (24) |
splitAt#(s(z0),cons(z1,z2)) | → | c5(u#(splitAt(z0,activate(z2)),z0,z1,activate(z2)),splitAt#(z0,activate(z2)),activate#(z2),activate#(z2)) | (26) |
u#(pair(z0,z1),z2,z3,z4) | → | c6(activate#(z3)) | (28) |
head#(cons(z0,z1)) | → | c7 | (30) |
tail#(cons(z0,z1)) | → | c8(activate#(z1)) | (32) |
sel#(z0,z1) | → | c9(head#(afterNth(z0,z1)),afterNth#(z0,z1)) | (34) |
take#(z0,z1) | → | c10(fst#(splitAt(z0,z1)),splitAt#(z0,z1)) | (36) |
afterNth#(z0,z1) | → | c11(snd#(splitAt(z0,z1)),splitAt#(z0,z1)) | (38) |
activate#(n__natsFrom(z0)) | → | c12(natsFrom#(z0)) | (40) |
activate#(z0) | → | c13 | (42) |
natsFrom(z0) | → | cons(z0,n__natsFrom(s(z0))) | (15) |
activate(n__natsFrom(z0)) | → | natsFrom(z0) | (39) |
activate(z0) | → | z0 | (41) |
natsFrom(z0) | → | n__natsFrom(z0) | (17) |
activate#(n__natsFrom(z0)) | → | c12(natsFrom#(z0)) | (40) |
activate#(z0) | → | c13 | (42) |
[c] | = | 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8(x1)] | = | 1 · x1 + 0 |
[c9(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c10(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c11(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13] | = | 0 |
[splitAt(x1, x2)] | = | 3 · x1 + 0 + 3 · x2 |
[activate(x1)] | = | 2 |
[natsFrom(x1)] | = | 3 + 3 · x1 |
[u(x1,...,x4)] | = | 1 · x1 + 0 + 3 · x4 |
[afterNth(x1, x2)] | = | 2 + 3 · x1 + 3 · x2 |
[snd(x1)] | = | 3 |
[natsFrom#(x1)] | = | 0 |
[fst#(x1)] | = | 1 |
[snd#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 1 · x1 + 0 |
[u#(x1,...,x4)] | = | 1 |
[head#(x1)] | = | 0 |
[tail#(x1)] | = | 3 + 3 · x1 |
[sel#(x1, x2)] | = | 1 + 3 · x1 + 3 · x2 |
[take#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[afterNth#(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[activate#(x1)] | = | 1 |
[0] | = | 1 |
[pair(x1, x2)] | = | 1 · x2 + 0 |
[nil] | = | 3 |
[s(x1)] | = | 3 + 1 · x1 |
[cons(x1, x2)] | = | 3 |
[n__natsFrom(x1)] | = | 1 · x1 + 0 |
natsFrom#(z0) | → | c | (16) |
natsFrom#(z0) | → | c1 | (18) |
fst#(pair(z0,z1)) | → | c2 | (20) |
snd#(pair(z0,z1)) | → | c3 | (22) |
splitAt#(0,z0) | → | c4 | (24) |
splitAt#(s(z0),cons(z1,z2)) | → | c5(u#(splitAt(z0,activate(z2)),z0,z1,activate(z2)),splitAt#(z0,activate(z2)),activate#(z2),activate#(z2)) | (26) |
u#(pair(z0,z1),z2,z3,z4) | → | c6(activate#(z3)) | (28) |
head#(cons(z0,z1)) | → | c7 | (30) |
tail#(cons(z0,z1)) | → | c8(activate#(z1)) | (32) |
sel#(z0,z1) | → | c9(head#(afterNth(z0,z1)),afterNth#(z0,z1)) | (34) |
take#(z0,z1) | → | c10(fst#(splitAt(z0,z1)),splitAt#(z0,z1)) | (36) |
afterNth#(z0,z1) | → | c11(snd#(splitAt(z0,z1)),splitAt#(z0,z1)) | (38) |
activate#(n__natsFrom(z0)) | → | c12(natsFrom#(z0)) | (40) |
activate#(z0) | → | c13 | (42) |
natsFrom#(z0) | → | c | (16) |
natsFrom#(z0) | → | c1 | (18) |
[c] | = | 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c6(x1)] | = | 1 · x1 + 0 |
[c7] | = | 0 |
[c8(x1)] | = | 1 · x1 + 0 |
[c9(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c10(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c11(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c12(x1)] | = | 1 · x1 + 0 |
[c13] | = | 0 |
[splitAt(x1, x2)] | = | 2 + 2 · x2 |
[activate(x1)] | = | 0 |
[natsFrom(x1)] | = | 3 + 3 · x1 |
[u(x1,...,x4)] | = | 2 · x1 + 0 |
[afterNth(x1, x2)] | = | 2 + 3 · x1 + 3 · x2 |
[snd(x1)] | = | 3 |
[natsFrom#(x1)] | = | 1 |
[fst#(x1)] | = | 1 |
[snd#(x1)] | = | 0 |
[splitAt#(x1, x2)] | = | 1 · x1 + 0 |
[u#(x1,...,x4)] | = | 1 |
[head#(x1)] | = | 0 |
[tail#(x1)] | = | 3 + 3 · x1 |
[sel#(x1, x2)] | = | 1 + 1 · x1 + 3 · x2 |
[take#(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[afterNth#(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[activate#(x1)] | = | 1 |
[0] | = | 3 |
[pair(x1, x2)] | = | 2 + 1 · x2 |
[nil] | = | 3 |
[s(x1)] | = | 3 + 1 · x1 |
[cons(x1, x2)] | = | 1 |
[n__natsFrom(x1)] | = | 0 |
natsFrom#(z0) | → | c | (16) |
natsFrom#(z0) | → | c1 | (18) |
fst#(pair(z0,z1)) | → | c2 | (20) |
snd#(pair(z0,z1)) | → | c3 | (22) |
splitAt#(0,z0) | → | c4 | (24) |
splitAt#(s(z0),cons(z1,z2)) | → | c5(u#(splitAt(z0,activate(z2)),z0,z1,activate(z2)),splitAt#(z0,activate(z2)),activate#(z2),activate#(z2)) | (26) |
u#(pair(z0,z1),z2,z3,z4) | → | c6(activate#(z3)) | (28) |
head#(cons(z0,z1)) | → | c7 | (30) |
tail#(cons(z0,z1)) | → | c8(activate#(z1)) | (32) |
sel#(z0,z1) | → | c9(head#(afterNth(z0,z1)),afterNth#(z0,z1)) | (34) |
take#(z0,z1) | → | c10(fst#(splitAt(z0,z1)),splitAt#(z0,z1)) | (36) |
afterNth#(z0,z1) | → | c11(snd#(splitAt(z0,z1)),splitAt#(z0,z1)) | (38) |
activate#(n__natsFrom(z0)) | → | c12(natsFrom#(z0)) | (40) |
activate#(z0) | → | c13 | (42) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).