(COMMENT generated from Maude module 'OvConsOS' by 'nosorts-noand' transformation)
(VAR IL L M N Z Y X)
(STRATEGY CONTEXTSENSITIVE

(U11 1)
(U12 1)
(U21 1)
(U22 1)
(U23 1)
(cons 1)





)
(RULES
zeros -> cons(0,zeros)

U11(tt,L) -> U12(tt,L)

U12(tt,L) -> s(length(L))

U21(tt,IL,M,N) -> U22(tt,IL,M,N)

U22(tt,IL,M,N) -> U23(tt,IL,M,N)

U23(tt,IL,M,N) -> cons(N,take(M,IL))

length(nil) -> 0

length(cons(N,L)) -> U11(tt,L)

take(0,IL) -> nil

take(s(M),cons(N,IL)) -> U21(tt,IL,M,N)
)