paso a latex

template/templateTP.tex

@@ -116,29 +116,64 @@
 	\asegura{mismos(res,noParticiparon(j))}
 	\aux{noParticiparon}{j: JJOO}{[Atleta]}{[x | x \leftarrow atletas(j), \neg en(x, participaronConRepes(j))]}
 	\aux{participaronConRepes}{j: JJOO}{[Atleta]}{[atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow atletas(j), en(atl, participantes(comp))]}
-
 \end{problema}
 
 \begin{problema}{medallero}{j: JJOO}{[(Pais, [\ent])]}
 \end{problema}
 
 \begin{problema}{boicotPorDisciplina}{j: JJOO, cat: (Deporte, Sexo), p: Pais}{\ent}
+	\requiere{existe (c \leftarrow 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{ano(j) == ano(pre(j))}
+	\asegura{mismos(atletas(j), atletas(pre(j)))}
+	\asegura{cantDias(j) == cantDias(pre(j))}
+	\asegura{jornadaActual(j) == jornadaActual(pre(j))}
+	\asegura{(\forall dia \leftarrow [1..cantDias (j)] ) \newline
+		|cronograma(j,dia) | == |cronograma(pre(j), dia)|}
+
+	\asegura{ (\forall dia \leftarrow [1..cantDias(j)]) \newline
+		(\forall( x \leftarrow [1..(long(cronograma(j,dia))-1)])) \newline
+		((cronograma((j,dia)[x] == cronograma (pre(j),dia) [x]) \vee ( categoria(cronograma(j,dia)[x]) == (categoria(cronograma(pre(j),dia)[x])) \wedge (categoria(cronograma(j,dia)[x]) == cat )))}
+
+	\asegura{ (\forall comp \leftarrow todasLasCompetencias(j), categoria(comp) == cat)
+		(\forall( atl \leftarrow participantes(comp)) nacionalidad (atl) != p}
+
+	\asegura{ mismos (participantes(competenciaFiltrada(j,cat)), [x | x \leftarrow participantes(competenciaFiltrada(pre(j),cat)), nacionalidad(x) != p])}
+	\asegura{ res == |[x | comp \leftarrow todasLasCompetencias(pre(j)), x \leftarrow participantes(comp), (categoria(comp) == cat \wedge nacionalidad(x) == p)]|}
+	\aux{todasLasCompetencias}{j:JJOO}{[competencia]}{[x | y \leftarrow [1..cantDIas(j)], x \leftarrow cronogramas(j,y) ] }
+	\aux{competenciaFiltrada}{j:JJOO, c:(deporte,sexo)}{competencia}{cab( [x | x \leftarrow todasLasCompetencias(j), c== categoria(x) ] )}
 \end{problema}
 
 
 
 \begin{problema}{losMasFracasados}{j: JJOO, p: Pais}{[Atleta]}
-	%\\asegura{(\forall x \rightarrow [ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl) | atl \rightarrow res, comp \rightarrow todasLasCompetencias(j), finalizada(comp)]) x}
-	%\\asegura{(\forAll x \rightarrow [ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl) | atl \rightarrow res, comp \rightarrow todasLasCompetencias(j), finalizada(comp)]) x}
-	%\\asegura{(\forAll x \rightarrow res) nacionalidad(x) == p}
-	%\\asegura{(\forAll i \rightarrow [0..|res|-2]) competenciasEnLasQueParticipo(j, res[i]) \geq competenciasEnLasQueParticipo(j, res[i+1])}
-	%\\aux{competenciasEnLasQueParticipo}{j: JJOO, a: Atleta}{\ent}{\longitud{[z | z \leftarrow todasLasCompetencias(j), en(a, participantes(z))]}}
+	\asegura{noGanaronMedallas: (\forall x \leftarrow [noGanoMedallas(atl, comp) | atl \leftarrow result, comp \leftarrow todasLasCompetencias(j), finalizada(comp)]) x;}
+	\asegura{todosDelPais: (\forall x \leftarrow result) nacionalidad(x) == p;}
+	\asegura{(\forall x \leftarrow result, y \leftarrow atletas(j), nacionalidad(y)==p) competenciasEnLasQueParticipo(j, x) >= competenciasEnLasQueParticipo(j, y)}
+
+	\aux{competenciasEnLasQueParticipo}{j: JJOO, a:Atleta}{\ent}{long([z | z\leftarrow todasLasCompetencias(j), en(a, participantes(z))])}
+	\aux{noGanoMedallas}{atl: Atleta, comp: Competencia}{Bool}{ciaNumber(ranking(comp)[0]) != ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) != ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) != ciaNumber(atl)}
 \end{problema}
 
 \begin{problema}{liuSong}{j: JJOO, a: Atleta, p: Pa\'is}{}
+
 \end{problema}
 
 \begin{problema}{stevenBradbury}{j: JJOO}{Atleta}
+	//Requiere que al menos una competencia ya haya finalizado (y, por lo tanto, se haya entregado un oro)
+	\requiere{algunOro: long([comp | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0])>0}
+
+	//Asegura que result haya ganado un oro
+	\asegura{ganoOro: existe(f \leftarrow [ranking(comp)[0] | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0]) ciaNumber(result)==ciaNumber(f)}
+
+	//Asegura que entre todos los ganadores de oro, el result es el que tiene la menor habilidad en alguna de las medallas que gano.	
+	\asegura{esElPeor: existe(dep \leftarrow deportesEnLosQueGano(j, result)) paraTodo(f \leftarrow [ranking(comp)[0] | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0]) capacidad(result, dep) <= capacidad(f, prm(categoria(comp))}
+
+	\aux{deportesEnLosQueGanoOro}{j: JJOO, a: Atleta}{[Deportes]}
+		{[prm(categoria(comp)) | comp \leftarrow todasLasCompetencias(j), finalizada(comp)\wedge|ranking(comp)|>0 \wedge ciaNumber(ranking(comp)[0])==ciaNumber(a)]}
 \end{problema}
 
 \begin{problema}{uyOrdenadoAs\'iHayUnPatr\'on}{j: JJOO}{\bool}
@@ -146,6 +181,27 @@
 
 
 \begin{problema}{sequ\'iaOl\'impica}{j: JJOO}{[Pa\'is]}
+
+	\asegura{ (\forall p \leftarrow result) sequiaPais(p) == maximaSequia(j)}
+	\asegura{ (\forall p \leftarrow listaPaisesConSequia(j), sequiaPais(p)==maximaSequia(j)) p \in result }
+
+	\aux{sequiaPais}{p:pais}{\ent}{jornadaActual(j)-cuantosDiasGano(p)}
+
+	\aux{cuantosDiasGano}{p:pais}{\ent} 
+		{|[ 1 | x \leftarrow [0..jornadaActual(j)-1], ganoEnElDia(x,p) ]|}
+
+	\aux{ganoEnElDia}{dia,pais}{Bool}
+		{|[ 1 | c \leftarrow cronograma(j, dia), en(pais, paisesQueGanaronCompetencia(c)) ]|>0}
+
+	\aux{listaPaisesConSequia}{j: JJOO}{[(Pais, Int)]}
+		{[(p, sequiaPais(p)) | p \leftarrow listaPaises(j)]}
+
+	\aux{maximaSequia}{j: JJOO}{\ent}
+		{maximoLista([ sequiaPais(p) | p \leftarrow listaPaises(j)])}
+
+	\aux{paisesQueGanaronCompetencia}{c:Competencia}{[paises]}
+		{\newline [ pais(ranking(c)[a]) | a  \leftarrow [0.. |ranking(c) |-1 ], a <= 2 ]}
+
 \end{problema}
 
 \begin{problema}{transcurrirDia}{j: JJOO}{}