(VAR N XS X Y YS ZS) (RULES U101(tt) -> fst(splitAt(N,XS)) U11(tt) -> snd(splitAt(N,XS)) U21(tt) -> X U31(tt) -> N U41(tt) -> cons(N) U51(tt) -> head(afterNth(N,XS)) U61(tt) -> Y U71(tt) -> pair(nil,XS) U81(tt) -> U82(splitAt(N,XS)) U82(pair(YS,ZS)) -> pair(cons(X),ZS) U91(tt) -> XS afterNth(N,XS) -> U11(and(isNatural)) and(tt) -> X fst(pair(X,Y)) -> U21(and(isLNat)) head(cons(N)) -> U31(and(isNatural)) isLNat -> tt isLNat -> and(isNatural) isLNat -> and(isNatural) isLNat -> isPLNat isLNat -> isNatural isLNat -> isPLNat isLNat -> isLNat isLNat -> and(isNatural) isNatural -> tt isNatural -> isLNat isNatural -> isNatural isNatural -> and(isNatural) isPLNat -> and(isLNat) isPLNat -> and(isNatural) natsFrom(N) -> U41(isNatural) sel(N,XS) -> U51(and(isNatural)) snd(pair(X,Y)) -> U61(and(isLNat)) splitAt(0,XS) -> U71(isLNat) splitAt(s(N),cons(X)) -> U81(and(isNatural)) tail(cons(N)) -> U91(and(isNatural)) take(N,XS) -> U101(and(isNatural)) )