(VAR N XS X Y YS ZS X1 X2 X3 X4) (RULES active(U11(tt,N,XS)) -> mark(U12(tt,N,XS)) active(U12(tt,N,XS)) -> mark(snd(splitAt(N,XS))) active(U21(tt,X)) -> mark(U22(tt,X)) active(U22(tt,X)) -> mark(X) active(U31(tt,N)) -> mark(U32(tt,N)) active(U32(tt,N)) -> mark(N) active(U41(tt,N,XS)) -> mark(U42(tt,N,XS)) active(U42(tt,N,XS)) -> mark(head(afterNth(N,XS))) active(U51(tt,Y)) -> mark(U52(tt,Y)) active(U52(tt,Y)) -> mark(Y) active(U61(tt,N,X,XS)) -> mark(U62(tt,N,X,XS)) active(U62(tt,N,X,XS)) -> mark(U63(tt,N,X,XS)) active(U63(tt,N,X,XS)) -> mark(U64(splitAt(N,XS),X)) active(U64(pair(YS,ZS),X)) -> mark(pair(cons(X,YS),ZS)) active(U71(tt,XS)) -> mark(U72(tt,XS)) active(U72(tt,XS)) -> mark(XS) active(U81(tt,N,XS)) -> mark(U82(tt,N,XS)) active(U82(tt,N,XS)) -> mark(fst(splitAt(N,XS))) active(afterNth(N,XS)) -> mark(U11(tt,N,XS)) active(fst(pair(X,Y))) -> mark(U21(tt,X)) active(head(cons(N,XS))) -> mark(U31(tt,N)) active(natsFrom(N)) -> mark(cons(N,natsFrom(s(N)))) active(sel(N,XS)) -> mark(U41(tt,N,XS)) active(snd(pair(X,Y))) -> mark(U51(tt,Y)) active(splitAt(0,XS)) -> mark(pair(nil,XS)) active(splitAt(s(N),cons(X,XS))) -> mark(U61(tt,N,X,XS)) active(tail(cons(N,XS))) -> mark(U71(tt,XS)) active(take(N,XS)) -> mark(U81(tt,N,XS)) active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3) active(U12(X1,X2,X3)) -> U12(active(X1),X2,X3) active(snd(X)) -> snd(active(X)) active(splitAt(X1,X2)) -> splitAt(active(X1),X2) active(splitAt(X1,X2)) -> splitAt(X1,active(X2)) active(U21(X1,X2)) -> U21(active(X1),X2) active(U22(X1,X2)) -> U22(active(X1),X2) active(U31(X1,X2)) -> U31(active(X1),X2) active(U32(X1,X2)) -> U32(active(X1),X2) active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3) active(U42(X1,X2,X3)) -> U42(active(X1),X2,X3) active(head(X)) -> head(active(X)) active(afterNth(X1,X2)) -> afterNth(active(X1),X2) active(afterNth(X1,X2)) -> afterNth(X1,active(X2)) active(U51(X1,X2)) -> U51(active(X1),X2) active(U52(X1,X2)) -> U52(active(X1),X2) active(U61(X1,X2,X3,X4)) -> U61(active(X1),X2,X3,X4) active(U62(X1,X2,X3,X4)) -> U62(active(X1),X2,X3,X4) active(U63(X1,X2,X3,X4)) -> U63(active(X1),X2,X3,X4) active(U64(X1,X2)) -> U64(active(X1),X2) active(pair(X1,X2)) -> pair(active(X1),X2) active(pair(X1,X2)) -> pair(X1,active(X2)) active(cons(X1,X2)) -> cons(active(X1),X2) active(U71(X1,X2)) -> U71(active(X1),X2) active(U72(X1,X2)) -> U72(active(X1),X2) active(U81(X1,X2,X3)) -> U81(active(X1),X2,X3) active(U82(X1,X2,X3)) -> U82(active(X1),X2,X3) active(fst(X)) -> fst(active(X)) active(natsFrom(X)) -> natsFrom(active(X)) active(s(X)) -> s(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(tail(X)) -> tail(active(X)) active(take(X1,X2)) -> take(active(X1),X2) active(take(X1,X2)) -> take(X1,active(X2)) U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3)) U12(mark(X1),X2,X3) -> mark(U12(X1,X2,X3)) snd(mark(X)) -> mark(snd(X)) splitAt(mark(X1),X2) -> mark(splitAt(X1,X2)) splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2)) U21(mark(X1),X2) -> mark(U21(X1,X2)) U22(mark(X1),X2) -> mark(U22(X1,X2)) U31(mark(X1),X2) -> mark(U31(X1,X2)) U32(mark(X1),X2) -> mark(U32(X1,X2)) U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3)) U42(mark(X1),X2,X3) -> mark(U42(X1,X2,X3)) head(mark(X)) -> mark(head(X)) afterNth(mark(X1),X2) -> mark(afterNth(X1,X2)) afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2)) U51(mark(X1),X2) -> mark(U51(X1,X2)) U52(mark(X1),X2) -> mark(U52(X1,X2)) U61(mark(X1),X2,X3,X4) -> mark(U61(X1,X2,X3,X4)) U62(mark(X1),X2,X3,X4) -> mark(U62(X1,X2,X3,X4)) U63(mark(X1),X2,X3,X4) -> mark(U63(X1,X2,X3,X4)) U64(mark(X1),X2) -> mark(U64(X1,X2)) pair(mark(X1),X2) -> mark(pair(X1,X2)) pair(X1,mark(X2)) -> mark(pair(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) U71(mark(X1),X2) -> mark(U71(X1,X2)) U72(mark(X1),X2) -> mark(U72(X1,X2)) U81(mark(X1),X2,X3) -> mark(U81(X1,X2,X3)) U82(mark(X1),X2,X3) -> mark(U82(X1,X2,X3)) fst(mark(X)) -> mark(fst(X)) natsFrom(mark(X)) -> mark(natsFrom(X)) s(mark(X)) -> mark(s(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) tail(mark(X)) -> mark(tail(X)) take(mark(X1),X2) -> mark(take(X1,X2)) take(X1,mark(X2)) -> mark(take(X1,X2)) proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3)) proper(tt) -> ok(tt) proper(U12(X1,X2,X3)) -> U12(proper(X1),proper(X2),proper(X3)) proper(snd(X)) -> snd(proper(X)) proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2)) proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) proper(U22(X1,X2)) -> U22(proper(X1),proper(X2)) proper(U31(X1,X2)) -> U31(proper(X1),proper(X2)) proper(U32(X1,X2)) -> U32(proper(X1),proper(X2)) proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3)) proper(U42(X1,X2,X3)) -> U42(proper(X1),proper(X2),proper(X3)) proper(head(X)) -> head(proper(X)) proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2)) proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) proper(U52(X1,X2)) -> U52(proper(X1),proper(X2)) proper(U61(X1,X2,X3,X4)) -> U61(proper(X1),proper(X2),proper(X3),proper(X4)) proper(U62(X1,X2,X3,X4)) -> U62(proper(X1),proper(X2),proper(X3),proper(X4)) proper(U63(X1,X2,X3,X4)) -> U63(proper(X1),proper(X2),proper(X3),proper(X4)) proper(U64(X1,X2)) -> U64(proper(X1),proper(X2)) proper(pair(X1,X2)) -> pair(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) proper(U72(X1,X2)) -> U72(proper(X1),proper(X2)) proper(U81(X1,X2,X3)) -> U81(proper(X1),proper(X2),proper(X3)) proper(U82(X1,X2,X3)) -> U82(proper(X1),proper(X2),proper(X3)) proper(fst(X)) -> fst(proper(X)) proper(natsFrom(X)) -> natsFrom(proper(X)) proper(s(X)) -> s(proper(X)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(0) -> ok(0) proper(nil) -> ok(nil) proper(tail(X)) -> tail(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3)) U12(ok(X1),ok(X2),ok(X3)) -> ok(U12(X1,X2,X3)) snd(ok(X)) -> ok(snd(X)) splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2)) U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) U22(ok(X1),ok(X2)) -> ok(U22(X1,X2)) U31(ok(X1),ok(X2)) -> ok(U31(X1,X2)) U32(ok(X1),ok(X2)) -> ok(U32(X1,X2)) U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3)) U42(ok(X1),ok(X2),ok(X3)) -> ok(U42(X1,X2,X3)) head(ok(X)) -> ok(head(X)) afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2)) U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) U52(ok(X1),ok(X2)) -> ok(U52(X1,X2)) U61(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U61(X1,X2,X3,X4)) U62(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U62(X1,X2,X3,X4)) U63(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U63(X1,X2,X3,X4)) U64(ok(X1),ok(X2)) -> ok(U64(X1,X2)) pair(ok(X1),ok(X2)) -> ok(pair(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) U72(ok(X1),ok(X2)) -> ok(U72(X1,X2)) U81(ok(X1),ok(X2),ok(X3)) -> ok(U81(X1,X2,X3)) U82(ok(X1),ok(X2),ok(X3)) -> ok(U82(X1,X2,X3)) fst(ok(X)) -> ok(fst(X)) natsFrom(ok(X)) -> ok(natsFrom(X)) s(ok(X)) -> ok(s(X)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) tail(ok(X)) -> ok(tail(X)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) )