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))==(C_TableParkings.BASIC_ARRAY_VAR);
  Inherited_List_Includes(Implementation(TP3WinnieImp))==(C_TableParkings.BASIC_ARRAY_VAR)
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))==(TableParkings);
  Local_List_Variables(Implementation(TP3WinnieImp))==(?);
  List_Variables(Implementation(TP3WinnieImp))==(C_TableParkingsarr_vrb);
  External_List_Variables(Implementation(TP3WinnieImp))==(C_TableParkings.arr_vrb)
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))==(?);
  Internal_List_VisibleVariables(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListInvariantX IS
  Gluing_Seen_List_Invariant(Implementation(TP3WinnieImp))==(btrue);
  Abstract_List_Invariant(Implementation(TP3WinnieImp))==(TableParkings: 0..10 --> 0..600);
  Expanded_List_Invariant(Implementation(TP3WinnieImp))==(C_TableParkingsarr_vrb: 0..10 --> 0..600);
  Context_List_Invariant(Implementation(TP3WinnieImp))==(btrue);
  List_Invariant(Implementation(TP3WinnieImp))==(C_TableParkingsarr_vrb = TableParkings)
END
&
THEORY ListAssertionsX IS
  Abstract_List_Assertions(Implementation(TP3WinnieImp))==(btrue);
  Expanded_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))==(@(arr_vrb$0).(arr_vrb$0: 0..10 --> 0..600 ==> C_TableParkingsarr_vrb:=arr_vrb$0);(0: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{0|->600});(1: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{1|->600});(2: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{2|->600});(3: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{3|->600});(4: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{4|->600});(5: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{5|->600});(6: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{6|->600});(7: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{7|->600});(8: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{8|->600});(9: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{9|->600});(10: 0..10 & 600: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{10|->600}));
  Context_List_Initialisation(Implementation(TP3WinnieImp))==(skip);
  List_Initialisation(Implementation(TP3WinnieImp))==((C_TableParkings.STR_ARRAY)(0,600);(C_TableParkings.STR_ARRAY)(1,600);(C_TableParkings.STR_ARRAY)(2,600);(C_TableParkings.STR_ARRAY)(3,600);(C_TableParkings.STR_ARRAY)(4,600);(C_TableParkings.STR_ARRAY)(5,600);(C_TableParkings.STR_ARRAY)(6,600);(C_TableParkings.STR_ARRAY)(7,600);(C_TableParkings.STR_ARRAY)(8,600);(C_TableParkings.STR_ARRAY)(9,600);(C_TableParkings.STR_ARRAY)(10,600))
END
&
THEORY ListParametersX IS
  List_Parameters(Implementation(TP3WinnieImp))==(?)
END
&
THEORY ListInstanciatedParametersX IS
  Precond_Instanciated_Parameters(Implementation(TP3WinnieImp),Machine(C_TableParkings.BASIC_ARRAY_VAR))==(btrue);
  List_Instanciated_Parameters(Implementation(TP3WinnieImp),Machine(C_TableParkings.BASIC_ARRAY_VAR))==(0..10,0..600)
END
&
THEORY ListConstraintsX IS
  List_Constraints(Implementation(TP3WinnieImp),Machine(C_TableParkings.BASIC_ARRAY_VAR))==(0..10: FIN(INTEGER) & not(0..10 = {}) & 0..600: FIN(INTEGER) & not(0..600 = {}));
  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)==(IdParking);
  List_Input(Implementation(TP3WinnieImp),Retire_Voiture)==(IdParking);
  List_Input(Implementation(TP3WinnieImp),Get_NbLibre)==(IdParking);
  List_Input(Implementation(TP3WinnieImp),Get_NbVoitures)==(IdParking)
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(IdParking));
  List_Header(Implementation(TP3WinnieImp),Retire_Voiture)==(Retire_Voiture(IdParking));
  List_Header(Implementation(TP3WinnieImp),Get_NbLibre)==(NbLibre <-- Get_NbLibre(IdParking));
  List_Header(Implementation(TP3WinnieImp),Get_NbVoitures)==(NbVoitures <-- Get_NbVoitures(IdParking))
END
&
THEORY ListPreconditionX IS
  Own_Precondition(Implementation(TP3WinnieImp),Ajout_Voiture)==(btrue);
  List_Precondition(Implementation(TP3WinnieImp),Ajout_Voiture)==(IdParking: 0..10 & TableParkings(IdParking)>0);
  Own_Precondition(Implementation(TP3WinnieImp),Retire_Voiture)==(btrue);
  List_Precondition(Implementation(TP3WinnieImp),Retire_Voiture)==(IdParking: 0..10 & TableParkings(IdParking): 0..599);
  Own_Precondition(Implementation(TP3WinnieImp),Get_NbLibre)==(btrue);
  List_Precondition(Implementation(TP3WinnieImp),Get_NbLibre)==(IdParking: 0..10);
  Own_Precondition(Implementation(TP3WinnieImp),Get_NbVoitures)==(btrue);
  List_Precondition(Implementation(TP3WinnieImp),Get_NbVoitures)==(IdParking: 0..10)
