Ejercicios 16,20,24, 28(28:Incompleto) y 32

16)
problema eliminarTemasSA(n:Nombre, l:[etiqueta],s:SA){
modifica s
asegura mismos (etiquetas(s),etiquetas(pre(s)));//no se que hacer en el caso que el tema que borre era el unico que tenia cierta etiqueta.(si saco la etiqueta de el SA o no)
asegura (¥ t<- temas(s))¬(nombre(t)==n y mismos(etiquetas(t),l));
asegura (¥ t <- temas(s))(E t' <- temas(pre(s)),¬(nombre(t)==n y mismos(etiquetas(t),l))) t == t';
}

20)
problema eliminarEtiquetaDeTema(t:Tema, e:Etiqueta, s:SA){
requiere en(e,etiquetas(s));
modifica s;
asegura Mismos(etiquetas(s),etiquetas(pre(s)));
asegura (¥ h <- temas(s), TemasIguales(h,t))mismos(etiquetas(t),etiquetas(h)++[e]);
}

24)
invariante LasListasSonValidas:
(¥ x <- listas(r:Reproductor))(¥ y <- x) en(y,etiquetas(archivo(r:Reproductor)));

28)
// este lo dejo para despues por que hay que hacer el aux indexador.

32)
problema hitR(r:Reproductor) result:Tema{
requiere |temas(archivos(r))| > 0
asegura en(result,temas(archivos(r)))
asegura (¥ h <- temas(archivos(r))) CantRepTemas(result) >= CantRepTemas(h)
}

16)
problema eliminarTemasSA(n:Nombre, l:[etiqueta],s:SA){
modifica s
asegura mismos (etiquetas(s),etiquetas(pre(s)));//no se que hacer en el caso que el tema que borre era el unico que tenia cierta etiqueta.(si saco la etiqueta de el SA o no)
asegura (¥ t<- temas(s))(nombre(t)==n y mismos(etiquetas(t),l));
asegura (¥ t <- temas(s))(E t' <- temas(pre(s)),(nombre(t)==n y mismos(etiquetas(t),l))) t == t';
}// Este creo que está perfecto. La única duda es lo que pusiste vos.

20)
problema eliminarEtiquetaDeTema(t:Tema, e:Etiqueta, s:SA){
requiere en(e,etiquetas(s));
modifica s;
asegura Mismos(etiquetas(s),etiquetas(pre(s)));
asegura (¥ h <- temas(s), TemasIguales(h,t))mismos(etiquetas(t),etiquetas(h)++[e]);
}// Supongo que acá surge la misma duda de antes sobre si la etiqueta estaba solo en ese tema. Para mi el requiere no va, si no existe o no es válida no hace nada, pero el requiere te dice que no lo podés usar en ese caso. Habría que usar implica o if else. El último asegura me parece que tendrías que asegurar también que los demás temas que las etiquetas no cambian. O eso es sobreespecificar? No me acuerdo si había que asegurarse que todo ande bien cuando modificabas como cuando hacías una cosa de tipo nueva.

24)
invariante LasListasSonValidas:
(¥ x <- listas(r:Reproductor))(¥ y <- x) en(y,etiquetas(archivo(r:Reproductor)));//Está perfecto para mí.

28)
// este lo dejo para despues por que hay que hacer el aux indexador.

32)
problema hitR(r:Reproductor) result:Tema{
requiere |temas(archivos(r))| > 0;
asegura en(result,temas(archivos(r)));
asegura (¥ h <- temas(archivos(r))) CantRepTemas(result) >= CantRepTemas(h);
}Jaja, yo sin querer había hecho esto en el ejericio 50 porque no entendía al princpipio que quería decir temaContenidoEnMasListas. asegura Mayor(cantRepTema(result,r),[cantRepTema(x,r) | x ←archivos(r)]); Fijate cual te gusta más, creo que los dos están bien.

20)
problema eliminarEtiquetaDeTema(t:Tema, e:Etiqueta, s:SA){
requiere en(e,etiquetas(s));
modifica s;
asegura Mismos(etiquetas(s),etiquetas(pre(s)));
asegura (¥ h <- temas(s), TemasIguales(h,t))mismos(etiquetas(t),etiquetas(h)++[e]);

// tambien vamos a tener que tener cuidado del ejemplo shakira etiquetas 1, 2, 3. Tendríamos que requerir entonces que no exista un tema que tiene etiquetas(t) - e = etiquetas (t').