The rewrite relation of the following TRS is considered.
U11(tt,N,XS) | → | U12(tt,activate(N),activate(XS)) | (1) |
U12(tt,N,XS) | → | snd(splitAt(activate(N),activate(XS))) | (2) |
U21(tt,X) | → | U22(tt,activate(X)) | (3) |
U22(tt,X) | → | activate(X) | (4) |
U31(tt,N) | → | U32(tt,activate(N)) | (5) |
U32(tt,N) | → | activate(N) | (6) |
U41(tt,N,XS) | → | U42(tt,activate(N),activate(XS)) | (7) |
U42(tt,N,XS) | → | head(afterNth(activate(N),activate(XS))) | (8) |
U51(tt,Y) | → | U52(tt,activate(Y)) | (9) |
U52(tt,Y) | → | activate(Y) | (10) |
U61(tt,N,X,XS) | → | U62(tt,activate(N),activate(X),activate(XS)) | (11) |
U62(tt,N,X,XS) | → | U63(tt,activate(N),activate(X),activate(XS)) | (12) |
U63(tt,N,X,XS) | → | U64(splitAt(activate(N),activate(XS)),activate(X)) | (13) |
U64(pair(YS,ZS),X) | → | pair(cons(activate(X),YS),ZS) | (14) |
U71(tt,XS) | → | U72(tt,activate(XS)) | (15) |
U72(tt,XS) | → | activate(XS) | (16) |
U81(tt,N,XS) | → | U82(tt,activate(N),activate(XS)) | (17) |
U82(tt,N,XS) | → | fst(splitAt(activate(N),activate(XS))) | (18) |
afterNth(N,XS) | → | U11(tt,N,XS) | (19) |
fst(pair(X,Y)) | → | U21(tt,X) | (20) |
head(cons(N,XS)) | → | U31(tt,N) | (21) |
natsFrom(N) | → | cons(N,n__natsFrom(n__s(N))) | (22) |
sel(N,XS) | → | U41(tt,N,XS) | (23) |
snd(pair(X,Y)) | → | U51(tt,Y) | (24) |
splitAt(0,XS) | → | pair(nil,XS) | (25) |
splitAt(s(N),cons(X,XS)) | → | U61(tt,N,X,activate(XS)) | (26) |
tail(cons(N,XS)) | → | U71(tt,activate(XS)) | (27) |
take(N,XS) | → | U81(tt,N,XS) | (28) |
natsFrom(X) | → | n__natsFrom(X) | (29) |
s(X) | → | n__s(X) | (30) |
activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | (31) |
activate(n__s(X)) | → | s(activate(X)) | (32) |
activate(X) | → | X | (33) |
U12#(tt,N,XS) | → | splitAt#(activate(N),activate(XS)) | (34) |
splitAt#(s(N),cons(X,XS)) | → | activate#(XS) | (35) |
U41#(tt,N,XS) | → | activate#(XS) | (36) |
tail#(cons(N,XS)) | → | activate#(XS) | (37) |
U21#(tt,X) | → | U22#(tt,activate(X)) | (38) |
splitAt#(s(N),cons(X,XS)) | → | U61#(tt,N,X,activate(XS)) | (39) |
afterNth#(N,XS) | → | U11#(tt,N,XS) | (40) |
U81#(tt,N,XS) | → | activate#(N) | (41) |
U21#(tt,X) | → | activate#(X) | (42) |
U42#(tt,N,XS) | → | activate#(N) | (43) |
U11#(tt,N,XS) | → | U12#(tt,activate(N),activate(XS)) | (44) |
U82#(tt,N,XS) | → | fst#(splitAt(activate(N),activate(XS))) | (45) |
U82#(tt,N,XS) | → | activate#(XS) | (46) |
U81#(tt,N,XS) | → | activate#(XS) | (47) |
U63#(tt,N,X,XS) | → | U64#(splitAt(activate(N),activate(XS)),activate(X)) | (48) |
U82#(tt,N,XS) | → | splitAt#(activate(N),activate(XS)) | (49) |
U71#(tt,XS) | → | U72#(tt,activate(XS)) | (50) |
activate#(n__s(X)) | → | activate#(X) | (51) |
U42#(tt,N,XS) | → | head#(afterNth(activate(N),activate(XS))) | (52) |
U61#(tt,N,X,XS) | → | U62#(tt,activate(N),activate(X),activate(XS)) | (53) |
U63#(tt,N,X,XS) | → | activate#(XS) | (54) |
U51#(tt,Y) | → | U52#(tt,activate(Y)) | (55) |
U22#(tt,X) | → | activate#(X) | (56) |
activate#(n__natsFrom(X)) | → | activate#(X) | (57) |
activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | (58) |
U72#(tt,XS) | → | activate#(XS) | (59) |
U51#(tt,Y) | → | activate#(Y) | (60) |
U31#(tt,N) | → | U32#(tt,activate(N)) | (61) |
U71#(tt,XS) | → | activate#(XS) | (62) |
U61#(tt,N,X,XS) | → | activate#(N) | (63) |
U52#(tt,Y) | → | activate#(Y) | (64) |
U42#(tt,N,XS) | → | afterNth#(activate(N),activate(XS)) | (65) |
U11#(tt,N,XS) | → | activate#(N) | (66) |
U64#(pair(YS,ZS),X) | → | activate#(X) | (67) |
U62#(tt,N,X,XS) | → | activate#(N) | (68) |
U63#(tt,N,X,XS) | → | splitAt#(activate(N),activate(XS)) | (69) |
activate#(n__s(X)) | → | s#(activate(X)) | (70) |
U63#(tt,N,X,XS) | → | activate#(X) | (71) |
take#(N,XS) | → | U81#(tt,N,XS) | (72) |
U32#(tt,N) | → | activate#(N) | (73) |
head#(cons(N,XS)) | → | U31#(tt,N) | (74) |
U41#(tt,N,XS) | → | activate#(N) | (75) |
U62#(tt,N,X,XS) | → | activate#(XS) | (76) |
tail#(cons(N,XS)) | → | U71#(tt,activate(XS)) | (77) |
U41#(tt,N,XS) | → | U42#(tt,activate(N),activate(XS)) | (78) |
U82#(tt,N,XS) | → | activate#(N) | (79) |
snd#(pair(X,Y)) | → | U51#(tt,Y) | (80) |
U31#(tt,N) | → | activate#(N) | (81) |
U62#(tt,N,X,XS) | → | U63#(tt,activate(N),activate(X),activate(XS)) | (82) |
fst#(pair(X,Y)) | → | U21#(tt,X) | (83) |
U81#(tt,N,XS) | → | U82#(tt,activate(N),activate(XS)) | (84) |
U62#(tt,N,X,XS) | → | activate#(X) | (85) |
U61#(tt,N,X,XS) | → | activate#(XS) | (86) |
U12#(tt,N,XS) | → | activate#(N) | (87) |
U12#(tt,N,XS) | → | snd#(splitAt(activate(N),activate(XS))) | (88) |
U42#(tt,N,XS) | → | activate#(XS) | (89) |
U63#(tt,N,X,XS) | → | activate#(N) | (90) |
U61#(tt,N,X,XS) | → | activate#(X) | (91) |
U12#(tt,N,XS) | → | activate#(XS) | (92) |
U11#(tt,N,XS) | → | activate#(XS) | (93) |
sel#(N,XS) | → | U41#(tt,N,XS) | (94) |
The dependency pairs are split into 2 components.
U61#(tt,N,X,XS) | → | U62#(tt,activate(N),activate(X),activate(XS)) | (53) |
U62#(tt,N,X,XS) | → | U63#(tt,activate(N),activate(X),activate(XS)) | (82) |
splitAt#(s(N),cons(X,XS)) | → | U61#(tt,N,X,activate(XS)) | (39) |
U63#(tt,N,X,XS) | → | splitAt#(activate(N),activate(XS)) | (69) |
[U72#(x1, x2)] | = | 0 |
[U32#(x1, x2)] | = | 0 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 0 |
[U64(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 23618 |
[take#(x1, x2)] | = | 0 |
[U42(x1, x2, x3)] | = | 0 |
[activate(x1)] | = | x1 + 1 |
[U82#(x1, x2, x3)] | = | 0 |
[take(x1, x2)] | = | 0 |
[U71(x1, x2)] | = | 0 |
[U81#(x1, x2, x3)] | = | 0 |
[pair(x1, x2)] | = | 0 |
[fst(x1)] | = | 0 |
[activate#(x1)] | = | 0 |
[natsFrom(x1)] | = | 1 |
[head#(x1)] | = | 0 |
[U63(x1,...,x4)] | = | 0 |
[splitAt(x1, x2)] | = | 0 |
[U72(x1, x2)] | = | 0 |
[fst#(x1)] | = | 0 |
[U52#(x1, x2)] | = | 0 |
[U12(x1, x2, x3)] | = | 0 |
[n__natsFrom(x1)] | = | 1 |
[n__s(x1)] | = | x1 + 23618 |
[U42#(x1, x2, x3)] | = | 0 |
[U12#(x1, x2, x3)] | = | 0 |
[tail(x1)] | = | 0 |
[U62#(x1,...,x4)] | = | x1 + x2 + 14 |
[0] | = | 0 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 0 |
[nil] | = | 0 |
[U62(x1,...,x4)] | = | 0 |
[tail#(x1)] | = | 0 |
[U63#(x1,...,x4)] | = | x1 + x2 + 12 |
[splitAt#(x1, x2)] | = | x1 + 13 |
[afterNth#(x1, x2)] | = | 0 |
[U32(x1, x2)] | = | 0 |
[U52(x1, x2)] | = | 0 |
[U61(x1,...,x4)] | = | 0 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1, x2, x3)] | = | 0 |
[U64#(x1, x2)] | = | 0 |
[U31(x1, x2)] | = | 0 |
[head(x1)] | = | 0 |
[snd#(x1)] | = | 0 |
[U41#(x1, x2, x3)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[natsFrom#(x1)] | = | 0 |
[snd(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U81(x1, x2, x3)] | = | 0 |
[U82(x1, x2, x3)] | = | 0 |
[U22#(x1, x2)] | = | 0 |
[tt] | = | 3 |
[U71#(x1, x2)] | = | 0 |
[U22(x1, x2)] | = | 0 |
[U51(x1, x2)] | = | 0 |
[U41(x1, x2, x3)] | = | 0 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1,...,x4)] | = | x1 + x2 + 16 |
activate(n__s(X)) | → | s(activate(X)) | (32) |
natsFrom(N) | → | cons(N,n__natsFrom(n__s(N))) | (22) |
activate(X) | → | X | (33) |
s(X) | → | n__s(X) | (30) |
activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | (31) |
natsFrom(X) | → | n__natsFrom(X) | (29) |
U61#(tt,N,X,XS) | → | U62#(tt,activate(N),activate(X),activate(XS)) | (53) |
U62#(tt,N,X,XS) | → | U63#(tt,activate(N),activate(X),activate(XS)) | (82) |
splitAt#(s(N),cons(X,XS)) | → | U61#(tt,N,X,activate(XS)) | (39) |
U63#(tt,N,X,XS) | → | splitAt#(activate(N),activate(XS)) | (69) |
The dependency pairs are split into 0 components.
activate#(n__natsFrom(X)) | → | activate#(X) | (57) |
activate#(n__s(X)) | → | activate#(X) | (51) |
[U72#(x1, x2)] | = | 0 |
[U32#(x1, x2)] | = | 0 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 0 |
[U64(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1, x2, x3)] | = | 0 |
[activate(x1)] | = | x1 + 0 |
[U82#(x1, x2, x3)] | = | 0 |
[take(x1, x2)] | = | 0 |
[U71(x1, x2)] | = | 0 |
[U81#(x1, x2, x3)] | = | 0 |
[pair(x1, x2)] | = | 0 |
[fst(x1)] | = | 0 |
[activate#(x1)] | = | x1 + 0 |
[natsFrom(x1)] | = | x1 + 1 |
[head#(x1)] | = | 0 |
[U63(x1,...,x4)] | = | 0 |
[splitAt(x1, x2)] | = | 0 |
[U72(x1, x2)] | = | 0 |
[fst#(x1)] | = | 0 |
[U52#(x1, x2)] | = | 0 |
[U12(x1, x2, x3)] | = | 0 |
[n__natsFrom(x1)] | = | x1 + 1 |
[n__s(x1)] | = | x1 + 0 |
[U42#(x1, x2, x3)] | = | 0 |
[U12#(x1, x2, x3)] | = | 0 |
[tail(x1)] | = | 0 |
[U62#(x1,...,x4)] | = | x2 + 14 |
[0] | = | 0 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 0 |
[nil] | = | 0 |
[U62(x1,...,x4)] | = | 0 |
[tail#(x1)] | = | 0 |
[U63#(x1,...,x4)] | = | x2 + 12 |
[splitAt#(x1, x2)] | = | x1 + 13 |
[afterNth#(x1, x2)] | = | 0 |
[U32(x1, x2)] | = | 0 |
[U52(x1, x2)] | = | 0 |
[U61(x1,...,x4)] | = | 0 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1, x2, x3)] | = | 0 |
[U64#(x1, x2)] | = | 0 |
[U31(x1, x2)] | = | 0 |
[head(x1)] | = | 0 |
[snd#(x1)] | = | 0 |
[U41#(x1, x2, x3)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[natsFrom#(x1)] | = | 0 |
[snd(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U81(x1, x2, x3)] | = | 0 |
[U82(x1, x2, x3)] | = | 0 |
[U22#(x1, x2)] | = | 0 |
[tt] | = | 3 |
[U71#(x1, x2)] | = | 0 |
[U22(x1, x2)] | = | 0 |
[U51(x1, x2)] | = | 0 |
[U41(x1, x2, x3)] | = | 0 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1,...,x4)] | = | 16 |
activate(n__s(X)) | → | s(activate(X)) | (32) |
natsFrom(N) | → | cons(N,n__natsFrom(n__s(N))) | (22) |
activate(X) | → | X | (33) |
s(X) | → | n__s(X) | (30) |
activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | (31) |
natsFrom(X) | → | n__natsFrom(X) | (29) |
activate#(n__natsFrom(X)) | → | activate#(X) | (57) |
The dependency pairs are split into 1 component.
activate#(n__s(X)) | → | activate#(X) | (51) |
[U72#(x1, x2)] | = | 0 |
[U32#(x1, x2)] | = | 0 |
[U21(x1, x2)] | = | 0 |
[U11(x1, x2, x3)] | = | 0 |
[U64(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 17888 |
[take#(x1, x2)] | = | 0 |
[U42(x1, x2, x3)] | = | 0 |
[activate(x1)] | = | x1 + 0 |
[U82#(x1, x2, x3)] | = | 0 |
[take(x1, x2)] | = | 0 |
[U71(x1, x2)] | = | 0 |
[U81#(x1, x2, x3)] | = | 0 |
[pair(x1, x2)] | = | 0 |
[fst(x1)] | = | 0 |
[activate#(x1)] | = | x1 + 0 |
[natsFrom(x1)] | = | x1 + 1 |
[head#(x1)] | = | 0 |
[U63(x1,...,x4)] | = | 0 |
[splitAt(x1, x2)] | = | 0 |
[U72(x1, x2)] | = | 0 |
[fst#(x1)] | = | 0 |
[U52#(x1, x2)] | = | 0 |
[U12(x1, x2, x3)] | = | 0 |
[n__natsFrom(x1)] | = | x1 + 1 |
[n__s(x1)] | = | x1 + 17888 |
[U42#(x1, x2, x3)] | = | 0 |
[U12#(x1, x2, x3)] | = | 0 |
[tail(x1)] | = | 0 |
[U62#(x1,...,x4)] | = | x2 + 14 |
[0] | = | 0 |
[sel#(x1, x2)] | = | 0 |
[sel(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[afterNth(x1, x2)] | = | 0 |
[nil] | = | 0 |
[U62(x1,...,x4)] | = | 0 |
[tail#(x1)] | = | 0 |
[U63#(x1,...,x4)] | = | x2 + 12 |
[splitAt#(x1, x2)] | = | x1 + 13 |
[afterNth#(x1, x2)] | = | 0 |
[U32(x1, x2)] | = | 0 |
[U52(x1, x2)] | = | 0 |
[U61(x1,...,x4)] | = | 0 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1, x2, x3)] | = | 0 |
[U64#(x1, x2)] | = | 0 |
[U31(x1, x2)] | = | 0 |
[head(x1)] | = | 0 |
[snd#(x1)] | = | 0 |
[U41#(x1, x2, x3)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[natsFrom#(x1)] | = | 0 |
[snd(x1)] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U81(x1, x2, x3)] | = | 0 |
[U82(x1, x2, x3)] | = | 0 |
[U22#(x1, x2)] | = | 0 |
[tt] | = | 3 |
[U71#(x1, x2)] | = | 0 |
[U22(x1, x2)] | = | 0 |
[U51(x1, x2)] | = | 0 |
[U41(x1, x2, x3)] | = | 0 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1,...,x4)] | = | 16 |
activate(n__s(X)) | → | s(activate(X)) | (32) |
natsFrom(N) | → | cons(N,n__natsFrom(n__s(N))) | (22) |
activate(X) | → | X | (33) |
s(X) | → | n__s(X) | (30) |
activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | (31) |
natsFrom(X) | → | n__natsFrom(X) | (29) |
activate#(n__s(X)) | → | activate#(X) | (51) |
The dependency pairs are split into 0 components.