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