(VAR L N X) (RULES zeros -> cons(0,n__zeros) U11(tt,L) -> U12(tt,activate(L)) U12(tt,L) -> s(length(activate(L))) length(nil) -> 0 length(cons(N,L)) -> U11(tt,activate(L)) zeros -> n__zeros activate(n__zeros) -> zeros activate(X) -> X )