aed1-tpe/textoPlano/punto 10

10.
problema losMasFracasados (j: JJOO, p:Pais) = result:[Atleta]{
	//Interpretación: Devuelve los atletas del país p que no
	//ganaron medallas en las competencias acabadas hasta ahora,
	//ordenados desde el que en más competencias participó hasta el que que menos.

	asegura noGanaronMedallas: (paraTodo x <- [noGanoMedallas(atl, comp) | atl <- result, comp <- todasLasCompetencias(j), finalizada(comp)]) x;
	asegura todosDelPais: (paraTodo x <- result) nacionalidad(x) == p;
	asegura (paraTodo x <- result, y <- atletas(j), nacionalidad(y)==p) competenciasEnLasQueParticipó(j, x) >= competenciasEnLasQueParticipó(j, y);
}

aux competenciasEnLasQueParticipó(j: JJOO, a:Atleta) : int =
	long([z | z<- todasLasCompetencias(j), en(a, participantes(z))]);

aux noGanoMedallas(atl: Atleta, comp: Competencia) : Bool = (ciaNumber(ranking(comp)[0]) != ciaNumber(atl) && ciaNumber(ranking(comp)[1]) != ciaNumber(atl) && ciaNumber(ranking(comp)[2]) != ciaNumber(atl));