|
@@ -139,9 +139,9 @@
|
|
|
((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 )))}
|
|
((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)
|
|
\asegura{ (\forall comp \leftarrow todasLasCompetencias(j), categoria(comp) == cat)
|
|
|
- (\forall( atl \leftarrow participantes(comp)) nacionalidad (atl) != p}
|
|
|
|
|
|
|
+ (\forall( atl \leftarrow participantes(comp)) nacionalidad (atl) \neq p}
|
|
|
|
|
|
|
|
- \asegura{ mismos (participantes(competenciaFiltrada(j,cat)), [x | x \leftarrow participantes(competenciaFiltrada(pre(j),cat)), nacionalidad(x) != p])}
|
|
|
|
|
|
|
+ \asegura{ mismos (participantes(competenciaFiltrada(j,cat)), [x | x \leftarrow participantes(competenciaFiltrada(pre(j),cat)), nacionalidad(x) \neq p])}
|
|
|
\asegura{ res == |[x | comp \leftarrow todasLasCompetencias(pre(j)), x \leftarrow participantes(comp), (categoria(comp) == cat \wedge 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{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) ] )}
|
|
\aux{competenciaFiltrada}{j:JJOO, c:(deporte,sexo)}{competencia}{cab( [x | x \leftarrow todasLasCompetencias(j), c== categoria(x) ] )}
|
|
@@ -155,7 +155,7 @@
|
|
|
\asegura{(\forall x \leftarrow result, y \leftarrow atletas(j), nacionalidad(y)==p) competenciasEnLasQueParticipo(j, x) >= competenciasEnLasQueParticipo(j, y)}
|
|
\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{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)}
|
|
|
|
|
|
|
+ \aux{noGanoMedallas}{atl: Atleta, comp: Competencia}{Bool}{ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl)}
|
|
|
\end{problema}
|
|
\end{problema}
|
|
|
|
|
|
|
|
\begin{problema}{liuSong}{j: JJOO, a: Atleta, p: Pa\'is}{}
|
|
\begin{problema}{liuSong}{j: JJOO, a: Atleta, p: Pa\'is}{}
|
|
@@ -205,11 +205,11 @@
|
|
|
|
|
|
|
|
//Filtra para que no repita prim() en la lista \newline
|
|
//Filtra para que no repita prim() en la lista \newline
|
|
|
\aux{f2}{ls:[(\ent,\ent)]}{[(\ent,\ent)]}
|
|
\aux{f2}{ls:[(\ent,\ent)]}{[(\ent,\ent)]}
|
|
|
- {[ ls(i) | i \leftarrow [0..|ls|-1], j\leftarrow [i..|ls|-1], prm(ls[i]) != prm(ls[j]) ]}
|
|
|
|
|
|
|
+ {[ ls(i) | i \leftarrow [0..|ls|-1], j\leftarrow [i..|ls|-1], prm(ls[i]) \neq prm(ls[j]) ]}
|
|
|
|
|
|
|
|
//Filtra para que no repita sgd() en la lista \newline
|
|
//Filtra para que no repita sgd() en la lista \newline
|
|
|
\aux{f3}{ls:[(\ent,\ent)]}{[(\ent,\ent)]}
|
|
\aux{f3}{ls:[(\ent,\ent)]}{[(\ent,\ent)]}
|
|
|
- {[ ls(i) | i \leftarrow [0..|ls|-1], j\leftarrow [i..|ls|-1], sgd(ls[i]) != sgd(ls[j]) ]}
|
|
|
|
|
|
|
+ {[ ls(i) | i \leftarrow [0..|ls|-1], j\leftarrow [i..|ls|-1], sgd(ls[i]) \neq sgd(ls[j]) ]}
|
|
|
|
|
|
|
|
//me da la diferencia de (a,b) como b-a \newline
|
|
//me da la diferencia de (a,b) como b-a \newline
|
|
|
\aux{f4}{ls:[(\ent,\ent)]}{[\ent]}
|
|
\aux{f4}{ls:[(\ent,\ent)]}{[\ent]}
|