(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)
        
)