\subsection{Juego}
\nuevoTAD{Juego}
\genero{juego}
\begin{seccion}[generadores]
    \funcion{empezarJuego}{mapa}{juego}
    \funcion{agregarJugador}{Juego j \times Jugador j'}{Juego}
	\restriccion{j' \notin jugadores(j)}

    \funcion{agregarPoke}{Poke p \times coord c \times juego j}{juego}
	\restriccion{c \in coords(j) \wedge ( \forall p' \in pokes(j))(distancia?(c, pokeCoord(p')) > 5)}

    \funcion{MoverJugador}{Jugador j \times Juego j' \times coord c}{juego}
	\restriccion{c \in coords(j') \wedge j \in jugadores(j') \wedge  ¿¿ cviene del jugador ??}

    \funcion{capturar}{Jugador j \times Juego j' \times Poke p}{juego}
	\restriccion{ j \in jugadores(j') \wedge p \in pokesLibres(j')}

    \funcion{conectar}{Jugador j \times Juego j' }{juego}
	\restriccion { j \in jugadores(j') \wedge \not conectado?(j,j') \wedge coordenadas??}

    \funcion{desconectar}{Jugador j \times Juego j' }{juego}
	\restriccion { j \in jugadores(j') \wedge conectado?(j,j')}

    \funcion{expulsar}{Jugador j \times Juego j'}{juego}
	\restriccion { j \in jugadores(j') \wedge infraccionesDeJugador(j',j) > 5}
\end{seccion}
\begin{seccion}[observadores]
    \funcion{movimientosGlobales}{juego}{sec(jugador \times pos)}
    \funcion{jugadores}{juego}{conj(jugador)}
    \funcion{eliminado?}{juego g \times jugador j}{bool}
	\restriccion{j \in jugadores(g) }

    \funcion{conectado?}{juego g \times jugador j}{bool}
	\restriccion{j \in jugadores(g)}

    \funcion{PokeLibres}{juego}{dicc(coord \times pokemon)}
    \funcion{PokeCapturados}{juego}{dicc(jugador \times multiconj(pokemon))}
    \funcion{mapa}{juego}{mapa}
    
\end{seccion}
\begin{seccion}[otras operaciones]
    \funcion{PokeRareza}{Juego j \times Pokemon p}{nat}
	\restriccion{p \in poketotal(j)}

	\funcion{infraccionesDeJugador}{Juego j \times jugador j'}{nat}
	\restriccion{j' \in jugadores(j)}

	\funcion{PokeTotales}{Juego j}{multiconj(Pokemons)}

\end{seccion}
\begin{seccion}[axiomas]
    \doublespacing
    \funcion{alal}{}{nat}
    \funcion{alal}{}{nat}
    \funcion{alal}{}{nat}
    \singlespacing
\end{seccion}