aed1-tpe/textoPlano/punto 9

problema boicotPorDisciplna (j:JJOO, cat: (deporte,sexo), p:pais) = res : Int {

	requiere existe (c <- todasLasCompetencias(j)) categoria(c) == cat;
	requiere finalizada (competenciaFiltrada(j,cat)) == false     // asumimos que se saca a los participantes antes de finalizar la competencia


	modifica j;

	asegura finalizada ( competenciaFiltrada(j,cat) ) == finalizada (competenciaFiltrada(pre(j),cat));
	asegura año(j) == año(pre(j));
	asegura mismos(atletas(j), atletas(pre(j)));
	asegura cantDias(j) == cantDias(pre(j));
	asegura jornadaActual(j) == jornadaActual(pre(j));


	asegura (ParaTodo dia <- [1..cantDias (j)] ) |cronograma(j,dia) | == |cronograma(pre(j), dia)|;

	asegura (ParaTodo dia <- [1..cantDias(j)])
		(ParaTodo x <- [1..(long(cronograma(j,dia))-1)])
		((cronograma (j,dia)[x] == cronograma (pre(j),dia) [x]) || ( categoria(cronograma(j,dia)[x]) == (categoria(cronograma(pre(j),dia)[x])) && (categoria(cronograma(j,dia)[x]) == cat )))

	asegura (ParaToda comp <- todasLasCompetencias(j), categoria(comp) == cat)
		(ParaTodo atl <- participantes(comp)) nacionalidad (atl) != p;

	asegura mismos (participantes(competenciaFiltrada(j,cat)), [x | x <- participantes(competenciaFiltrada(pre(j),cat)), nacionalidad(x) != p])

	asegura res == |[x | comp <- todasLasCompetencias(pre(j)), x <- participantes(comp), (categoria(comp) == cat && nacionalidad(x) == p)]|;

	/*
	+---------------------+
	| v AUXILIAR GLOBAL v |
	+---------------------+
	*/
	aux todasLasCompetencias (j:JJOO) : [competencia] = [x | y <- [1..cantDIas(j)], x <- cronogramas(j,y) ] ;

	aux competenciaFiltrada ( j:JJOO, c:(deporte,sexo) ) : competencia = cab( [x | x <- todasLasCompetencias(j), c== categoria(x) ] )
}