ejercicio 30

problema agregarListaR (l:ListaDeReproduccion, r:Reproductor) {
requiere incluido(l,etiquetas(archivos(r)));
modifica r
asegura en(l,listas(r)) y mismos(listas(r),listas(pre(r))++ [l]);
asegura archivos(r) == archivos(pre(r))
asegura estado (r) == estado (pre(r))
asegura (¥ l’ ← [listas(r)]), l’ != l) cantRepLista(l’,r) == cantRepLista(l’,pre(r))
asegura cantRepLista(l,r) == 0
asegura (¥ t ← temas(archivos(r)), cantRepTema(t,r) == cantRepTema(t,pre(r))
}