module AlgoOrdreAppelSortie
  [@java:package:fr.parcoursup.whyml.ordreappel.algo]
  use mach.java.lang.Integer
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_entree.AlgoOrdreAppelEntree as Entree

  clone export fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_donnees_clone.AlgoOrdreAppelDonneesClone

  let algo_ordre_appel_sortie () = algo_ordre_appel_donnees ()

  predicate algo_ordre_appel_entree_sortie_ok (entree : Entree.t) (sortie : t) =
    Entree.get_nb_groupes entree = get_nb_groupes sortie /\
    forall i : integer. 0 <= i < get_nb_groupes sortie ->
      Entree.get_ith_c_gp_cod_safe entree i = get_ith_c_gp_cod_safe sortie i  /\
      seq_voeu_eq_up_to_rang_appel (get_ordre_pedagogique entree[i]) (get_ordre_pedagogique sortie[i])

  predicate algo_ordre_appel_sortie_ok (sortie : t) =
    forall i : integer. 0 <= i < get_nb_groupes sortie ->
      ordre_appel_properties sortie[i]

end

(* generated on Mon Dec  2 02:04:28 UTC 2024 from rev:  *)