fertilizar por fila

espec/sistema.tex

@@ -1,6 +1,6 @@
 \begin{problema}{crearS}{c: Campo, ds: [Drone]}{Sistema}
 	\asegura{igualdadCamapo(campo(res),c)}
-	\asegura{(\forall d \leftarrow ds)(\exists d' \leftarrow enjambreDrones(s))id(d)==id(d') \wedge bateria(d')==100 \wedge \neg enVuelo(d') \wedge \newline enRango(dimesiones(campo(res)), prs(posiconActual(d')),snd(posiconActual(d'))) \wedge \newline contenido(campo(res), prs(posiconActual(d')),snd(posiconActual(d')))==Granero}
+	\asegura{(\forall d \leftarrow ds)(\exists d' \leftarrow enjambreDrones(s))id(d)==id(d') \wedge bateria(d')==100 \wedge \neg enVuelo(d') \wedge \newline enRango(dimesiones(campo(res)), prs(posicionActual(d')),snd(posicionActual(d'))) \wedge \newline contenido(campo(res), prs(posicionActual(d')),snd(posicionActual(d')))==Granero}
 \end{problema}
 
 \begin{problema}{campoS}{s: Sistema}{Campo}
@@ -76,14 +76,15 @@
 \end{problema}
 
 \begin{problema}{fertilizarPorFilas}{s: Sistema}{}
-	\modifica s
-	\asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), !puedeMoverOeste(d)) NOCAMBIA }
-	\asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), puedeMoverOeste(d)) \newline
-		\IfThenElse{bateria(d) == 0}{NOCAMBIA}{
-			if { !tieneFertilizante(d)} \newline
-				{NOCAMBIA}\newline
-		fi
+	\modifica s \asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), !puedeMoverOeste(d)) igualdadDrone(d,pre(d)) }
+	\asegura{ (\forall(d) \leftarrow enjambreDrones(pre(s)), puedeMoverOeste(d))
+		\newline dronesIgualesSinPosicion(d,pre(d)) \wedge \newline posicionActual(d)==(pri(posicionActual(pre(d)-1)),sgd(posicionActual(pre(d)))) 
+	}
+	\begin{aux}{puedeMoverOeste}{d: Drone, s:Sistema}{\bool}{
+		\newline
+		\IfThenElse{ bateria(d) == 0 \vee noTieneFertilizante(d) \vee \newline contenido(campo(pre(s)),pri(posicionActual(d)),sgd(posicionActual(d))) \neq Cultivo \vee \newline pri(posicionActual(d)) == 0 }{\newline False \newline }{\newline True}
 	}
+	\end{aux}
 \end{problema}
 
 \begin{problema}{volarYSensarS}{s: Sistema, d: Drone}{}