Normalised(
THEORY MagicNumberX IS
  MagicNumber(Implementation(SimulationImp))==(3.5)
END
&
THEORY UpperLevelX IS
  First_Level(Implementation(SimulationImp))==(Machine(Simulation));
  Level(Implementation(SimulationImp))==(1);
  Upper_Level(Implementation(SimulationImp))==(Machine(Simulation))
END
&
THEORY LoadedStructureX IS
  Implementation(SimulationImp)
END
&
THEORY ListSeesX IS
  List_Sees(Implementation(SimulationImp))==(?)
END
&
THEORY ListIncludesX IS
  List_Includes(Implementation(SimulationImp))==(BASIC_IO,affichage,TP3WinnieInterface);
  Inherited_List_Includes(Implementation(SimulationImp))==(TP3WinnieInterface,affichage,BASIC_IO)
END
&
THEORY ListPromotesX IS
  List_Promotes(Implementation(SimulationImp))==(?)
END
&
THEORY ListExtendsX IS
  List_Extends(Implementation(SimulationImp))==(?)
END
&
THEORY ListVariablesX IS
  External_Context_List_Variables(Implementation(SimulationImp))==(?);
  Context_List_Variables(Implementation(SimulationImp))==(?);
  Abstract_List_Variables(Implementation(SimulationImp))==(?);
  Local_List_Variables(Implementation(SimulationImp))==(?);
  List_Variables(Implementation(SimulationImp))==(?);
  External_List_Variables(Implementation(SimulationImp))==(?)
END
&
THEORY ListVisibleVariablesX IS
  Inherited_List_VisibleVariables(Implementation(SimulationImp))==(?);
  Abstract_List_VisibleVariables(Implementation(SimulationImp))==(?);
  External_List_VisibleVariables(Implementation(SimulationImp))==(?);
  Expanded_List_VisibleVariables(Implementation(SimulationImp))==(?);
  List_VisibleVariables(Implementation(SimulationImp))==(?);
  Internal_List_VisibleVariables(Implementation(SimulationImp))==(?)
END
&
THEORY ListInvariantX IS
  Gluing_Seen_List_Invariant(Implementation(SimulationImp))==(btrue);
  Abstract_List_Invariant(Implementation(SimulationImp))==(btrue);
  Expanded_List_Invariant(Implementation(SimulationImp))==(btrue);
  Context_List_Invariant(Implementation(SimulationImp))==(btrue);
  List_Invariant(Implementation(SimulationImp))==(btrue)
END
&
THEORY ListAssertionsX IS
  Abstract_List_Assertions(Implementation(SimulationImp))==(btrue);
  Expanded_List_Assertions(Implementation(SimulationImp))==(btrue);
  Context_List_Assertions(Implementation(SimulationImp))==(btrue);
  List_Assertions(Implementation(SimulationImp))==(btrue)
END
&
THEORY ListInitialisationX IS
  Expanded_List_Initialisation(Implementation(SimulationImp))==(skip);
  Context_List_Initialisation(Implementation(SimulationImp))==(skip);
  List_Initialisation(Implementation(SimulationImp))==(skip)
END
&
THEORY ListParametersX IS
  List_Parameters(Implementation(SimulationImp))==(?)
END
&
THEORY ListInstanciatedParametersX IS
  List_Instanciated_Parameters(Implementation(SimulationImp),Machine(BASIC_IO))==(?);
  List_Instanciated_Parameters(Implementation(SimulationImp),Machine(affichage))==(?);
  List_Instanciated_Parameters(Implementation(SimulationImp),Machine(TP3WinnieInterface))==(?)
END
&
THEORY ListConstraintsX IS
  List_Constraints(Implementation(SimulationImp),Machine(TP3WinnieInterface))==(btrue);
  List_Constraints(Implementation(SimulationImp))==(btrue);
  List_Context_Constraints(Implementation(SimulationImp))==(btrue);
  List_Constraints(Implementation(SimulationImp),Machine(affichage))==(btrue);
  List_Constraints(Implementation(SimulationImp),Machine(BASIC_IO))==(btrue)
END
&
THEORY ListOperationsX IS
  Internal_List_Operations(Implementation(SimulationImp))==(main);
  List_Operations(Implementation(SimulationImp))==(main)
END
&
THEORY ListInputX IS
  List_Input(Implementation(SimulationImp),main)==(?)
END
&
THEORY ListOutputX IS
  List_Output(Implementation(SimulationImp),main)==(?)
END
&
THEORY ListHeaderX IS
  List_Header(Implementation(SimulationImp),main)==(main)
END
&
THEORY ListPreconditionX IS
  Own_Precondition(Implementation(SimulationImp),main)==(btrue);
  List_Precondition(Implementation(SimulationImp),main)==(btrue)
END
&
THEORY ListSubstitutionX IS
  Expanded_List_Substitution(Implementation(SimulationImp),main)==(btrue | @(ch,ctr).(ch:=1;ctr:=MAXINT;WHILE ch/=0 & ctr>0 DO (ctr-1: INT & ctr: INT & 1: INT | ctr:=ctr-1);(btrue | skip);(3: NAT & 0: NAT & 0<=3 | @(bb$0).(bb$0: 0..3 ==> ch:=bb$0));(not(ch = 3) & not(ch = 2) & not(ch = 1) & ch = 0 ==> skip [] not(ch = 0) & not(ch = 3) & not(ch = 2) & ch = 1 ==> (btrue | skip) [] not(ch = 0) & not(ch = 1) & not(ch = 3) & ch = 2 ==> (btrue | skip) [] not(ch = 0) & not(ch = 1) & not(ch = 2) & ch = 3 ==> (btrue | skip) [] not(ch = 0) & not(ch = 1) & not(ch = 2) & not(ch = 3) ==> skip) INVARIANT ch: 0..3 & ctr: NAT VARIANT ctr END));
  List_Substitution(Implementation(SimulationImp),main)==(VAR ch,ctr IN ch:=1;ctr:=MAXINT;WHILE ch/=0 & ctr>0 DO ctr:=ctr-1;affichageMenu;ch <-- INTERVAL_READ(0,3);CASE ch OF EITHER 0 THEN skip OR 1 THEN XAjout_voiture OR 2 THEN XRetire_Voiture OR 3 THEN XNbLibre END END INVARIANT ch: 0..3 & ctr: NAT VARIANT ctr END END)
END
&
THEORY ListConstantsX IS
  List_Valuable_Constants(Implementation(SimulationImp))==(?);
  Inherited_List_Constants(Implementation(SimulationImp))==(?);
  List_Constants(Implementation(SimulationImp))==(?)
END
&
THEORY ListSetsX IS
  Context_List_Enumerated(Implementation(SimulationImp))==(?);
  Context_List_Defered(Implementation(SimulationImp))==(?);
  Context_List_Sets(Implementation(SimulationImp))==(?);
  List_Own_Enumerated(Implementation(SimulationImp))==(?);
  List_Valuable_Sets(Implementation(SimulationImp))==(?);
  Inherited_List_Enumerated(Implementation(SimulationImp))==(?);
  Inherited_List_Defered(Implementation(SimulationImp))==(?);
  Inherited_List_Sets(Implementation(SimulationImp))==(?);
  List_Enumerated(Implementation(SimulationImp))==(?);
  List_Defered(Implementation(SimulationImp))==(?);
  List_Sets(Implementation(SimulationImp))==(?)
END
&
THEORY ListHiddenConstantsX IS
  Abstract_List_HiddenConstants(Implementation(SimulationImp))==(?);
  Expanded_List_HiddenConstants(Implementation(SimulationImp))==(?);
  List_HiddenConstants(Implementation(SimulationImp))==(?);
  External_List_HiddenConstants(Implementation(SimulationImp))==(?)
END
&
THEORY ListPropertiesX IS
  Abstract_List_Properties(Implementation(SimulationImp))==(btrue);
  Context_List_Properties(Implementation(SimulationImp))==(btrue);
  Inherited_List_Properties(Implementation(SimulationImp))==(btrue);
  List_Properties(Implementation(SimulationImp))==(btrue)
END
&
THEORY ListValuesX IS
  Values_Subs(Implementation(SimulationImp))==(aa: aa);
  List_Values(Implementation(SimulationImp))==(?)
END
&
THEORY ListSeenInfoX END
&
THEORY ListIncludedOperationsX IS
  List_Included_Operations(Implementation(SimulationImp),Machine(TP3WinnieInterface))==(XAjout_voiture,XRetire_Voiture,XNbLibre,XNbVoitures);
  List_Included_Operations(Implementation(SimulationImp),Machine(affichage))==(affichageMenu);
  List_Included_Operations(Implementation(SimulationImp),Machine(BASIC_IO))==(INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE)
END
&
THEORY InheritedEnvX IS
  Operations(Implementation(SimulationImp))==(Type(main) == Cst(No_type,No_type))
END
&
THEORY ListVisibleStaticX END
&
THEORY ListOfIdsX IS
  List_Of_Ids(Implementation(SimulationImp)) == (? | ? | ? | ? | main | ? | imported(Machine(BASIC_IO)),imported(Machine(affichage)),imported(Machine(TP3WinnieInterface)) | ? | SimulationImp);
  List_Of_HiddenCst_Ids(Implementation(SimulationImp)) == (? | ?);
  List_Of_VisibleCst_Ids(Implementation(SimulationImp)) == (?);
  List_Of_VisibleVar_Ids(Implementation(SimulationImp)) == (? | ?);
  List_Of_Ids_SeenBNU(Implementation(SimulationImp)) == (?: ?);
  List_Of_Ids(Machine(TP3WinnieInterface)) == (? | ? | ? | ? | XAjout_voiture,XRetire_Voiture,XNbLibre,XNbVoitures | ? | ? | ? | TP3WinnieInterface);
  List_Of_HiddenCst_Ids(Machine(TP3WinnieInterface)) == (? | ?);
  List_Of_VisibleCst_Ids(Machine(TP3WinnieInterface)) == (?);
  List_Of_VisibleVar_Ids(Machine(TP3WinnieInterface)) == (? | ?);
  List_Of_Ids_SeenBNU(Machine(TP3WinnieInterface)) == (?: ?);
  List_Of_Ids(Machine(affichage)) == (? | ? | ? | ? | affichageMenu | ? | ? | ? | affichage);
  List_Of_HiddenCst_Ids(Machine(affichage)) == (? | ?);
  List_Of_VisibleCst_Ids(Machine(affichage)) == (?);
  List_Of_VisibleVar_Ids(Machine(affichage)) == (? | ?);
  List_Of_Ids_SeenBNU(Machine(affichage)) == (?: ?);
  List_Of_Ids(Machine(BASIC_IO)) == (? | ? | ? | ? | INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE | ? | ? | ? | BASIC_IO);
  List_Of_HiddenCst_Ids(Machine(BASIC_IO)) == (? | ?);
  List_Of_VisibleCst_Ids(Machine(BASIC_IO)) == (?);
  List_Of_VisibleVar_Ids(Machine(BASIC_IO)) == (? | ?);
  List_Of_Ids_SeenBNU(Machine(BASIC_IO)) == (?: ?)
END
&
THEORY VariablesLocEnvX IS
  Variables_Loc(Implementation(SimulationImp),main, 1) == (Type(ch) == Lvl(btype(INTEGER,?,?));Type(ctr) == 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(SimulationImp))==(?)
END
&
THEORY ListLocalInputX END
&
THEORY ListLocalOutputX END
&
THEORY ListLocalHeaderX END
&
THEORY ListLocalPreconditionX END
&
THEORY ListLocalSubstitutionX END
&
THEORY TypingPredicateX IS
  TypingPredicate(Implementation(SimulationImp))==(btrue)
END
&
THEORY ImportedVariablesListX IS
  ImportedVariablesList(Implementation(SimulationImp),Machine(BASIC_IO))==(?);
  ImportedVisVariablesList(Implementation(SimulationImp),Machine(BASIC_IO))==(?);
  ImportedVariablesList(Implementation(SimulationImp),Machine(affichage))==(?);
  ImportedVisVariablesList(Implementation(SimulationImp),Machine(affichage))==(?);
  ImportedVariablesList(Implementation(SimulationImp),Machine(TP3WinnieInterface))==(?);
  ImportedVisVariablesList(Implementation(SimulationImp),Machine(TP3WinnieInterface))==(?)
END
&
THEORY ListLocalOpInvariantX END
)