(VAR L N IL M) (RULES zeros -> cons(0) U11(tt) -> U12(tt) U12(tt) -> s(length(L)) U21(tt) -> U22(tt) U22(tt) -> U23(tt) U23(tt) -> cons(N) length(nil) -> 0 length(cons(N)) -> U11(tt) take(0,IL) -> nil take(s(M),cons(N)) -> U21(tt) )