END
&
THEORY ListSubstitutionX IS
  Expanded_List_Substitution(Implementation(TP3WinnieImp),Get_NbVoitures)==(IdParking: 0..10 | @xx.((IdParking: 0..10 | xx:=C_TableParkingsarr_vrb(IdParking));(600-xx: INT & 600: INT & xx: INT | NbVoitures:=600-xx)));
  Expanded_List_Substitution(Implementation(TP3WinnieImp),Get_NbLibre)==(IdParking: 0..10 | NbLibre:=C_TableParkingsarr_vrb(IdParking));
  Expanded_List_Substitution(Implementation(TP3WinnieImp),Retire_Voiture)==(IdParking: 0..10 & TableParkings(IdParking): 0..599 | @xx.((IdParking: 0..10 | xx:=C_TableParkingsarr_vrb(IdParking));(xx+1: INT & xx: INT & 1: INT | xx:=xx+1);(IdParking: 0..10 & xx: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{IdParking|->xx})));
  Expanded_List_Substitution(Implementation(TP3WinnieImp),Ajout_Voiture)==(IdParking: 0..10 & TableParkings(IdParking)>0 | @xx.((IdParking: 0..10 | xx:=C_TableParkingsarr_vrb(IdParking));(xx-1: INT & xx: INT & 1: INT | xx:=xx-1);(IdParking: 0..10 & xx: 0..600 | C_TableParkingsarr_vrb:=C_TableParkingsarr_vrb<+{IdParking|->xx})));
  List_Substitution(Implementation(TP3WinnieImp),Ajout_Voiture)==(VAR xx IN xx <-- (C_TableParkings.VAL_ARRAY)(IdParking);xx:=xx-1;(C_TableParkings.STR_ARRAY)(IdParking,xx) END);
  List_Substitution(Implementation(TP3WinnieImp),Retire_Voiture)==(VAR xx IN xx <-- (C_TableParkings.VAL_ARRAY)(IdParking);xx:=xx+1;(C_TableParkings.STR_ARRAY)(IdParking,xx) END);
  List_Substitution(Implementation(TP3WinnieImp),Get_NbLibre)==(NbLibre <-- (C_TableParkings.VAL_ARRAY)(IdParking));
  List_Substitution(Implementation(TP3WinnieImp),Get_NbVoitures)==(VAR xx IN xx <-- (C_TableParkings.VAL_ARRAY)(IdParking);NbVoitures:=600-xx END)
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 IS
  List_Included_Operations(Implementation(TP3WinnieImp),Machine(BASIC_ARRAY_VAR))==(VAL_ARRAY,STR_ARRAY)
END
&
THEORY InheritedEnvX IS
  Operations(Implementation(TP3WinnieImp))==(Type(Get_NbVoitures) == Cst(btype(INTEGER,?,?),btype(INTEGER,?,?));Type(Get_NbLibre) == Cst(btype(INTEGER,?,?),btype(INTEGER,?,?));Type(Retire_Voiture) == Cst(No_type,btype(INTEGER,?,?));Type(Ajout_Voiture) == Cst(No_type,btype(INTEGER,?,?)))
END
&
THEORY ListVisibleStaticX END
&
THEORY ListOfIdsX IS
  List_Of_Ids(Implementation(TP3WinnieImp)) == (? | ? | ? | C_TableParkingsarr_vrb | Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures | ? | imported(Machine(C_TableParkings.BASIC_ARRAY_VAR)) | ? | TP3WinnieImp);
  List_Of_HiddenCst_Ids(Implementation(TP3WinnieImp)) == (? | ?);
  List_Of_VisibleCst_Ids(Implementation(TP3WinnieImp)) == (?);
  List_Of_VisibleVar_Ids(Implementation(TP3WinnieImp)) == (? | ?);
  List_Of_Ids_SeenBNU(Implementation(TP3WinnieImp)) == (?: ?);
  List_Of_Ids(Machine(BASIC_ARRAY_VAR)) == (? | ? | arr_vrb | ? | VAL_ARRAY,STR_ARRAY | ? | ? | BAV_INDEX,BAV_VALUE | BASIC_ARRAY_VAR);
  List_Of_HiddenCst_Ids(Machine(BASIC_ARRAY_VAR)) == (? | ?);
  List_Of_VisibleCst_Ids(Machine(BASIC_ARRAY_VAR)) == (?);
  List_Of_VisibleVar_Ids(Machine(BASIC_ARRAY_VAR)) == (? | ?);
  List_Of_Ids_SeenBNU(Machine(BASIC_ARRAY_VAR)) == (?: ?)
END
&
THEORY VariablesLocEnvX IS
  Variables_Loc(Implementation(TP3WinnieImp),Ajout_Voiture, 1) == (Type(xx) == Lvl(btype(INTEGER,?,?)));
  Variables_Loc(Implementation(TP3WinnieImp),Retire_Voiture, 1) == (Type(xx) == Lvl(btype(INTEGER,?,?)));
  Variables_Loc(Implementation(TP3WinnieImp),Get_NbVoitures, 1) == (Type(xx) == Lvl(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))==(btrue)
END
&
THEORY ImportedVariablesListX IS
  ImportedVariablesList(Implementation(TP3WinnieImp),Machine(C_TableParkings.BASIC_ARRAY_VAR))==(C_TableParkings.arr_vrb);
  ImportedVisVariablesList(Implementation(TP3WinnieImp),Machine(C_TableParkings.BASIC_ARRAY_VAR))==(?)
END
&
THEORY ListLocalOpInvariantX END
)