-- P1: a sequ�ncia de professores n�o tem repeti��es
					card elems professores = len professores
      -- P2: todos os professores indicam prefer�ncias
					and elems professores <-: preferencias = {|->}
      -- P3: as vagas referidas nas prefer�ncias est�o no conjunto das vagas
          and  dunion {elems x | x in set rng preferencias} subset vagas
      -- P4: a lista de prefer�ncias de um professor n�o tem repeti��es
          and forall p in set elems professores &  len preferencias(p) = card elems preferencias(p)
      -- P5: os professores com coloca��o inicial est�o no conjunto dos professores
          and dom colocacaoInicial subset elems professores
      -- P6: as vagas referidas na coloca��o inicial est�o no conjunto das vagas
      -- (implicado por P3 e P7)
          and rng colocacaoInicial subset vagas
      -- P7: no caso de professores que tinham coloca��o inicial, a sua coloca��o inicial
      -- deve estar no fim da lista de prefer�ncias
          --and forall x in set dom colocacaoInicial & colocacaoInicial(x) = preferencias(x)(len preferencias(x) - 1)