Arreglado liu song

template/templateTP.aux

@@ -11,4 +11,4 @@
 \@writefile{toc}{\contentsline {section}{\numberline {2}Atleta}{1}}
 \@writefile{toc}{\contentsline {section}{\numberline {3}Competencia}{1}}
 \@writefile{toc}{\contentsline {section}{\numberline {4}JJOO}{2}}
-\@writefile{toc}{\contentsline {section}{\numberline {5}Auxiliares}{5}}
+\@writefile{toc}{\contentsline {section}{\numberline {5}Auxiliares}{6}}

template/templateTP.log

@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.14159265-2.6-1.40.15 (TeX Live 2015/dev/Debian) (preloaded format=pdflatex 2016.9.3)  4 SEP 2016 19:41
+This is pdfTeX, Version 3.14159265-2.6-1.40.15 (TeX Live 2015/dev/Debian) (preloaded format=pdflatex 2016.9.3)  4 SEP 2016 19:50
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -349,82 +349,19 @@ File: umsb.fd 2013/01/14 v3.01 AMS symbols B
 
 {/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]) (./tipos/jjoo.tex [2]) [3
 ]
-Overfull \hbox (11.40186pt too wide) in paragraph at lines 192--192
- \OML/cmm/m/it/10 anoNacimiento\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 x\OT1/cmr/m/n/
-10 ) == \OML/cmm/m/it/10 anoNacimiento\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 a\OT1/c
-mr/m/n/10 ) \OMS/cmsy/m/n/10 ^ \OML/cmm/m/it/10 nacionalidad\OT1/cmr/m/n/10 (\O
-ML/cmm/m/it/10 x\OT1/cmr/m/n/10 ) == \OML/cmm/m/it/10 p \OMS/cmsy/m/n/10 ^ \OML
-/cmm/m/it/10 deportes\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 x\OT1/cmr/m/n/10 ) == \O
-ML/cmm/m/it/10 deportes\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 a\OT1/cmr/m/n/10 ) \OM
-S/cmsy/m/n/10 ^ \OML/cmm/m/it/10 capacidad\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 x\O
-T1/cmr/m/n/10 ) ==
+Overfull \hbox (35.32408pt too wide) in paragraph at lines 211--211
+ \OT1/cmr/m/n/10 [\OML/cmm/m/it/10 atl\OMS/cmsy/m/n/10 j\OML/cmm/m/it/10 dia \O
+MS/cmsy/m/n/10   \OT1/cmr/m/n/10 [1\OML/cmm/m/it/10 ::cantDias\OT1/cmr/m/n/10 (
+\OML/cmm/m/it/10 j\OT1/cmr/m/n/10 )]\OML/cmm/m/it/10 ; comp \OMS/cmsy/m/n/10   
+\OML/cmm/m/it/10 cronograma\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j; dia\OT1/cmr/m/n
+/10 )\OML/cmm/m/it/10 ; atl \OMS/cmsy/m/n/10   \OML/cmm/m/it/10 lesTocoControlA
+ntiDopping\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 comp\OT1/cmr/m/n/10 )\OML/cmm/m/it/
+10 ; finalizada\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 comp\OT1/cmr/m/n/10 )]$\OT1/cm
+r/bx/n/10 ; 
  []
 
 
