\begin{problema}{medallero}{j: JJOO}{[(Pais, [\ent])]}
	//Se asegura que el resultado y el medallero sin repeticiones tengan los mismos elementos.\newline
	\asegura{mismos(result, sacarSinMedallas(crearMedallero(j)))}
	//Se asegura de que el medallero est\'e ordenado de mayor a menor.\newline
	\asegura{medalleroOrdenado(result)}

	\aux{listaNacionalidadesAtletas}{j: JJOO}{[Pais]}{[nacionalidad(at) | at \leftarrow atletas(j)]}
	//Crea una lista a partir de las nacionalidades de los atletas. Si hay dos atletas rusos, Rusia aparece dos veces.\newline

	\aux{sacarRepeticiones}{ls : [T]}{[T]}{[ls[x] | x \leftarrow [0..|ls|-1], \neg en(ls[x], ls[0..x-1])]}
	//Dada una lista cualquiera, describe una lista con una sola aparici\'on de cada elemento de la lista original.\newline

	\aux{listaPaises}{j: JJOO}{[Pais]}{sacarRepeticiones(listaNacionalidadesAtletas(j))}
	//ListaPaises decribe la lista de los pa\'ises participantes de los juegos, sin repeticiones.\newline

	\aux{cuenta}{x: T, a: [T]}{\ent}{|[y | y \leftarrow a, y == x]|}
	//Cuenta las apariciones del elemento x en la lista a.\newline

	\aux{nacionalidadPrimerosTres}{c:Competencia}{[Pais]}{\newline
	[ifthenelse(i \leq |ranking (c)|-1, nacionalidad(ranking(c)[i]), "Narnia") | i \leftarrow [0..2]]}
	//Dada una competencia finalizada, describe una lista con los primeros tres pa\'ises del ranking. Si el ranking tiene menos de tres elementos, rellena los otros con Narnia.\newline

	\aux{ganadoresMTotales}{M: \ent, j: JJOO}{[Pais]}{\newline
	[nacionalidadPrimerosTres(c)[M] | dia \leftarrow [1.. jornadaActual(j)], c \leftarrow cronograma(j, dia), finalizada(c)]}
	//Describe una lista de todos los pa\'ises que ganaron bronce hasta ahora. Si gan\'o varias veces, aparece varias veces en la lista.\newline

	\aux{crearMedallero}{j: JJOO}{[(Pais, [\ent])]}{\newline
	[(p, [cuenta(p, ganadoresMTotales(0,j)), cuenta(p, ganadoresMTotales(1,j)),\newline cuenta(p, ganadoresMTotales(2,j))]) | p \leftarrow listaPaises(j)]}
	//Para cada pa\'is participante en los juegos, describe una tupla con el nombre del pa\'is y una lista que consiste en tres ints, que son la cantidad de veces que el pa\'is aparece en la lista de ganadores de medallas de oro, de plata y de bronce respectivamente. Como Narnia no participa en los juegos, no aparece en la lista resultante.\newline

	\aux{sacarSinMedallas}{lista : [(Pais, [\ent])]}{[(Pais, [\ent])]}{[x | x \leftarrow lista, sgn(x) \neq [0,0,0]]}
	//Dada una lista de tuplas de pa\'ises y listas de sus respectivas medallas, describe una lista subconjunto la anterior en la que solo aparecen los pa\'ises que ganaron alguna medalla.\newline

	\aux{medalleroOrdenado}{lista : [(Pais, [\ent])]}{Bool}{\newline
	(\forall x \leftarrow [0..|lista|-2]) ((sgd(lista[x])[0] \geq sgd(lista[x+1])[0]) \newline
	\vee ((sgd(lista[x])[0]==sgd(lista[x+1])[0]) \wedge (sgd(lista[x])[1] \geq sgd(lista[x+1])[1]))\newline
	\vee ((sgd(lista[x])[0]==sgd(lista[x+1])[0]) \wedge (sgd(lista[x])[1]==sgd(lista[x+1])[1]) \wedge (sgd(lista[x])[2] \geq sgd(lista[x+1])[2])))}
	//Dada una lista de paises con sus medallas [oro, plata, bronce], medalleroOrdenado vale true si todo elemento de la lista tiene m\'as o igual medallas de oro que el siguiente, o tiene igual medallas de oro pero m\'as o igual platas que el siguiente, o tiene igual medallas de oro y de plata pero m\'as o igual de bronce que el siguiente.\newline
\end{problema}