problema liuSong (j:JJOO, a:Atleta, p:Pais) { 

requiere en(a, atletas(j));

modifica j;
	
asegura año(j)==año(pre(j));
asegura(paraTodo i <- [0..|atletas(pre(j))|-1], atletas(pre(j))[i]!= a)
atletas(pre(j))[i]==atletas(j)[i];

asegura(paraTodo x <-atletas(j), ciaNumber(x)==ciaNumber(a))
(nombre(x)==nombre(a) && sexo(x)==sexo(a) && añoNacimiento(x)==añoNacimiento(a) && nacionalidad(x)==p && deportes(x)==deportes(a) && capacidad(x)==capacidad(a));

asegura cantDias(j)==cantDias(pre(j));
asegura jornadaActual(j)==jornadaActual(pre(j));

asegura(paraTodo d <- [1..cantDias(j)])
|cronograma(d,j)|==|cronograma(d,pre(j))| ^
(paraTodo i <- [0..|cronograma(d,j)|-1] )
categoria(cronograma(d,j)[i])==categoria(cronograma(d,pre(j))[i]) ^
finalizada(cronograma(d,j)[i])==finalizada(cronograma(d,pre(j))[i])

-> Hay que ver que todos los participantes de cada competencia sean iguales menos el modificado.

aux partComp(j: JJOO) : [Atleta] 
= [atl | dia <- [1..cantDias(j)], comp <- cronograma(j, dia), atl <- participantes(comp)];

aux todosIgualesMenosLiuSong(ls : [Atleta], lsOld : [Atleta]) : Bool =
	paraTodo(x <- [0..|ls|-1])
(ls[x]==lsOld[x] || ciaNumber(ls)==ciaNumber(a));

aux todoIgualMenosNacionalidad(ls: [Atleta]) : Bool = 
paraTodo(x <- ls, ciaNumber(x) == ciaNumber(a))
(nombre(x)==nombre(a) && sexo(x)==sexo(a) && añoNacimiento(x)==añoNacimiento(a) && nacionalidad(x)==p && deportes(x)==deportes(a) && capacidad(x)==capacidad(a));

asegura todosIgualesMenosLiuSong(partComp(j), partComp(pre(j)));
asegura todoIgualMenosNacionalidad(partComp(j));

-> Hay que ver que todos los atletas del ranking de cada competencia sean iguales menos el modificado.

aux rankComp(j: JJOO) : [Atleta]
= [atl | dia <- [1..cantDias(j)], comp <- cronograma(j, dia), atl <- ranking(comp), finalizada(comp)];

asegura todosIgualesMenosLiuSong(rankComp(j), rankComp(pre(j)));
asegura todoIgualMenosNacionalidad(rankComp(j));

-> Hay que ver que todos los atletas de lesTocoControlAntidopping de cada competencia sean iguales menos el modificado.

aux doppComp(j: JJOO) : [Atleta] 
= [atl | dia <- [1..cantDias(j)], comp <- cronograma(j, dia), atl <- lesTocoControlAntiDopping(comp), finalizada(comp)];

asegura todosIgualesMenosLiuSong(doppComp(j), doppComp(pre(j)));
asegura todoIgualMenosNacionalidad(doppComp(j));

-> Hay que ver que el valor antidopping para cada atleta no haya cambiado.

	asegura paraTodo(dia <- [1..jornadaActual(j)], comp <- [0..|cronograma(j, dia)-1|], finalizada(cronograma(j, dia)))
			leDioPositivo(cronograma(j, dia)[comp], atl) == leDioPositivo(cronograma(pre(j), dia)[comp], atl);

}