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