-Overfull \hbox (195.24945pt too wide) in paragraph at lines 219--219
- []\OT1/cmtt/m/n/10 asegura $\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 (\OML/cmm/m/it/1
-0 dia \OMS/cmsy/m/n/10   \OT1/cmr/m/n/10 [1\OML/cmm/m/it/10 ::jornadaActual\OT1
-/cmr/m/n/10 (\OML/cmm/m/it/10 j\OT1/cmr/m/n/10 )]\OML/cmm/m/it/10 ; comp \OMS/c
-msy/m/n/10   \OT1/cmr/m/n/10 [0\OML/cmm/m/it/10 ::\OMS/cmsy/m/n/10 j\OML/cmm/m/
-it/10 cronograma\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j; dia\OT1/cmr/m/n/10 ) \OMS/
-cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 ]\OML/cmm/m/
-it/10 ; finalizada\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 cronograma\OT1/cmr/m/n/10 (
-\OML/cmm/m/it/10 j; dia\OT1/cmr/m/n/10 )))\OML/cmm/m/it/10 leDioPositivo\OT1/cm
-r/m/n/10 (\OML/cmm/m/it/10 cronograma\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j; dia\O
-T1/cmr/m/n/10 )[\OML/cmm/m/it/10 comp\OT1/cmr/m/n/10 ]\OML/cmm/m/it/10 ; atl\OT
-1/cmr/m/n/10 ) ==
- []
-
-
-Overfull \hbox (100.3108pt too wide) in paragraph at lines 222--222
- []\OT1/cmtt/m/n/10 aux rankComp \OT1/cmr/m/n/10 (j: JJOO) : [Atle-ta] = $= [\O
-ML/cmm/m/it/10 atl\OMS/cmsy/m/n/10 j\OML/cmm/m/it/10 dia \OMS/cmsy/m/n/10   \OT
-1/cmr/m/n/10 [1\OML/cmm/m/it/10 ::cantDias\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j\O
-T1/cmr/m/n/10 )]\OML/cmm/m/it/10 ; comp \OMS/cmsy/m/n/10   \OML/cmm/m/it/10 cro
-nograma\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j; dia\OT1/cmr/m/n/10 )\OML/cmm/m/it/1
-0 ; atl \OMS/cmsy/m/n/10   \OML/cmm/m/it/10 ranking\OT1/cmr/m/n/10 (\OML/cmm/m/
-it/10 comp\OT1/cmr/m/n/10 )\OML/cmm/m/it/10 ; finalizada\OT1/cmr/m/n/10 (\OML/c
-mm/m/it/10 comp\OT1/cmr/m/n/10 )]$\OT1/cmr/bx/n/10 ; 
- []
-
-
-Overfull \hbox (191.657pt too wide) in paragraph at lines 225--225
- []\OT1/cmtt/m/n/10 aux doppComp \OT1/cmr/m/n/10 (j: JJOO) : [Atle-ta] = $= [\O
-ML/cmm/m/it/10 atl\OMS/cmsy/m/n/10 j\OML/cmm/m/it/10 dia \OMS/cmsy/m/n/10   \OT
-1/cmr/m/n/10 [1\OML/cmm/m/it/10 ::cantDias\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j\O
-T1/cmr/m/n/10 )]\OML/cmm/m/it/10 ; comp \OMS/cmsy/m/n/10   \OML/cmm/m/it/10 cro
-nograma\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j; dia\OT1/cmr/m/n/10 )\OML/cmm/m/it/1
-0 ; atl \OMS/cmsy/m/n/10   \OML/cmm/m/it/10 lesTocoControlAntiDopping\OT1/cmr/m
-/n/10 (\OML/cmm/m/it/10 comp\OT1/cmr/m/n/10 )\OML/cmm/m/it/10 ; finalizada\OT1/
-cmr/m/n/10 (\OML/cmm/m/it/10 comp\OT1/cmr/m/n/10 )]$\OT1/cmr/bx/n/10 ; 
- []
-
-
-Overfull \hbox (29.38405pt too wide) in paragraph at lines 228--228
- []\OT1/cmtt/m/n/10 aux partComp \OT1/cmr/m/n/10 (j: JJOO) : [Atle-ta] = $[\OML
-/cmm/m/it/10 atl\OMS/cmsy/m/n/10 j\OML/cmm/m/it/10 dia \OMS/cmsy/m/n/10   \OT1/
-cmr/m/n/10 [1\OML/cmm/m/it/10 ::cantDias\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j\OT1
-/cmr/m/n/10 )]\OML/cmm/m/it/10 ; comp \OMS/cmsy/m/n/10   \OML/cmm/m/it/10 crono
-grama\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j; dia\OT1/cmr/m/n/10 )\OML/cmm/m/it/10 
-; atl \OMS/cmsy/m/n/10   \OML/cmm/m/it/10 participantes\OT1/cmr/m/n/10 (\OML/cm
-m/m/it/10 comp\OT1/cmr/m/n/10 )]$\OT1/cmr/bx/n/10 ; 
- []
-
-
-Overfull \hbox (11.50313pt too wide) in paragraph at lines 236--236
- \OT1/cmr/m/n/10 (\OML/cmm/m/it/10 nombre\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 x\OT
-1/cmr/m/n/10 ) == \OML/cmm/m/it/10 nombre\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 a\OT
-1/cmr/m/n/10 ) \OMS/cmsy/m/n/10 ^ \OML/cmm/m/it/10 sexo\OT1/cmr/m/n/10 (\OML/cm
-m/m/it/10 x\OT1/cmr/m/n/10 ) == \OML/cmm/m/it/10 sexo\OT1/cmr/m/n/10 (\OML/cmm/
-m/it/10 a\OT1/cmr/m/n/10 ) \OMS/cmsy/m/n/10 ^ \OML/cmm/m/it/10 anoNacimiento\OT
-1/cmr/m/n/10 (\OML/cmm/m/it/10 x\OT1/cmr/m/n/10 ) == \OML/cmm/m/it/10 anoNacimi
-ento\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 a\OT1/cmr/m/n/10 ) \OMS/cmsy/m/n/10 ^ \OM
-L/cmm/m/it/10 nacionalidad\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 x\OT1/cmr/m/n/10 ) 
-==
- []
-
-
-Overfull \hbox (4.11461pt too wide) in paragraph at lines 247--248
+Overfull \hbox (4.11461pt too wide) in paragraph at lines 229--230
  \OT1/cmtt/m/n/10 asegura $\OML/cmm/m/it/10 esElPeor \OT1/cmr/m/n/10 : \OML/cmm
 /m/it/10 existe\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 dep \OMS/cmsy/m/n/10   \OML/cm
 m/m/it/10 deportesEnLosQueGano\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j; result\OT1/c
