Normalised(
THEORY MagicNumberX IS
  MagicNumber(Machine(TP1LapinWinnie))==(3.5)
END
&
THEORY UpperLevelX IS
  First_Level(Machine(TP1LapinWinnie))==(Machine(TP1LapinWinnie));
  Level(Machine(TP1LapinWinnie))==(0)
END
&
THEORY LoadedStructureX IS
  Machine(TP1LapinWinnie)
END
&
THEORY ListSeesX IS
  List_Sees(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListUsesX IS
  List_Uses(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListIncludesX IS
  Inherited_List_Includes(Machine(TP1LapinWinnie))==(?);
  List_Includes(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListPromotesX IS
  List_Promotes(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListExtendsX IS
  List_Extends(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListVariablesX IS
  External_Context_List_Variables(Machine(TP1LapinWinnie))==(?);
  Context_List_Variables(Machine(TP1LapinWinnie))==(?);
  Abstract_List_Variables(Machine(TP1LapinWinnie))==(?);
  Local_List_Variables(Machine(TP1LapinWinnie))==(pratique,sport,etudiant);
  List_Variables(Machine(TP1LapinWinnie))==(pratique,sport,etudiant);
  External_List_Variables(Machine(TP1LapinWinnie))==(pratique,sport,etudiant)
END
&
THEORY ListVisibleVariablesX IS
  Inherited_List_VisibleVariables(Machine(TP1LapinWinnie))==(?);
  Abstract_List_VisibleVariables(Machine(TP1LapinWinnie))==(?);
  External_List_VisibleVariables(Machine(TP1LapinWinnie))==(?);
  Expanded_List_VisibleVariables(Machine(TP1LapinWinnie))==(?);
  List_VisibleVariables(Machine(TP1LapinWinnie))==(?);
  Internal_List_VisibleVariables(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListInvariantX IS
  Gluing_Seen_List_Invariant(Machine(TP1LapinWinnie))==(btrue);
  Gluing_List_Invariant(Machine(TP1LapinWinnie))==(btrue);
  Expanded_List_Invariant(Machine(TP1LapinWinnie))==(btrue);
  Abstract_List_Invariant(Machine(TP1LapinWinnie))==(btrue);
  Context_List_Invariant(Machine(TP1LapinWinnie))==(btrue);
  List_Invariant(Machine(TP1LapinWinnie))==(etudiant <: ETUDIANT & sport <: SPORT & pratique: etudiant --> sport)
END
&
THEORY ListAssertionsX IS
  Expanded_List_Assertions(Machine(TP1LapinWinnie))==(btrue);
  Abstract_List_Assertions(Machine(TP1LapinWinnie))==(btrue);
  Context_List_Assertions(Machine(TP1LapinWinnie))==(btrue);
  List_Assertions(Machine(TP1LapinWinnie))==(btrue)
END
&
THEORY ListInitialisationX IS
  Expanded_List_Initialisation(Machine(TP1LapinWinnie))==(etudiant,sport,pratique:={},{},{});
  Context_List_Initialisation(Machine(TP1LapinWinnie))==(skip);
  List_Initialisation(Machine(TP1LapinWinnie))==(etudiant,sport,pratique:={},{},{})
END
&
THEORY ListParametersX IS
  List_Parameters(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListInstanciatedParametersX END
&
THEORY ListConstraintsX IS
  List_Context_Constraints(Machine(TP1LapinWinnie))==(btrue);
  List_Constraints(Machine(TP1LapinWinnie))==(btrue)
END
&
THEORY ListOperationsX IS
  Internal_List_Operations(Machine(TP1LapinWinnie))==(ajout_etudiant,ajout_sport,supprimer_etudiant,supprimer_sport,Quel_sport,Quels_etudiants);
  List_Operations(Machine(TP1LapinWinnie))==(ajout_etudiant,ajout_sport,supprimer_etudiant,supprimer_sport,Quel_sport,Quels_etudiants)
END
&
THEORY ListInputX IS
  List_Input(Machine(TP1LapinWinnie),ajout_etudiant)==(ee,ss);
  List_Input(Machine(TP1LapinWinnie),ajout_sport)==(ss);
  List_Input(Machine(TP1LapinWinnie),supprimer_etudiant)==(ee);
  List_Input(Machine(TP1LapinWinnie),supprimer_sport)==(ss);
  List_Input(Machine(TP1LapinWinnie),Quel_sport)==(ee);
  List_Input(Machine(TP1LapinWinnie),Quels_etudiants)==(ss)
END
&
THEORY ListOutputX IS
  List_Output(Machine(TP1LapinWinnie),ajout_etudiant)==(?);
  List_Output(Machine(TP1LapinWinnie),ajout_sport)==(?);
  List_Output(Machine(TP1LapinWinnie),supprimer_etudiant)==(?);
  List_Output(Machine(TP1LapinWinnie),supprimer_sport)==(?);
  List_Output(Machine(TP1LapinWinnie),Quel_sport)==(ss);
  List_Output(Machine(TP1LapinWinnie),Quels_etudiants)==(ee)
END
&
THEORY ListHeaderX IS
  List_Header(Machine(TP1LapinWinnie),ajout_etudiant)==(ajout_etudiant(ee,ss));
  List_Header(Machine(TP1LapinWinnie),ajout_sport)==(ajout_sport(ss));
  List_Header(Machine(TP1LapinWinnie),supprimer_etudiant)==(supprimer_etudiant(ee));
  List_Header(Machine(TP1LapinWinnie),supprimer_sport)==(supprimer_sport(ss));
  List_Header(Machine(TP1LapinWinnie),Quel_sport)==(ss <-- Quel_sport(ee));
  List_Header(Machine(TP1LapinWinnie),Quels_etudiants)==(ee <-- Quels_etudiants(ss))
END
&
THEORY ListPreconditionX IS
  List_Precondition(Machine(TP1LapinWinnie),ajout_etudiant)==(ee: ETUDIANT-etudiant & ss: sport);
  List_Precondition(Machine(TP1LapinWinnie),ajout_sport)==(ss: SPORT-sport);
  List_Precondition(Machine(TP1LapinWinnie),supprimer_etudiant)==(ee: etudiant);
  List_Precondition(Machine(TP1LapinWinnie),supprimer_sport)==(ss: sport & ss/:ran(pratique));
  List_Precondition(Machine(TP1LapinWinnie),Quel_sport)==(ee: dom(pratique));
  List_Precondition(Machine(TP1LapinWinnie),Quels_etudiants)==(ss: ran(pratique))
END
&
THEORY ListSubstitutionX IS
  Expanded_List_Substitution(Machine(TP1LapinWinnie),Quels_etudiants)==(ss: ran(pratique) | ee:=pratique~(ss));
  Expanded_List_Substitution(Machine(TP1LapinWinnie),Quel_sport)==(ee: dom(pratique) | ss:=pratique(ee));
  Expanded_List_Substitution(Machine(TP1LapinWinnie),supprimer_sport)==(ss: sport & ss/:ran(pratique) | sport:=sport-{ss});
  Expanded_List_Substitution(Machine(TP1LapinWinnie),supprimer_etudiant)==(ee: etudiant | pratique,etudiant:={ee}<<|pratique,etudiant-{ee});
  Expanded_List_Substitution(Machine(TP1LapinWinnie),ajout_sport)==(ss: SPORT-sport | sport:=sport\/{ss});
  Expanded_List_Substitution(Machine(TP1LapinWinnie),ajout_etudiant)==(ee: ETUDIANT-etudiant & ss: sport | etudiant,pratique:=etudiant\/{ee},pratique\/{ee|->ss});
  List_Substitution(Machine(TP1LapinWinnie),ajout_etudiant)==(etudiant:=etudiant\/{ee} || pratique:=pratique\/{ee|->ss});
  List_Substitution(Machine(TP1LapinWinnie),ajout_sport)==(sport:=sport\/{ss});
  List_Substitution(Machine(TP1LapinWinnie),supprimer_etudiant)==(pratique:={ee}<<|pratique || etudiant:=etudiant-{ee});
  List_Substitution(Machine(TP1LapinWinnie),supprimer_sport)==(sport:=sport-{ss});
  List_Substitution(Machine(TP1LapinWinnie),Quel_sport)==(ss:=pratique(ee));
  List_Substitution(Machine(TP1LapinWinnie),Quels_etudiants)==(ee:=pratique~(ss))
END
&
THEORY ListConstantsX IS
  List_Valuable_Constants(Machine(TP1LapinWinnie))==(?);
  Inherited_List_Constants(Machine(TP1LapinWinnie))==(?);
  List_Constants(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListSetsX IS
  Set_Definition(Machine(TP1LapinWinnie),ETUDIANT)==(?);
  Context_List_Enumerated(Machine(TP1LapinWinnie))==(?);
  Context_List_Defered(Machine(TP1LapinWinnie))==(?);
  Context_List_Sets(Machine(TP1LapinWinnie))==(?);
  List_Valuable_Sets(Machine(TP1LapinWinnie))==(ETUDIANT,SPORT);
  Inherited_List_Enumerated(Machine(TP1LapinWinnie))==(?);
  Inherited_List_Defered(Machine(TP1LapinWinnie))==(?);
  Inherited_List_Sets(Machine(TP1LapinWinnie))==(?);
  List_Enumerated(Machine(TP1LapinWinnie))==(?);
  List_Defered(Machine(TP1LapinWinnie))==(ETUDIANT,SPORT);
  List_Sets(Machine(TP1LapinWinnie))==(ETUDIANT,SPORT);
  Set_Definition(Machine(TP1LapinWinnie),SPORT)==(?)
END
&
THEORY ListHiddenConstantsX IS
  Abstract_List_HiddenConstants(Machine(TP1LapinWinnie))==(?);
  Expanded_List_HiddenConstants(Machine(TP1LapinWinnie))==(?);
  List_HiddenConstants(Machine(TP1LapinWinnie))==(?);
  External_List_HiddenConstants(Machine(TP1LapinWinnie))==(?)
END
&
THEORY ListPropertiesX IS
  Abstract_List_Properties(Machine(TP1LapinWinnie))==(btrue);
  Context_List_Properties(Machine(TP1LapinWinnie))==(btrue);
  Inherited_List_Properties(Machine(TP1LapinWinnie))==(btrue);
  List_Properties(Machine(TP1LapinWinnie))==(ETUDIANT: FIN(INTEGER) & not(ETUDIANT = {}) & SPORT: FIN(INTEGER) & not(SPORT = {}))
END
&
THEORY ListSeenInfoX END
&
THEORY ListOfIdsX IS
  List_Of_Ids(Machine(TP1LapinWinnie)) == (ETUDIANT,SPORT | ? | pratique,sport,etudiant | ? | ajout_etudiant,ajout_sport,supprimer_etudiant,supprimer_sport,Quel_sport,Quels_etudiants | ? | ? | ? | TP1LapinWinnie);
  List_Of_HiddenCst_Ids(Machine(TP1LapinWinnie)) == (? | ?);
  List_Of_VisibleCst_Ids(Machine(TP1LapinWinnie)) == (?);
  List_Of_VisibleVar_Ids(Machine(TP1LapinWinnie)) == (? | ?);
  List_Of_Ids_SeenBNU(Machine(TP1LapinWinnie)) == (?: ?)
END
&
THEORY SetsEnvX IS
  Sets(Machine(TP1LapinWinnie)) == (Type(ETUDIANT) == Cst(SetOf(atype(ETUDIANT,"[ETUDIANT","]ETUDIANT")));Type(SPORT) == Cst(SetOf(atype(SPORT,"[SPORT","]SPORT"))))
END
&
THEORY VariablesEnvX IS
  Variables(Machine(TP1LapinWinnie)) == (Type(pratique) == Mvl(SetOf(atype(ETUDIANT,?,?)*atype(SPORT,?,?)));Type(sport) == Mvl(SetOf(atype(SPORT,?,?)));Type(etudiant) == Mvl(SetOf(atype(ETUDIANT,?,?))))
END
&
THEORY OperationsEnvX IS
  Operations(Machine(TP1LapinWinnie)) == (Type(Quels_etudiants) == Cst(atype(ETUDIANT,?,?),atype(SPORT,?,?));Type(Quel_sport) == Cst(atype(SPORT,?,?),atype(ETUDIANT,?,?));Type(supprimer_sport) == Cst(No_type,atype(SPORT,?,?));Type(supprimer_etudiant) == Cst(No_type,atype(ETUDIANT,?,?));Type(ajout_sport) == Cst(No_type,atype(SPORT,?,?));Type(ajout_etudiant) == Cst(No_type,atype(ETUDIANT,?,?)*atype(SPORT,?,?)));
  Observers(Machine(TP1LapinWinnie)) == (Type(Quels_etudiants) == Cst(atype(ETUDIANT,?,?),atype(SPORT,?,?));Type(Quel_sport) == Cst(atype(SPORT,?,?),atype(ETUDIANT,?,?)))
END
&
THEORY TCIntRdX IS
  predB0 == OK;
  extended_sees == KO;
  B0check_tab == KO;
  local_op == OK;
  abstract_constants_visible_in_values == KO
END
)