\subsection{Campo}
% los aux del tipo campo
$igualdadCampo(c,c':Campo):Bool= dimensiones(c)==dimensiones(c') \wedge (\forall i \leftarrow [0..fst(dimensionesCampo(c)),$\\ $j \leftarrow [0..snd(dimensionesCampo(c)) contenido(c,i,j)==contenido(c',i,j)) $ 

parcelasCampo(c:Campo):$[(\ent , \ent)]$= \newline [(x,y) \textbar x $\leftarrow$ [0..prs(dimensiones(c))),y $\leftarrow$ [0..snd(dimensiones(c)))]

\subsection{Drone}
\begin{aux}{miDronePre}{id: \ent, s:Sistema}{Drone}{
	[d | d \leftarrow enjambreDrones(pre(s)), id(d) ==id ][0]
}
	\end{aux}
% los aux del tipo drone
$igualdadDrone(d,d':Drone):Bool= id(d)==id(d') \wedge bateria(d)==bateria(d') \wedge enVuelo(d)==enVuelo(d') \wedge vueloRealizado(d)==vueloRealizado(d') \wedge \newline posicionActual(d)==posicionActual(d') \wedge mismos(productosDisponibles(d),productosDisponibles(d'))$
\newline
\newline
$dronesIgualesSinPosicionNiBat(d,d':Drone):Bool= id(d)==id(d') \wedge enVuelo(d)==enVuelo(d') \wedge vueloRealizado(d)==vueloRealizado(d') \wedge mismos(productosDisponibles(d),productosDisponibles(d'))$
\newline
\newline
mismosDrones(ds,xs:[Drone]):Bool= \textbar ds \textbar == \textbar xs \textbar $ \wedge ( \forall d \leftarrow ds)cantidadAparicionesD(d,ds)==cantidadAperecionesD(d,xs)$
\newline
\newline
$cantidadAparicionesD(d:Drones,ds:[Drones])=$\textbar $[x $\textbar$ x \leftarrow ds, iguadadDrone(x,d)]$\textbar
%│[x │ x\leftarrow ds, iguadadDrone(x,d)]│$
\newline
\newline
escalera1(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \leq prm(vueloRealizado(d)_{i+1}$)\newline if \  $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\  then  $snd(vueloRealizado(d)_{i})+1== snd(vueloRealizado(d)_{i+1}$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
\newline
\newline
escalera2(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \geq prm(vueloRealizado(d)_{i+1}$)\newline if \  $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\  then  $snd(vueloRealizado(d)_{i})-1== snd(vueloRealizado(d)_{i+1})$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
\newline
\newline
escalera3(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \leq prm(vueloRealizado(d)_{i+1}$)\newline if \  $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\  then  $snd(vueloRealizado(d)_{i})-1== snd(vueloRealizado(d)_{i+1})$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
\newline
\newline
escalera4(d:Drone):Bool= ($\forall i \leftarrow$ [0..\textbar vueloRealizado(d)\textbar -1) $prm(vueloRealizado(d)_{i}) \geq prm(vueloRealizado(d)_{i+1}$)\newline if \  $prm(vueloRealizado(d)_{i})== prm(vueloRealizado(d)_{i+1}$\  then  $snd(vueloRealizado(d)_{i})+1== snd(vueloRealizado(d)_{i+1})$\ else $snd(vueloRealizado(d)_{i})== snd(vueloRealizado(d)_{i+1}$
\newline
\newline
parcelasConChoques(ds:[Drones]):[(($\ent,\ent),\ent$)]= \newline [(p,cantidadDronesenMomento(p,i,ds))\textbar d $\leftarrow$ ds, i $\leftarrow$ [0..\textbar vueloRealizado(d) \textbar), p $\leftarrow$ vueloRealizado(d), \\ cantidadDronesEnMomento(p,i,ds) $\geq$ 2]
\newline
\newline
cantidadDronesenMomento($p:(\ent, \ent),i:\ent,ds:[Drones]): \ent$ = \\ \textbar [p \textbar d $\leftarrow$ ds, $vueloRecorrido(d)_{i} $== p] \textbar
\newline
\newline
quitarRepetidos(xs:[($\ent,\ent),\ent$)])=[$x_{i}$ \textbar i $\leftarrow$ [0.. \textbar xs \textbar), ($\forall$ j $\leftarrow$ [0.. \textbar xs \textbar), i $\leq$ j)$x_{i}$ $\lneq$ $x_{j}$]
\newline
\newline
estaOrdenadoPorLaSugundaCoordenada(xs:[($\ent,\ent),\ent$)]):Bool = ($\forall$ x $\leftarrow$ xs)($\forall$ i,j $\leftarrow$ [0.. \textbar xs \textbar), i$\leq$j)$snd(x_{i})$ $\leq$ $snd(x_{j})$ $\vee$ $snd(x_{i})$ $\geq$ $snd(x_{j})$

\subsection{Sistema}

$parcelasAdyacentes(s:Sistema,i: \ent , j: \ent)): [(\ent , \ent)]$ = [p \textbar p $\leftarrow$ [(i+1,j), (i-1,j), (i,j+1),(i,j-1)], \newline enRango(dimensiones(campo(s)),prs(p),snd(p))]

parcelaAdyacenteConPlaga(s:Sistema, i,j: $\ent$): Bool = $(\forall p \leftarrow parcelasAdyacentes(s,i,j), \newline contenido(campo(s),prs(p),snd(p))==Cultivo)$ estadoDelCultivo(s,prs(p),snd(p))==ConMaleza

algunAdyacenteConPlaga(s:Sistema,i,j:$\ent$):Bool = $(\exists p \leftarrow parcelasAdyacentes(s,i,j),\newline contenido(campo(s),prs(p),snd(p))==Cultivo)$ estadoDelCultivo(s,prs(p),snd(p))==ConMaleza

soloUnDrone(s:Sistema,p:$(\ent , \ent)$):Bool= \textbar [d \textbar d $\leftarrow$ enjambreDrones(s), posicionActual(d) == p ]\textbar == 1 

estaAdyacenteAlGranero(s:Sistema,d:Drone):Bool = \newline ($\exists$ (i,j) $\leftarrow$ parcelasAdyacentes(s,prs(posicionActual(d)),snd(posicionAlcual(s))))
enRango(dimensiones(campo(s)),i,j) \newline $\wedge$ contenido(campo(s),i,j) $\neq$ Granero

parcelaAdyacenteAlGraneroLibre(s:Sistema):Bool= \newline
($\exists$ (i,j),(n,m) $\leftarrow$ parcelasCampo(campo(s)))contenido(campo(s),i,j) $\neq$ Granero $\wedge$ contenido(campo(s),n,m)==Granero $\wedge$ (n,m) $\in$ parcelasAdyacentes(i,j)