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) |
U11#(tt,N,XS) |
→ |
activate#(XS) |
(34) |
U11#(tt,N,XS) |
→ |
activate#(N) |
(35) |
U11#(tt,N,XS) |
→ |
U12#(tt,activate(N),activate(XS)) |
(36) |
U12#(tt,N,XS) |
→ |
activate#(XS) |
(37) |
U12#(tt,N,XS) |
→ |
activate#(N) |
(38) |
U12#(tt,N,XS) |
→ |
splitAt#(activate(N),activate(XS)) |
(39) |
U12#(tt,N,XS) |
→ |
snd#(splitAt(activate(N),activate(XS))) |
(40) |
U21#(tt,X) |
→ |
activate#(X) |
(41) |
U21#(tt,X) |
→ |
U22#(tt,activate(X)) |
(42) |
U22#(tt,X) |
→ |
activate#(X) |
(43) |
U31#(tt,N) |
→ |
activate#(N) |
(44) |
U31#(tt,N) |
→ |
U32#(tt,activate(N)) |
(45) |
U32#(tt,N) |
→ |
activate#(N) |
(46) |
U41#(tt,N,XS) |
→ |
activate#(XS) |
(47) |
U41#(tt,N,XS) |
→ |
activate#(N) |
(48) |
U41#(tt,N,XS) |
→ |
U42#(tt,activate(N),activate(XS)) |
(49) |
U42#(tt,N,XS) |
→ |
activate#(XS) |
(50) |
U42#(tt,N,XS) |
→ |
activate#(N) |
(51) |
U42#(tt,N,XS) |
→ |
afterNth#(activate(N),activate(XS)) |
(52) |
U42#(tt,N,XS) |
→ |
head#(afterNth(activate(N),activate(XS))) |
(53) |
U51#(tt,Y) |
→ |
activate#(Y) |
(54) |
U51#(tt,Y) |
→ |
U52#(tt,activate(Y)) |
(55) |
U52#(tt,Y) |
→ |
activate#(Y) |
(56) |
U61#(tt,N,X,XS) |
→ |
activate#(XS) |
(57) |
U61#(tt,N,X,XS) |
→ |
activate#(X) |
(58) |
U61#(tt,N,X,XS) |
→ |
activate#(N) |
(59) |
U61#(tt,N,X,XS) |
→ |
U62#(tt,activate(N),activate(X),activate(XS)) |
(60) |
U62#(tt,N,X,XS) |
→ |
activate#(XS) |
(61) |
U62#(tt,N,X,XS) |
→ |
activate#(X) |
(62) |
U62#(tt,N,X,XS) |
→ |
activate#(N) |
(63) |
U62#(tt,N,X,XS) |
→ |
U63#(tt,activate(N),activate(X),activate(XS)) |
(64) |
U63#(tt,N,X,XS) |
→ |
activate#(X) |
(65) |
U63#(tt,N,X,XS) |
→ |
activate#(XS) |
(66) |
U63#(tt,N,X,XS) |
→ |
activate#(N) |
(67) |
U63#(tt,N,X,XS) |
→ |
splitAt#(activate(N),activate(XS)) |
(68) |
U63#(tt,N,X,XS) |
→ |
U64#(splitAt(activate(N),activate(XS)),activate(X)) |
(69) |
U64#(pair(YS,ZS),X) |
→ |
activate#(X) |
(70) |
U71#(tt,XS) |
→ |
activate#(XS) |
(71) |
U71#(tt,XS) |
→ |
U72#(tt,activate(XS)) |
(72) |
U72#(tt,XS) |
→ |
activate#(XS) |
(73) |
U81#(tt,N,XS) |
→ |
activate#(XS) |
(74) |
U81#(tt,N,XS) |
→ |
activate#(N) |
(75) |
U81#(tt,N,XS) |
→ |
U82#(tt,activate(N),activate(XS)) |
(76) |
U82#(tt,N,XS) |
→ |
activate#(XS) |
(77) |
U82#(tt,N,XS) |
→ |
activate#(N) |
(78) |
U82#(tt,N,XS) |
→ |
splitAt#(activate(N),activate(XS)) |
(79) |
U82#(tt,N,XS) |
→ |
fst#(splitAt(activate(N),activate(XS))) |
(80) |
afterNth#(N,XS) |
→ |
U11#(tt,N,XS) |
(81) |
fst#(pair(X,Y)) |
→ |
U21#(tt,X) |
(82) |
head#(cons(N,XS)) |
→ |
U31#(tt,N) |
(83) |
sel#(N,XS) |
→ |
U41#(tt,N,XS) |
(84) |
snd#(pair(X,Y)) |
→ |
U51#(tt,Y) |
(85) |
splitAt#(s(N),cons(X,XS)) |
→ |
activate#(XS) |
(86) |
splitAt#(s(N),cons(X,XS)) |
→ |
U61#(tt,N,X,activate(XS)) |
(87) |
tail#(cons(N,XS)) |
→ |
activate#(XS) |
(88) |
tail#(cons(N,XS)) |
→ |
U71#(tt,activate(XS)) |
(89) |
take#(N,XS) |
→ |
U81#(tt,N,XS) |
(90) |
activate#(n__natsFrom(X)) |
→ |
activate#(X) |
(91) |
activate#(n__natsFrom(X)) |
→ |
natsFrom#(activate(X)) |
(92) |
activate#(n__s(X)) |
→ |
activate#(X) |
(93) |
activate#(n__s(X)) |
→ |
s#(activate(X)) |
(94) |
The dependency pairs are split into 2
components.