@@ -435,7 +372,7 @@ msy/m/n/10
  []
 
 
-Overfull \hbox (92.09532pt too wide) in paragraph at lines 247--248
+Overfull \hbox (92.09532pt too wide) in paragraph at lines 229--230
  \OML/cmm/m/it/10 todasLasCompetencias\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 j\OT1/c
 mr/m/n/10 )\OML/cmm/m/it/10 ; finalizada\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 comp\
 OT1/cmr/m/n/10 ) \OMS/cmsy/m/n/10 ^ j\OML/cmm/m/it/10 ranking\OT1/cmr/m/n/10 (\
@@ -447,8 +384,8 @@ apacidad\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f; prm\OT1/cmr/m/n/10 (\OML/cmm/m/it/
 x/n/10 ; 
  []
 
-
-Overfull \hbox (136.8026pt too wide) in paragraph at lines 251--251
+[4]
+Overfull \hbox (136.8026pt too wide) in paragraph at lines 233--233
  []\OT1/cmtt/m/n/10 aux deportesEnLosQueGanoOro \OT1/cmr/m/n/10 (j: JJOO, a: At
 le-ta) : [De-por-tes] = $[\OML/cmm/m/it/10 prm\OT1/cmr/m/n/10 (\OML/cmm/m/it/10
  categoria\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 comp\OT1/cmr/m/n/10 ))\OMS/cmsy/m/n
@@ -458,7 +395,7 @@ lizada\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 comp\OT1/cmr/m/n/10 ) \OMS/cmsy/m/n/10
 ^
  []
 
-[4] (./auxiliaresTipos.tex [5]) [6] (./templateTP.aux
+(./auxiliaresTipos.tex [5]) [6] (./templateTP.aux
 LaTeX Info: Redefining \. on input line 6.
 LaTeX Info: Redefining \% on input line 6.
 ) ) 
@@ -483,7 +420,7 @@ s/cm/cmss10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
 msy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.p
 fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></u
 sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb>
-Output written on templateTP.pdf (6 pages, 164540 bytes).
+Output written on templateTP.pdf (6 pages, 164527 bytes).
 PDF statistics:
  79 PDF objects out of 1000 (max. 8388607)
  56 compressed objects within 1 object stream

template/templateTP.tex

@@ -182,59 +182,41 @@
 \end{problema}
 
 \begin{problema}{liuSong}{j: JJOO, a: Atleta, p: Pa\'is}{}
+	%Fixed by martu
 	\requiere{a \in atletas(j)}
 	\modifica{j}
 	\asegura{ano(j)==ano(pre(j))}
 	\asegura{(\forall i  \leftarrow  [0..|atletas(pre(j))|-1], atletas(pre(j))_i!= a)
 		atletas(pre(j))_i==atletas(j)_i}
-
-	\asegura{(\forall x  \leftarrow atletas(j), ciaNumber(x)==ciaNumber(a))
-	(nombre(x)==nombre(a) \wedge sexo(x)==sexo(a) \wedge anoNacimiento(x)==anoNacimiento(a) \wedge nacionalidad(x)==p \wedge deportes(x)==deportes(a) \wedge capacidad(x)==capacidad(a))}
-
+	\asegura{(\forall x  \leftarrow atletas(j), ciaNumber(x)==ciaNumber(a))\newline
+		(nombre(x)==nombre(a) \wedge sexo(x)==sexo(a) \wedge a\tilde{n}oNacimiento(x)==a\tilde{n}oNacimiento(a)\newline
+		\wedge nacionalidad(x)==p \wedge deportes(x)==deportes(a) \wedge capacidad(x)==capacidad(a))}
 	\asegura{cantDias(j)==cantDias(pre(j))}
 	\asegura{jornadaActual(j)==jornadaActual(pre(j))}
-
-	\asegura{(\forall d  \leftarrow  [1..cantDias(j)])\newline
-	|cronograma(d,j)|==|cronograma(d,pre(j))| \wedge \newline
-	(\forall i  \leftarrow  [0..|cronograma(d,j)|-1] )\newline
-	categoria(cronograma(d,j)[i])==categoria(cronograma(d,pre(j))[i]) \wedge
-		finalizada(cronograma(d,j)[i])==finalizada(cronograma(d,pre(j))[i])}
-
+	\asegura{(\forall d  \leftarrow  [1..cantDias(j)]) |cronograma(d,j)|==|cronograma(d,pre(j))|\newline
+		\wedge (\forall i  \leftarrow  [0..|cronograma(d,j)|-1] )\newline
+		categoria(cronograma(d,j)[i])==categoria(cronograma(d,pre(j))[i])\newline
+		\wedge finalizada(cronograma(d,j)[i])==finalizada(cronograma(d,pre(j))[i])}
 	\asegura{todosIgualesMenosLiuSong(partComp(j), $part$Comp(pre(j)))}
 	\asegura{todoIgualMenosNacionalidad(partComp(j))}
-
-	%-> Hay que ver que todos los atletas del ranking de cada competencia sean iguales menos el modificado.
-
 	\asegura{todosIgualesMenosLiuSong(rankComp(j), $rank$Comp(pre(j)))}
 	\asegura{todoIgualMenosNacionalidad(rankComp(j))}
-
-	%-> Hay que ver que todos los atletas de lesTocoControlAntidopping de cada competencia sean iguales menos el modificado.
-
 	\asegura{todosIgualesMenosLiuSong(doppComp(j), $dopp$Comp(pre(j)))}
 	\asegura{todoIgualMenosNacionalidad(doppComp(j))}
-
-	%-> Hay que ver que el valor antidopping para cada atleta no haya cambiado.
-
-	\asegura{\forall(dia  \leftarrow  [1..jornadaActual(j)], comp  \leftarrow  [0..|cronograma(j, dia)-1|], finalizada(cronograma(j, dia)))
+	\asegura{\forall(dia  \leftarrow  [1..jornadaActual(j)], comp  \leftarrow  [0..|cronograma(j, dia)-1|], finalizada(cronograma(j, dia)))\newline
 		leDioPositivo(cronograma(j, dia)[comp], atl) == leDioPositivo(cronograma(pre(j), dia)[comp], atl)}
-
-	\aux{rankComp}{j: JJOO}{[Atleta]}{
-	= [atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  ranking(comp), finalizada(comp)]}
-	%-> Hay que ver que todos los participantes de cada competencia sean iguales menos el modificado.
-	\aux{doppComp}{j: JJOO}{[Atleta]}{
-	= [atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  lesTocoControlAntiDopping(comp), finalizada(comp)]}
-
-	\aux{partComp}{j: JJOO}{[Atleta]}{
-	[atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  participantes(comp)]}
-
-	\aux{todosIgualesMenosLiuSong}{ls : [Atleta], lsOld : [Atleta]}{Bool}{
-		\forall(x  \leftarrow  [0..|ls|-1])\newline
-	(ls[x]==lsOld[x]  \vee  ciaNumber(ls)==ciaNumber(a))}
-
-	\aux{todoIgualMenosNacionalidad}{ls: [Atleta]}{Bool}{
-	\forall(x  \leftarrow  ls, ciaNumber(x) == ciaNumber(a))\newline
-	(nombre(x)==nombre(a) \wedge sexo(x)==sexo(a) \wedge anoNacimiento(x)==anoNacimiento(a) \wedge nacionalidad(x)==p \wedge deportes(x)==deportes(a) \wedge capacidad(x)==capacidad(a))}
-
+	\aux{rankComp}{j: JJOO}{[Atleta]}{\newline
+		[atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  ranking(comp), finalizada(comp)]}
+	\aux{doppComp}{j: JJOO}{[Atleta]}{\newline
+		[atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  lesTocoControlAntiDopping(comp), finalizada(comp)]}
+	\aux{partComp}{j: JJOO}{[Atleta]}{\newline
+		[atl | dia  \leftarrow  [1..cantDias(j)], comp  \leftarrow  cronograma(j, dia), atl  \leftarrow  participantes(comp)]}
+	\aux{todosIgualesMenosLiuSong}{ls : [Atleta], lsOld : [Atleta]}{Bool}{\newline
+		\forall(x  \leftarrow  [0..|ls|-1]) (ls[x]==lsOld[x]  \vee  ciaNumber(ls)==ciaNumber(a))}
+	\aux{todoIgualMenosNacionalidad}{ls: [Atleta]}{Bool}{\newline
+		\forall(x  \leftarrow  ls, ciaNumber(x) == ciaNumber(a)) (nombre(x)==nombre(a) \wedge sexo(x)==sexo(a)\newline
+		\wedge anoNacimiento(x)==anoNacimiento(a) \wedge nacionalidad(x)==p \wedge deportes(x)==deportes(a)\newline
+		\wedge capacidad(x)==capacidad(a))}
 \end{problema}
 
 \begin{problema}{stevenBradbury}{j: JJOO}{Atleta}