Ejercicios 22 y 26

22)
invariante laListaDelEstadoEsUnaListaValida:
en (sgd(estado(r)) , listas(r)) o sgd(estado(r)) == []

26)
problema reproducirR (r:Reproductor, l:ListaDeReproduccion) {
requiere en(l,listas(r)) o (l == []);
modifica r
asegura archivos(r) == archivos(pre(r))
asegura listas(r) == listas(pre(r))
asegura cantRepLista(l,r) == cantRepLista(l,pre(r)) + 1
asegura cantRepTema(PrimerTemaDeLaListaDeRep(r),r) == cantRepTema(PrimerTemaDeLaListaDeRep(r),pre(r)) + 1
asegura If l == [] Then prm(estado(r)) == 0 Else (sgd(estado(r)) == l y prm(estado(r)) == 1);
}

Están bien, mi única duda es lo de estado (0,[]), si el Z vendría a ser un indice, este no sería cero... directamente no existiría. El resto de las cosas están bien, te olvidás los ";" pero eso es un detalle.

;
;
;
;
jajaja ya voy a aprender.

El tema del indice, creo yo... es que funciona como indice si es mayor que uno, y dice "el reproductor esta detenido" si es 0. Al menos esa es mi interpretacion