\documentclass[a4paper]{article}

\usepackage[spanish]{babel}
\usepackage[latin1]{inputenc}

\usepackage{framed}
\input{Algo1Macros}

\newcommand{\comen}[2]{%
\begin{framed}	
\noindent \textsf{#1:} #2
\end{framed}
}



\begin{document}

\materia{Algoritmos y Estructura de Datos I}
\cuatrimestre{2}
\anio{2016}

%\fecha{26 de agosto de 2016}

\nombre{\LARGE TPE OJOTA (Organizaci\'on de Juegos Ol\'impicos Tp de Algoritmos 1) v1.0}

\titulotp


\section{Tipos}

\input{tipos/tipos.tex}

\section{Atleta}
\input{tipos/atleta.tex}

\begin{problema}{especialidad}{a: Atleta}{Deporte}
	\asegura{res \in deportes(a)}
	\asegura{capacidad(a,res)==maximoLista(listarCapacidades(a))}
	\aux{listarCapacidades}{a:Atleta}{[\ent]}{[capacidad(a,x) | x \leftarrow deportes(a) ]}
	\aux{maximoLista}{ls:[\ent]}{\ent}{[x|x\leftarrow ls, (\forall y \leftarrow ls) x \geq y][0]}
\end{problema}

\begin{problema}{entrenarNuevoDeporte}{a: Atleta, d: Deporte, c: \ent}{}
	\requiere{c \geq 0 \wedge c \leq 100}
	\requiere{d \notin deportes(a)}
	\modifica{a}
	\asegura{nombre(a)==nombre(pre(a))}
	\asegura{sexo(a) == sexo(pre(a))}
	\asegura{anoNacimiento(a)==anoNacimiento(pre(a))}
	\asegura{nacionalidad(a)==nacionalidad(pre(a))}
	\asegura{ciaNumber(a)==ciaNumber(pre(a))}
	\asegura{(\forall d' \leftarrow deportes(pre(a)))capacidad(a,d')==capacidad(pre(a),d')}

	\asegura{mismos(deportes(a),d:deportes(pre(a)))}
	\asegura{ordenada(deportes(a))}
	\asegura{capacidad(a,d)==c}
\end{problema}



\section{Competencia}

\input{tipos/competencia.tex}

\begin{problema}{finalizarCompetencia}{c: Competencia, posiciones: [Atleta], control: [(Atleta, \bool)]}{}
	%definir mismos en Auxiliares
	\requiere{\neg finalizada(c)}
	\requiere{contenida(posiciones,participantes(c))}
	\requiere{sinRepetidos(posiciones)}
	\requiere{(\forall x \leftarrow control) prm(x) \in participantes(c)}
	\requiere{sinRepetidos([prm(x) | x \leftarrow control])}
	\modifica{c}
	\asegura{finalizada(c)}
	\asegura{ranking(c)==posiciones}
	\asegura{participantes(c)==participantes(pre(c))}
	\asegura{mismos(LesTocoControlAntiDoping(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}
	\requiere{finalizada(c)}
	\asegura{res==(\forall x \leftarrow[0..|ranking(c)|-2]) \newline
	capacidad(ranking(c)[x],prm(categoria(c))) \geq capacidad(ranking(c)[x+1],prm(categoria(c)))}
\end{problema}

\begin{problema}{sancionarTramposos}{c: Competencia}{}
	\requiere{finalizada(c)}
	\modifica{c}
	\asegura{finalizada(c)}
	\asegura{categoria(c)==categoria(pre(c))}
	\asegura{mismos(participantes(c),participantes(pre(c)))}
	\asegura{incluida(ranking(c),participantes(c))}
	\asegura{incluida(LesTocoControlAntiDoping(c),participantes(c))}
	\asegura{mismos(ranking(pre(c)),ranking(c)++listaDoping(c,LesTocoControlAntiDoping(c)))}
	\asegura{ranking==[ el | el \leftarrow ranking(pre(c)),el \notin listaDoping(c,LesTocoControlAntiDoping(c))]}

	\aux{listaDoping}{c:competencia, a:[atleta]}{[atleta]}{[x|x \leftarrow a, leDioPositivo(c,x)]}

\end{problema}

\section{JJOO}
\input{tipos/jjoo.tex}

\begin{problema}{dePaseo}{j: JJOO}{[Atleta]} 
	\asegura{mismos(res,noParticiparon(j))}
	\aux{noParticiparon}{j: JJOO}{[Atleta]}{[x | x \leftarrow atletas(j), \neg en(x, participaronConRepes(j))]}
	\aux{participaronConRepes}{j: JJOO}{[Atleta]}{[atl | dia \leftarrow [1..cantDias(j)], comp \leftarrow cronograma(j, dia), atl \leftarrow atletas(j), en(atl, participantes(comp))]}

\end{problema}

\begin{problema}{medallero}{j: JJOO}{[(Pais, [\ent])]}
\end{problema}

\begin{problema}{boicotPorDisciplina}{j: JJOO, cat: (Deporte, Sexo), p: Pais}{\ent}
\end{problema}



\begin{problema}{losMasFracasados}{j: JJOO, p: Pais}{[Atleta]}
	%\\asegura{(\forall x \rightarrow [ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl) | atl \rightarrow res, comp \rightarrow todasLasCompetencias(j), finalizada(comp)]) x}
	%\\asegura{(\forAll x \rightarrow [ciaNumber(ranking(comp)[0]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[1]) \neq ciaNumber(atl) \wedge ciaNumber(ranking(comp)[2]) \neq ciaNumber(atl) | atl \rightarrow res, comp \rightarrow todasLasCompetencias(j), finalizada(comp)]) x}
	%\\asegura{(\forAll x \rightarrow res) nacionalidad(x) == p}
	%\\asegura{(\forAll i \rightarrow [0..|res|-2]) competenciasEnLasQueParticipo(j, res[i]) \geq competenciasEnLasQueParticipo(j, res[i+1])}
	%\\aux{competenciasEnLasQueParticipo}{j: JJOO, a: Atleta}{\ent}{\longitud{[z | z \leftarrow todasLasCompetencias(j), en(a, participantes(z))]}}
\end{problema}

\begin{problema}{liuSong}{j: JJOO, a: Atleta, p: Pa\'is}{}
\end{problema}

\begin{problema}{stevenBradbury}{j: JJOO}{Atleta}
\end{problema}

\begin{problema}{uyOrdenadoAs\'iHayUnPatr\'on}{j: JJOO}{\bool}
\end{problema}


\begin{problema}{sequ\'iaOl\'impica}{j: JJOO}{[Pa\'is]}
\end{problema}

\begin{problema}{transcurrirDia}{j: JJOO}{}
\end{problema}

\section{Auxiliares}

\input{auxiliaresTipos.tex}

\end{document}