problema 16

16.

problema eliminarTemasSA(n:Nombre, l:[etiqueta],s:SA){
requiere (existe t <- temas(pre (s)) ) nombre(t)==n y mismos (l , etiquetas (t))
modifica s
asegura mismos (etiquetas(s),Resta (etiquetas(pre(s)), UnicasEtiquetasTema(l,n, pre(s) ) );//siguiendo el 15 saco las etiquetas q no estan mas.
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';
}

aux UnicasEtiquetasTema( l: [Etiqueta] , n: Nombre, s: SA) : [etiqueta]=
[ e | e <- etiquetas (pre(s)), en( e, l) y ( ¥ t <- temas(s), ¬ (nombre(t)==n y mismos(etiquetas(t),l)) ) ¬en(e, etiquetas(t) ]

problema eliminarTemasSA(n:Nombre, l:[etiqueta],s:SA){
requiere (existe t <- temas(pre (s)) ) nombre(t)==n y mismos (l , etiquetas (t))
modifica s
asegura mismos (etiquetas(s),Resta (etiquetas(pre(s)), UnicasEtiquetasTema(l,n, pre(s) ) );//siguiendo el 15 saco las etiquetas q no estan mas.
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';
}

Estas seguro que hace falta eso? porque estas recorriendo los t del SA nuevo... donde no esta ese tema por el asegura anterior...

problema eliminarTemasSA(n:Nombre, l:[etiqueta],s:SA){
requiere (existe t <- temas(pre (s)) ) nombre(t)==n y mismos (l , etiquetas (t))
modifica s
asegura mismos (etiquetas(s),Resta (etiquetas(pre(s)), UnicasEtiquetasTema(l,n, pre(s) ) );//siguiendo el 15 saco las etiquetas q no estan mas.
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';
}


lo que estoy asegurando en la ultima parte es q , exceptuando el tema que saque, para todo tema en el s nuevo, existe uno en el pre(s) que le corresponde.