ej2+3

template/templateTP.tex

@@ -41,7 +41,7 @@
 	\requiere{c \geq 0 \wedge c \leq 100}
 	\requiere{\neg (a(d,deporte(a)))}
 	\modifica{a}
-	\asegura{mismos(deportes(a),deportes(pre(a))}
+	\asegura{mismos(deportes(a),deportes(pre(a)))}
 	\asegura{ordenada(deportes(a))}
 	\asegura{capacidad(a,d)==c}
 \end{problema}
@@ -53,9 +53,26 @@
 \input{tipos/competencia.tex}
 
 \begin{problema}{finalizarCompetencia}{c: Competencia, posiciones: [Atleta], control: [(Atleta, \bool)]}{}
+	%definir mismos en Auxiliares
+	\requiere{contenida(posiciones,participantes(c))}
+	\requiere{sinRepetidos(posiciones)}
+	\requiere{(\forall x \leftarrow control) prm(x) \in participantes(c)}
+	\modifica{c}
+	\asegura{finalizada(c)}
+	\asegura{ranking(c)==posiciones}
+	\asegura{participantes(c)==participantes(pre(c))}
+	\asegura{LesTocoControlAntiDOpping(c)== [prm(x) | x \leftarrow control]}
+	\asegura{(\forall x \leftarrow control) leDioPositivo(prm(x))==sgn(x)}
+	\asegura{categoria(c)==categoria(pre(c))}
 \end{problema}
 
 \begin{problema}{linfordChristie}{c: Competencia, a: Atleta}{}
+	\requiere{\neg finalizada(c)}
+	\requiere{a \in participantes(c)}
+	\modifica{c}
+	\asegura{mismos(participantes(pre(c)), a:participantes(c))}
+	\asegura{categoria(c)==categoria(pre(c))}
+	\asegura{\neg finalizada(c)}
 \end{problema}
 
 \begin{problema}{gananLosMasCapaces}{c: Competencia}{\bool}