\aux{ciaNumbers}{as: [Atleta]}{[\ent]}{\comp{ciaNumber(a)}{a \selec as}}
\aux{competencias}{j: JJOO}{[Competencia]}{\comp{c}{d \selec [1..cantDias(j)], c \selec cronograma(j, d)}}
\aux{incluida}{$l_1$, $l_2$:[T]}{\bool}{(\forall x \selec l_1) cuenta(x, l_1) \leq cuenta(x, l_2)}
\aux{lasPasadasFinalizaron}{j: JJOO}{\bool}{(\forall d \selec [1..jornadaActual(j)))(\forall c \selec cronograma(j, d))finalizada(c)}
\aux{lasQueNoPasaronNoFinalizaron}{j: JJOO}{\bool}{\\(\forall d \selec (jornadaActual(j)..cantDias(j)]) (\forall c \selec cronograma(j, d))\neg finalizada(c)}
\aux{ordenada}{l:[T]}{\bool}{(\forall i \selec [0.. \longitud{l}-1)) l_i \leq l_{i+1}}
\aux{sinRepetidos}{l: [T]}{\bool}{(\forall i, j \selec [0.. \longitud{l}), i \neq j) l_i \neq l_j}

%agregadas por nosotros
\aux{maximoLista}{ls:[\ent]}{\ent}{[x|x\leftarrow ls, (\forall y \leftarrow ls) x \geq y][0]}
\aux{cuenta}{x:T, a:[T]}{\ent}{|([y | y \leftarrow a, y == x])|} 
\aux{mismos}{a:[t], b:[T]}{Bool}{|a|==|b| \wedge (\forall c \leftarrow a) cuenta(c,a) == cuenta(c,b)}
\aux{listaDoping}{c:competencia, a:[atleta]}{[atleta]}{[x | x \leftarrow a, leDioPositivo(c,x)]}
\aux{todasLasCompetencias}{j:JJOO}{[competencia]}{[x | y \leftarrow [1..cantDias(j)], x \leftarrow cronogramas(j,y) ] }
\aux{listaNacionalidadesAtletas}{j: JJOO}{[Pais]}{[nacionalidad(at) | at \leftarrow atletas(j)]}
\aux{sacarRepeticiones}{ls : [T]}{[T]}{[ls[x] | x \leftarrow [0..|ls|-1], \neg en(ls[x], ls[0..x-1])]}
\aux{listaPaises}{j:JJOO}{[Pais]}{sacarRepeticiones(listaNacionalidadesAtletas(j))}