Normalised(
THEORY MagicNumberX IS
  MagicNumber(Machine(TP3WinnieMachine))==(3.5)
END
&
THEORY UpperLevelX IS
  First_Level(Machine(TP3WinnieMachine))==(Machine(TP3WinnieMachine));
  Level(Machine(TP3WinnieMachine))==(0)
END
&
THEORY LoadedStructureX IS
  Machine(TP3WinnieMachine)
END
&
THEORY ListSeesX IS
  List_Sees(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListUsesX IS
  List_Uses(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListIncludesX IS
  Inherited_List_Includes(Machine(TP3WinnieMachine))==(?);
  List_Includes(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListPromotesX IS
  List_Promotes(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListExtendsX IS
  List_Extends(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListVariablesX IS
  External_Context_List_Variables(Machine(TP3WinnieMachine))==(?);
  Context_List_Variables(Machine(TP3WinnieMachine))==(?);
  Abstract_List_Variables(Machine(TP3WinnieMachine))==(?);
  Local_List_Variables(Machine(TP3WinnieMachine))==(NbPlaces);
  List_Variables(Machine(TP3WinnieMachine))==(NbPlaces);
  External_List_Variables(Machine(TP3WinnieMachine))==(NbPlaces)
END
&
THEORY ListVisibleVariablesX IS
  Inherited_List_VisibleVariables(Machine(TP3WinnieMachine))==(?);
  Abstract_List_VisibleVariables(Machine(TP3WinnieMachine))==(?);
  External_List_VisibleVariables(Machine(TP3WinnieMachine))==(?);
  Expanded_List_VisibleVariables(Machine(TP3WinnieMachine))==(?);
  List_VisibleVariables(Machine(TP3WinnieMachine))==(?);
  Internal_List_VisibleVariables(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListInvariantX IS
  Gluing_Seen_List_Invariant(Machine(TP3WinnieMachine))==(btrue);
  Gluing_List_Invariant(Machine(TP3WinnieMachine))==(btrue);
  Expanded_List_Invariant(Machine(TP3WinnieMachine))==(btrue);
  Abstract_List_Invariant(Machine(TP3WinnieMachine))==(btrue);
  Context_List_Invariant(Machine(TP3WinnieMachine))==(btrue);
  List_Invariant(Machine(TP3WinnieMachine))==(NbPlaces: 0..600)
END
&
THEORY ListAssertionsX IS
  Expanded_List_Assertions(Machine(TP3WinnieMachine))==(btrue);
  Abstract_List_Assertions(Machine(TP3WinnieMachine))==(btrue);
  Context_List_Assertions(Machine(TP3WinnieMachine))==(btrue);
  List_Assertions(Machine(TP3WinnieMachine))==(btrue)
END
&
THEORY ListInitialisationX IS
  Expanded_List_Initialisation(Machine(TP3WinnieMachine))==(NbPlaces:=600);
  Context_List_Initialisation(Machine(TP3WinnieMachine))==(skip);
  List_Initialisation(Machine(TP3WinnieMachine))==(NbPlaces:=600)
END
&
THEORY ListParametersX IS
  List_Parameters(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListInstanciatedParametersX END
&
THEORY ListConstraintsX IS
  List_Context_Constraints(Machine(TP3WinnieMachine))==(btrue);
  List_Constraints(Machine(TP3WinnieMachine))==(btrue)
END
&
THEORY ListOperationsX IS
  Internal_List_Operations(Machine(TP3WinnieMachine))==(Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures);
  List_Operations(Machine(TP3WinnieMachine))==(Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures)
END
&
THEORY ListInputX IS
  List_Input(Machine(TP3WinnieMachine),Ajout_Voiture)==(?);
  List_Input(Machine(TP3WinnieMachine),Retire_Voiture)==(?);
  List_Input(Machine(TP3WinnieMachine),Get_NbLibre)==(?);
  List_Input(Machine(TP3WinnieMachine),Get_NbVoitures)==(?)
END
&
THEORY ListOutputX IS
  List_Output(Machine(TP3WinnieMachine),Ajout_Voiture)==(?);
  List_Output(Machine(TP3WinnieMachine),Retire_Voiture)==(?);
  List_Output(Machine(TP3WinnieMachine),Get_NbLibre)==(NbLibre);
  List_Output(Machine(TP3WinnieMachine),Get_NbVoitures)==(NbVoitures)
END
&
THEORY ListHeaderX IS
  List_Header(Machine(TP3WinnieMachine),Ajout_Voiture)==(Ajout_Voiture);
  List_Header(Machine(TP3WinnieMachine),Retire_Voiture)==(Retire_Voiture);
  List_Header(Machine(TP3WinnieMachine),Get_NbLibre)==(NbLibre <-- Get_NbLibre);
  List_Header(Machine(TP3WinnieMachine),Get_NbVoitures)==(NbVoitures <-- Get_NbVoitures)
END
&
THEORY ListPreconditionX IS
  List_Precondition(Machine(TP3WinnieMachine),Ajout_Voiture)==(NbPlaces>0);
  List_Precondition(Machine(TP3WinnieMachine),Retire_Voiture)==(NbPlaces: 0..599);
  List_Precondition(Machine(TP3WinnieMachine),Get_NbLibre)==(btrue);
  List_Precondition(Machine(TP3WinnieMachine),Get_NbVoitures)==(btrue)
END
&
THEORY ListSubstitutionX IS
  Expanded_List_Substitution(Machine(TP3WinnieMachine),Get_NbVoitures)==(btrue | NbVoitures:=600-NbPlaces);
  Expanded_List_Substitution(Machine(TP3WinnieMachine),Get_NbLibre)==(btrue | NbLibre:=NbPlaces);
  Expanded_List_Substitution(Machine(TP3WinnieMachine),Retire_Voiture)==(NbPlaces: 0..599 | NbPlaces:=NbPlaces+1);
  Expanded_List_Substitution(Machine(TP3WinnieMachine),Ajout_Voiture)==(NbPlaces>0 | NbPlaces:=NbPlaces-1);
  List_Substitution(Machine(TP3WinnieMachine),Ajout_Voiture)==(NbPlaces:=NbPlaces-1);
  List_Substitution(Machine(TP3WinnieMachine),Retire_Voiture)==(NbPlaces:=NbPlaces+1);
  List_Substitution(Machine(TP3WinnieMachine),Get_NbLibre)==(NbLibre:=NbPlaces);
  List_Substitution(Machine(TP3WinnieMachine),Get_NbVoitures)==(NbVoitures:=600-NbPlaces)
END
&
THEORY ListConstantsX IS
  List_Valuable_Constants(Machine(TP3WinnieMachine))==(?);
  Inherited_List_Constants(Machine(TP3WinnieMachine))==(?);
  List_Constants(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListSetsX IS
  Context_List_Enumerated(Machine(TP3WinnieMachine))==(?);
  Context_List_Defered(Machine(TP3WinnieMachine))==(?);
  Context_List_Sets(Machine(TP3WinnieMachine))==(?);
  List_Valuable_Sets(Machine(TP3WinnieMachine))==(?);
  Inherited_List_Enumerated(Machine(TP3WinnieMachine))==(?);
  Inherited_List_Defered(Machine(TP3WinnieMachine))==(?);
  Inherited_List_Sets(Machine(TP3WinnieMachine))==(?);
  List_Enumerated(Machine(TP3WinnieMachine))==(?);
  List_Defered(Machine(TP3WinnieMachine))==(?);
  List_Sets(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListHiddenConstantsX IS
  Abstract_List_HiddenConstants(Machine(TP3WinnieMachine))==(?);
  Expanded_List_HiddenConstants(Machine(TP3WinnieMachine))==(?);
  List_HiddenConstants(Machine(TP3WinnieMachine))==(?);
  External_List_HiddenConstants(Machine(TP3WinnieMachine))==(?)
END
&
THEORY ListPropertiesX IS
  Abstract_List_Properties(Machine(TP3WinnieMachine))==(btrue);
  Context_List_Properties(Machine(TP3WinnieMachine))==(btrue);
  Inherited_List_Properties(Machine(TP3WinnieMachine))==(btrue);
  List_Properties(Machine(TP3WinnieMachine))==(btrue)
END
&
THEORY ListSeenInfoX END
&
THEORY ListOfIdsX IS
  List_Of_Ids(Machine(TP3WinnieMachine)) == (? | ? | NbPlaces | ? | Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures | ? | ? | ? | TP3WinnieMachine);
  List_Of_HiddenCst_Ids(Machine(TP3WinnieMachine)) == (? | ?);
  List_Of_VisibleCst_Ids(Machine(TP3WinnieMachine)) == (?);
  List_Of_VisibleVar_Ids(Machine(TP3WinnieMachine)) == (? | ?);
  List_Of_Ids_SeenBNU(Machine(TP3WinnieMachine)) == (?: ?)
END
&
THEORY VariablesEnvX IS
  Variables(Machine(TP3WinnieMachine)) == (Type(NbPlaces) == Mvl(btype(INTEGER,?,?)))
END
&
THEORY OperationsEnvX IS
  Operations(Machine(TP3WinnieMachine)) == (Type(Get_NbVoitures) == Cst(btype(INTEGER,?,?),No_type);Type(Get_NbLibre) == Cst(btype(INTEGER,?,?),No_type);Type(Retire_Voiture) == Cst(No_type,No_type);Type(Ajout_Voiture) == Cst(No_type,No_type));
  Observers(Machine(TP3WinnieMachine)) == (Type(Get_NbVoitures) == Cst(btype(INTEGER,?,?),No_type);Type(Get_NbLibre) == Cst(btype(INTEGER,?,?),No_type))
END
&
THEORY TCIntRdX IS
  predB0 == OK;
  extended_sees == KO;
  B0check_tab == KO;
  local_op == OK;
  abstract_constants_visible_in_values == KO
END
)