Normalised(
THEORY MagicNumberX IS
  MagicNumber(Implementation(TP3WinnieImp))==(3.5)
END
&
THEORY UpperLevelX IS
  First_Level(Implementation(TP3WinnieImp))==(Machine(TP3WinnieMachine));
  Level(Implementation(TP3WinnieImp))==(1);
  Upper_Level(Implementation(TP3WinnieImp))==(Machine(TP3WinnieMachine))
END
&
THEORY LoadedStructureX IS
  Implementation(TP3WinnieImp)
END
&
THEORY ListSeesX IS
  List_Sees(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListIncludesX IS
  List_Includes(Implementation(TP3WinnieImp))==(?);
  Inherited_List_Includes(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListPromotesX IS
  List_Promotes(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListExtendsX IS
  List_Extends(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListVariablesX IS
  External_Context_List_Variables(Implementation(TP3WinnieImp))==(?);
  Context_List_Variables(Implementation(TP3WinnieImp))==(?);
  Abstract_List_Variables(Implementation(TP3WinnieImp))==(NbPlaces);
  Local_List_Variables(Implementation(TP3WinnieImp))==(?);
  List_Variables(Implementation(TP3WinnieImp))==(?);
  External_List_Variables(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListVisibleVariablesX IS
  Inherited_List_VisibleVariables(Implementation(TP3WinnieImp))==(?);
  Abstract_List_VisibleVariables(Implementation(TP3WinnieImp))==(?);
  External_List_VisibleVariables(Implementation(TP3WinnieImp))==(?);
  Expanded_List_VisibleVariables(Implementation(TP3WinnieImp))==(?);
  List_VisibleVariables(Implementation(TP3WinnieImp))==(C_NbPlaces);
  Internal_List_VisibleVariables(Implementation(TP3WinnieImp))==(C_NbPlaces)
END
&
THEORY ListInvariantX IS
  Gluing_Seen_List_Invariant(Implementation(TP3WinnieImp))==(btrue);
  Expanded_List_Invariant(Implementation(TP3WinnieImp))==(btrue);
  Abstract_List_Invariant(Implementation(TP3WinnieImp))==(NbPlaces: 0..600);
  Context_List_Invariant(Implementation(TP3WinnieImp))==(btrue);
  List_Invariant(Implementation(TP3WinnieImp))==(C_NbPlaces: 0..600 & C_NbPlaces = NbPlaces)
END
&
THEORY ListAssertionsX IS
  Expanded_List_Assertions(Implementation(TP3WinnieImp))==(btrue);
  Abstract_List_Assertions(Implementation(TP3WinnieImp))==(btrue);
  Context_List_Assertions(Implementation(TP3WinnieImp))==(btrue);
  List_Assertions(Implementation(TP3WinnieImp))==(btrue)
END
&
THEORY ListInitialisationX IS
  Expanded_List_Initialisation(Implementation(TP3WinnieImp))==(600: INT | C_NbPlaces:=600);
  Context_List_Initialisation(Implementation(TP3WinnieImp))==(skip);
  List_Initialisation(Implementation(TP3WinnieImp))==(C_NbPlaces:=600)
END
&
THEORY ListParametersX IS
  List_Parameters(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListInstanciatedParametersX END
&
THEORY ListConstraintsX IS
  List_Constraints(Implementation(TP3WinnieImp))==(btrue);
  List_Context_Constraints(Implementation(TP3WinnieImp))==(btrue)
END
&
THEORY ListOperationsX IS
  Internal_List_Operations(Implementation(TP3WinnieImp))==(Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures);
  List_Operations(Implementation(TP3WinnieImp))==(Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures)
END
&
THEORY ListInputX IS
  List_Input(Implementation(TP3WinnieImp),Ajout_Voiture)==(?);
  List_Input(Implementation(TP3WinnieImp),Retire_Voiture)==(?);
  List_Input(Implementation(TP3WinnieImp),Get_NbLibre)==(?);
  List_Input(Implementation(TP3WinnieImp),Get_NbVoitures)==(?)
END
&
THEORY ListOutputX IS
  List_Output(Implementation(TP3WinnieImp),Ajout_Voiture)==(?);
  List_Output(Implementation(TP3WinnieImp),Retire_Voiture)==(?);
  List_Output(Implementation(TP3WinnieImp),Get_NbLibre)==(NbLibre);
  List_Output(Implementation(TP3WinnieImp),Get_NbVoitures)==(NbVoitures)
END
&
THEORY ListHeaderX IS
  List_Header(Implementation(TP3WinnieImp),Ajout_Voiture)==(Ajout_Voiture);
  List_Header(Implementation(TP3WinnieImp),Retire_Voiture)==(Retire_Voiture);
  List_Header(Implementation(TP3WinnieImp),Get_NbLibre)==(NbLibre <-- Get_NbLibre);
  List_Header(Implementation(TP3WinnieImp),Get_NbVoitures)==(NbVoitures <-- Get_NbVoitures)
END
&
THEORY ListPreconditionX IS
  Own_Precondition(Implementation(TP3WinnieImp),Ajout_Voiture)==(btrue);
  List_Precondition(Implementation(TP3WinnieImp),Ajout_Voiture)==(NbPlaces>0);
  Own_Precondition(Implementation(TP3WinnieImp),Retire_Voiture)==(btrue);
  List_Precondition(Implementation(TP3WinnieImp),Retire_Voiture)==(NbPlaces: 0..599);
  Own_Precondition(Implementation(TP3WinnieImp),Get_NbLibre)==(btrue);
  List_Precondition(Implementation(TP3WinnieImp),Get_NbLibre)==(btrue);
  Own_Precondition(Implementation(TP3WinnieImp),Get_NbVoitures)==(btrue);
  List_Precondition(Implementation(TP3WinnieImp),Get_NbVoitures)==(btrue)
END
&
THEORY ListSubstitutionX IS
  Expanded_List_Substitution(Implementation(TP3WinnieImp),Get_NbVoitures)==(btrue & 600-C_NbPlaces: INT & 600: INT & C_NbPlaces: INT | NbVoitures:=600-C_NbPlaces);
  Expanded_List_Substitution(Implementation(TP3WinnieImp),Get_NbLibre)==(btrue & C_NbPlaces: INT | NbLibre:=C_NbPlaces);
  Expanded_List_Substitution(Implementation(TP3WinnieImp),Retire_Voiture)==(NbPlaces: 0..599 & C_NbPlaces+1: INT & C_NbPlaces: INT & 1: INT | C_NbPlaces:=C_NbPlaces+1);
  Expanded_List_Substitution(Implementation(TP3WinnieImp),Ajout_Voiture)==(NbPlaces>0 & C_NbPlaces-1: INT & C_NbPlaces: INT & 1: INT | C_NbPlaces:=C_NbPlaces-1);
  List_Substitution(Implementation(TP3WinnieImp),Ajout_Voiture)==(C_NbPlaces:=C_NbPlaces-1);
  List_Substitution(Implementation(TP3WinnieImp),Retire_Voiture)==(C_NbPlaces:=C_NbPlaces+1);
  List_Substitution(Implementation(TP3WinnieImp),Get_NbLibre)==(NbLibre:=C_NbPlaces);
  List_Substitution(Implementation(TP3WinnieImp),Get_NbVoitures)==(NbVoitures:=600-C_NbPlaces)
END
&
THEORY ListConstantsX IS
  List_Valuable_Constants(Implementation(TP3WinnieImp))==(?);
  Inherited_List_Constants(Implementation(TP3WinnieImp))==(?);
  List_Constants(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListSetsX IS
  Context_List_Enumerated(Implementation(TP3WinnieImp))==(?);
  Context_List_Defered(Implementation(TP3WinnieImp))==(?);
  Context_List_Sets(Implementation(TP3WinnieImp))==(?);
  List_Own_Enumerated(Implementation(TP3WinnieImp))==(?);
  List_Valuable_Sets(Implementation(TP3WinnieImp))==(?);
  Inherited_List_Enumerated(Implementation(TP3WinnieImp))==(?);
  Inherited_List_Defered(Implementation(TP3WinnieImp))==(?);
  Inherited_List_Sets(Implementation(TP3WinnieImp))==(?);
  List_Enumerated(Implementation(TP3WinnieImp))==(?);
  List_Defered(Implementation(TP3WinnieImp))==(?);
  List_Sets(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListHiddenConstantsX IS
  Abstract_List_HiddenConstants(Implementation(TP3WinnieImp))==(?);
  Expanded_List_HiddenConstants(Implementation(TP3WinnieImp))==(?);
  List_HiddenConstants(Implementation(TP3WinnieImp))==(?);
  External_List_HiddenConstants(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListPropertiesX IS
  Abstract_List_Properties(Implementation(TP3WinnieImp))==(btrue);
  Context_List_Properties(Implementation(TP3WinnieImp))==(btrue);
  Inherited_List_Properties(Implementation(TP3WinnieImp))==(btrue);
  List_Properties(Implementation(TP3WinnieImp))==(btrue)
END
&
THEORY ListValuesX IS
  Values_Subs(Implementation(TP3WinnieImp))==(aa: aa);
  List_Values(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListSeenInfoX END
&
THEORY ListIncludedOperationsX END
&
THEORY InheritedEnvX IS
  VisibleVariables(Implementation(TP3WinnieImp))==(Type(C_NbPlaces) == Mvv(btype(INTEGER,?,?)));
  Operations(Implementation(TP3WinnieImp))==(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))
END
&
THEORY ListVisibleStaticX END
&
THEORY ListOfIdsX IS
  List_Of_Ids(Implementation(TP3WinnieImp)) == (? | ? | ? | ? | Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures | ? | ? | ? | TP3WinnieImp);
  List_Of_HiddenCst_Ids(Implementation(TP3WinnieImp)) == (? | ?);
  List_Of_VisibleCst_Ids(Implementation(TP3WinnieImp)) == (?);
  List_Of_VisibleVar_Ids(Implementation(TP3WinnieImp)) == (C_NbPlaces | ?);
  List_Of_Ids_SeenBNU(Implementation(TP3WinnieImp)) == (?: ?)
END
&
THEORY VisibleVariablesEnvX IS
  VisibleVariables(Implementation(TP3WinnieImp)) == (Type(C_NbPlaces) == Mvv(btype(INTEGER,?,?)))
END
&
THEORY TCIntRdX IS
  predB0 == OK;
  extended_sees == KO;
  B0check_tab == KO;
  local_op == OK;
  abstract_constants_visible_in_values == KO
END
&
THEORY ListLocalOperationsX IS
  List_Local_Operations(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListLocalInputX END
&
THEORY ListLocalOutputX END
&
THEORY ListLocalHeaderX END
&
THEORY ListLocalPreconditionX END
&
THEORY ListLocalSubstitutionX END
&
THEORY TypingPredicateX IS
  TypingPredicate(Implementation(TP3WinnieImp))==(C_NbPlaces: INTEGER)
END
&
THEORY ImportedVariablesListX END
&
THEORY ListLocalOpInvariantX END
)