Normalised(
THEORY MagicNumberX IS
  MagicNumber(Implementation(affichage_imp))==(3.5)
END
&
THEORY UpperLevelX IS
  First_Level(Implementation(affichage_imp))==(Machine(affichage));
  Level(Implementation(affichage_imp))==(1);
  Upper_Level(Implementation(affichage_imp))==(Machine(affichage))
END
&
THEORY LoadedStructureX IS
  Implementation(affichage_imp)
END
&
THEORY ListSeesX IS
  List_Sees(Implementation(affichage_imp))==(BASIC_IO)
END
&
THEORY ListIncludesX IS
  List_Includes(Implementation(affichage_imp))==(?);
  Inherited_List_Includes(Implementation(affichage_imp))==(?)
END
&
THEORY ListPromotesX IS
  List_Promotes(Implementation(affichage_imp))==(?)
END
&
THEORY ListExtendsX IS
  List_Extends(Implementation(affichage_imp))==(?)
END
&
THEORY ListVariablesX IS
  External_Context_List_Variables(Implementation(affichage_imp))==(?);
  Context_List_Variables(Implementation(affichage_imp))==(?);
  Abstract_List_Variables(Implementation(affichage_imp))==(?);
  Local_List_Variables(Implementation(affichage_imp))==(?);
  List_Variables(Implementation(affichage_imp))==(?);
  External_List_Variables(Implementation(affichage_imp))==(?)
END
&
THEORY ListVisibleVariablesX IS
  Inherited_List_VisibleVariables(Implementation(affichage_imp))==(?);
  Abstract_List_VisibleVariables(Implementation(affichage_imp))==(?);
  External_List_VisibleVariables(Implementation(affichage_imp))==(?);
  Expanded_List_VisibleVariables(Implementation(affichage_imp))==(?);
  List_VisibleVariables(Implementation(affichage_imp))==(?);
  Internal_List_VisibleVariables(Implementation(affichage_imp))==(?)
END
&
THEORY ListInvariantX IS
  Gluing_Seen_List_Invariant(Implementation(affichage_imp))==(btrue);
  Expanded_List_Invariant(Implementation(affichage_imp))==(btrue);
  Abstract_List_Invariant(Implementation(affichage_imp))==(btrue);
  Context_List_Invariant(Implementation(affichage_imp))==(btrue);
  List_Invariant(Implementation(affichage_imp))==(btrue)
END
&
THEORY ListAssertionsX IS
  Expanded_List_Assertions(Implementation(affichage_imp))==(btrue);
  Abstract_List_Assertions(Implementation(affichage_imp))==(btrue);
  Context_List_Assertions(Implementation(affichage_imp))==(btrue);
  List_Assertions(Implementation(affichage_imp))==(btrue)
END
&
THEORY ListInitialisationX IS
  Expanded_List_Initialisation(Implementation(affichage_imp))==(skip);
  Context_List_Initialisation(Implementation(affichage_imp))==(skip);
  List_Initialisation(Implementation(affichage_imp))==(skip)
END
&
THEORY ListParametersX IS
  List_Parameters(Implementation(affichage_imp))==(?)
END
&
THEORY ListInstanciatedParametersX IS
  List_Instanciated_Parameters(Implementation(affichage_imp),Machine(BASIC_IO))==(?)
END
&
THEORY ListConstraintsX IS
  List_Constraints(Implementation(affichage_imp))==(btrue);
  List_Context_Constraints(Implementation(affichage_imp))==(btrue)
END
&
THEORY ListOperationsX IS
  Internal_List_Operations(Implementation(affichage_imp))==(affichageMenu);
  List_Operations(Implementation(affichage_imp))==(affichageMenu)
END
&
THEORY ListInputX IS
  List_Input(Implementation(affichage_imp),affichageMenu)==(?)
END
&
THEORY ListOutputX IS
  List_Output(Implementation(affichage_imp),affichageMenu)==(?)
END
&
THEORY ListHeaderX IS
  List_Header(Implementation(affichage_imp),affichageMenu)==(affichageMenu)
END
&
THEORY ListPreconditionX IS
  Own_Precondition(Implementation(affichage_imp),affichageMenu)==(btrue);
  List_Precondition(Implementation(affichage_imp),affichageMenu)==(btrue)
END
&
THEORY ListSubstitutionX IS
  Expanded_List_Substitution(Implementation(affichage_imp),affichageMenu)==(btrue | ("\n----- MENU -----\n": STRING | skip);("1. Entre d'une voiture\n": STRING | skip);("2. Sortie d'une voiture\n": STRING | skip);("3. Nombre de places libres\n": STRING | skip));
  List_Substitution(Implementation(affichage_imp),affichageMenu)==(STRING_WRITE("\n----- MENU -----\n");STRING_WRITE("1. Entre d'une voiture\n");STRING_WRITE("2. Sortie d'une voiture\n");STRING_WRITE("3. Nombre de places libres\n"))
END
&
THEORY ListConstantsX IS
  List_Valuable_Constants(Implementation(affichage_imp))==(?);
  Inherited_List_Constants(Implementation(affichage_imp))==(?);
  List_Constants(Implementation(affichage_imp))==(?)
END
&
THEORY ListSetsX IS
  Context_List_Enumerated(Implementation(affichage_imp))==(?);
  Context_List_Defered(Implementation(affichage_imp))==(?);
  Context_List_Sets(Implementation(affichage_imp))==(?);
  List_Own_Enumerated(Implementation(affichage_imp))==(?);
  List_Valuable_Sets(Implementation(affichage_imp))==(?);
  Inherited_List_Enumerated(Implementation(affichage_imp))==(?);
  Inherited_List_Defered(Implementation(affichage_imp))==(?);
  Inherited_List_Sets(Implementation(affichage_imp))==(?);
  List_Enumerated(Implementation(affichage_imp))==(?);
  List_Defered(Implementation(affichage_imp))==(?);
  List_Sets(Implementation(affichage_imp))==(?)
END
&
THEORY ListHiddenConstantsX IS
  Abstract_List_HiddenConstants(Implementation(affichage_imp))==(?);
  Expanded_List_HiddenConstants(Implementation(affichage_imp))==(?);
  List_HiddenConstants(Implementation(affichage_imp))==(?);
  External_List_HiddenConstants(Implementation(affichage_imp))==(?)
END
&
THEORY ListPropertiesX IS
  Abstract_List_Properties(Implementation(affichage_imp))==(btrue);
  Context_List_Properties(Implementation(affichage_imp))==(btrue);
  Inherited_List_Properties(Implementation(affichage_imp))==(btrue);
  List_Properties(Implementation(affichage_imp))==(btrue)
END
&
THEORY ListValuesX IS
  Values_Subs(Implementation(affichage_imp))==(aa: aa);
  List_Values(Implementation(affichage_imp))==(?)
END
&
THEORY ListSeenInfoX IS
  Seen_Internal_List_Operations(Implementation(affichage_imp),Machine(BASIC_IO))==(INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE);
  Seen_Context_List_Enumerated(Implementation(affichage_imp))==(?);
  Seen_Context_List_Invariant(Implementation(affichage_imp))==(btrue);
  Seen_Context_List_Assertions(Implementation(affichage_imp))==(btrue);
  Seen_Context_List_Properties(Implementation(affichage_imp))==(btrue);
  Seen_List_Constraints(Implementation(affichage_imp))==(btrue);
  Seen_List_Precondition(Implementation(affichage_imp),STRING_WRITE)==(ss: STRING);
  Seen_Expanded_List_Substitution(Implementation(affichage_imp),STRING_WRITE)==(skip);
  Seen_List_Precondition(Implementation(affichage_imp),CHAR_WRITE)==(cc: 0..255);
  Seen_Expanded_List_Substitution(Implementation(affichage_imp),CHAR_WRITE)==(skip);
  Seen_List_Precondition(Implementation(affichage_imp),CHAR_READ)==(btrue);
  Seen_Expanded_List_Substitution(Implementation(affichage_imp),CHAR_READ)==(@(cc$0).(cc$0: 0..255 ==> cc:=cc$0));
  Seen_List_Precondition(Implementation(affichage_imp),BOOL_WRITE)==(bb: BOOL);
  Seen_Expanded_List_Substitution(Implementation(affichage_imp),BOOL_WRITE)==(skip);
  Seen_List_Precondition(Implementation(affichage_imp),BOOL_READ)==(btrue);
  Seen_Expanded_List_Substitution(Implementation(affichage_imp),BOOL_READ)==(@(bb$0).(bb$0: BOOL ==> bb:=bb$0));
  Seen_List_Precondition(Implementation(affichage_imp),INT_WRITE)==(vv: NAT);
  Seen_Expanded_List_Substitution(Implementation(affichage_imp),INT_WRITE)==(skip);
  Seen_List_Precondition(Implementation(affichage_imp),INTERVAL_READ)==(nn: NAT & mm: NAT & mm<=nn);
  Seen_Expanded_List_Substitution(Implementation(affichage_imp),INTERVAL_READ)==(@(bb$0).(bb$0: mm..nn ==> bb:=bb$0));
  Seen_List_Operations(Implementation(affichage_imp),Machine(BASIC_IO))==(INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE);
  Seen_Expanded_List_Invariant(Implementation(affichage_imp),Machine(BASIC_IO))==(btrue)
END
&
THEORY ListIncludedOperationsX IS
  List_Included_Operations(Implementation(affichage_imp),Machine(BASIC_IO))==(INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE)
END
&
THEORY InheritedEnvX IS
  Operations(Implementation(affichage_imp))==(Type(affichageMenu) == Cst(No_type,No_type))
END
&
THEORY ListVisibleStaticX END
&
THEORY ListOfIdsX IS
  List_Of_Ids(Implementation(affichage_imp)) == (? | ? | ? | ? | affichageMenu | ? | seen(Machine(BASIC_IO)) | ? | affichage_imp);
  List_Of_HiddenCst_Ids(Implementation(affichage_imp)) == (? | ?);
  List_Of_VisibleCst_Ids(Implementation(affichage_imp)) == (?);
  List_Of_VisibleVar_Ids(Implementation(affichage_imp)) == (? | ?);
  List_Of_Ids_SeenBNU(Implementation(affichage_imp)) == (?: ?);
  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 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(affichage_imp))==(?)
END
&
THEORY ListLocalInputX END
&
THEORY ListLocalOutputX END
&
THEORY ListLocalHeaderX END
&
THEORY ListLocalPreconditionX END
&
THEORY ListLocalSubstitutionX END
&
THEORY TypingPredicateX IS
  TypingPredicate(Implementation(affichage_imp))==(btrue)
END
&
THEORY ImportedVariablesListX END
&
THEORY ListLocalOpInvariantX END
)