Normalised(
THEORY MagicNumberX IS
  MagicNumber(Machine(TestAgl))==(3.5)
END
&
THEORY UpperLevelX IS
  First_Level(Machine(TestAgl))==(Machine(TestAgl));
  Level(Machine(TestAgl))==(0)
END
&
THEORY LoadedStructureX IS
  Machine(TestAgl)
END
&
THEORY ListSeesX IS
  List_Sees(Machine(TestAgl))==(?)
END
&
THEORY ListUsesX IS
  List_Uses(Machine(TestAgl))==(?)
END
&
THEORY ListIncludesX IS
  Inherited_List_Includes(Machine(TestAgl))==(?);
  List_Includes(Machine(TestAgl))==(?)
END
&
THEORY ListPromotesX IS
  List_Promotes(Machine(TestAgl))==(?)
END
&
THEORY ListExtendsX IS
  List_Extends(Machine(TestAgl))==(?)
END
&
THEORY ListVariablesX IS
  External_Context_List_Variables(Machine(TestAgl))==(?);
  Context_List_Variables(Machine(TestAgl))==(?);
  Abstract_List_Variables(Machine(TestAgl))==(?);
  Local_List_Variables(Machine(TestAgl))==(est_propose,a_pour_responsable,est_signataire,est_affecte,employe,entreprise,stage);
  List_Variables(Machine(TestAgl))==(est_propose,a_pour_responsable,est_signataire,est_affecte,employe,entreprise,stage);
  External_List_Variables(Machine(TestAgl))==(est_propose,a_pour_responsable,est_signataire,est_affecte,employe,entreprise,stage)
END
&
THEORY ListVisibleVariablesX IS
  Inherited_List_VisibleVariables(Machine(TestAgl))==(?);
  Abstract_List_VisibleVariables(Machine(TestAgl))==(?);
  External_List_VisibleVariables(Machine(TestAgl))==(?);
  Expanded_List_VisibleVariables(Machine(TestAgl))==(?);
  List_VisibleVariables(Machine(TestAgl))==(?);
  Internal_List_VisibleVariables(Machine(TestAgl))==(?)
END
&
THEORY ListInvariantX IS
  Gluing_Seen_List_Invariant(Machine(TestAgl))==(btrue);
  Gluing_List_Invariant(Machine(TestAgl))==(btrue);
  Expanded_List_Invariant(Machine(TestAgl))==(btrue);
  Abstract_List_Invariant(Machine(TestAgl))==(btrue);
  Context_List_Invariant(Machine(TestAgl))==(btrue);
  List_Invariant(Machine(TestAgl))==(stage <: STAGE & entreprise <: ENTREPRISE & employe <: EMPLOYE & est_affecte: employe --> entreprise & est_signataire: employe >+> entreprise & est_signataire <: est_affecte & a_pour_responsable: stage --> employe & est_propose: stage --> entreprise & ran(a_pour_responsable)/\dom(est_signataire) = {} & (a_pour_responsable~;est_propose) <: est_affecte)
END
&
THEORY ListAssertionsX IS
  Expanded_List_Assertions(Machine(TestAgl))==(btrue);
  Abstract_List_Assertions(Machine(TestAgl))==(btrue);
  Context_List_Assertions(Machine(TestAgl))==(btrue);
  List_Assertions(Machine(TestAgl))==(btrue)
END
&
THEORY ListInitialisationX IS
  Expanded_List_Initialisation(Machine(TestAgl))==(stage,entreprise,employe,est_affecte,est_signataire,a_pour_responsable,est_propose:={},{},{},{},{},{},{});
  Context_List_Initialisation(Machine(TestAgl))==(skip);
  List_Initialisation(Machine(TestAgl))==(stage,entreprise,employe,est_affecte,est_signataire,a_pour_responsable,est_propose:={},{},{},{},{},{},{})
END
&
THEORY ListParametersX IS
  List_Parameters(Machine(TestAgl))==(?)
END
&
THEORY ListInstanciatedParametersX END
&
THEORY ListConstraintsX IS
  List_Context_Constraints(Machine(TestAgl))==(btrue);
  List_Constraints(Machine(TestAgl))==(btrue)
END
&
THEORY ListOperationsX IS
  Internal_List_Operations(Machine(TestAgl))==(Ajout_entreprise,Supp_Employe,Affecte_Employe,Desaffecte_Employe,Affecte_Signataire,Desaffecte_Signataire,Ajout_Stage,Supp_Stage);
  List_Operations(Machine(TestAgl))==(Ajout_entreprise,Supp_Employe,Affecte_Employe,Desaffecte_Employe,Affecte_Signataire,Desaffecte_Signataire,Ajout_Stage,Supp_Stage)
END
&
THEORY ListInputX IS
  List_Input(Machine(TestAgl),Ajout_entreprise)==(ee);
  List_Input(Machine(TestAgl),Supp_Employe)==(em);
  List_Input(Machine(TestAgl),Affecte_Employe)==(em,en);
  List_Input(Machine(TestAgl),Desaffecte_Employe)==(em);
  List_Input(Machine(TestAgl),Affecte_Signataire)==(em,en);
  List_Input(Machine(TestAgl),Desaffecte_Signataire)==(em);
  List_Input(Machine(TestAgl),Ajout_Stage)==(en,em,st);
  List_Input(Machine(TestAgl),Supp_Stage)==(st)
END
&
THEORY ListOutputX IS
  List_Output(Machine(TestAgl),Ajout_entreprise)==(?);
  List_Output(Machine(TestAgl),Supp_Employe)==(?);
  List_Output(Machine(TestAgl),Affecte_Employe)==(?);
  List_Output(Machine(TestAgl),Desaffecte_Employe)==(?);
  List_Output(Machine(TestAgl),Affecte_Signataire)==(?);
  List_Output(Machine(TestAgl),Desaffecte_Signataire)==(?);
  List_Output(Machine(TestAgl),Ajout_Stage)==(?);
  List_Output(Machine(TestAgl),Supp_Stage)==(?)
END
&
THEORY ListHeaderX IS
  List_Header(Machine(TestAgl),Ajout_entreprise)==(Ajout_entreprise(ee));
  List_Header(Machine(TestAgl),Supp_Employe)==(Supp_Employe(em));
  List_Header(Machine(TestAgl),Affecte_Employe)==(Affecte_Employe(em,en));
  List_Header(Machine(TestAgl),Desaffecte_Employe)==(Desaffecte_Employe(em));
  List_Header(Machine(TestAgl),Affecte_Signataire)==(Affecte_Signataire(em,en));
  List_Header(Machine(TestAgl),Desaffecte_Signataire)==(Desaffecte_Signataire(em));
  List_Header(Machine(TestAgl),Ajout_Stage)==(Ajout_Stage(en,em,st));
  List_Header(Machine(TestAgl),Supp_Stage)==(Supp_Stage(st))
END
&
THEORY ListPreconditionX IS
  List_Precondition(Machine(TestAgl),Ajout_entreprise)==(ee: ENTREPRISE-entreprise);
  List_Precondition(Machine(TestAgl),Supp_Employe)==(em: employe);
  List_Precondition(Machine(TestAgl),Affecte_Employe)==(em: employe & em/:dom(est_affecte) & en: entreprise);
  List_Precondition(Machine(TestAgl),Desaffecte_Employe)==(em: employe & em: dom(est_affecte));
  List_Precondition(Machine(TestAgl),Affecte_Signataire)==(em: employe & em: dom(est_affecte) & em/:ran(a_pour_responsable) & en: entreprise & {em|->en} <: est_affecte & en/:ran(est_signataire));
  List_Precondition(Machine(TestAgl),Desaffecte_Signataire)==(em: employe & em: dom(est_affecte) & em: dom(est_signataire));
  List_Precondition(Machine(TestAgl),Ajout_Stage)==(en: entreprise & em: employe & em/:dom(est_signataire) & {em|->en} <: est_affecte & st: STAGE & st/:dom(est_propose));
  List_Precondition(Machine(TestAgl),Supp_Stage)==(st: stage)
END
&
THEORY ListSubstitutionX IS
  Expanded_List_Substitution(Machine(TestAgl),Supp_Stage)==(st: stage | stage,a_pour_responsable,est_propose:=stage-{st},{st}<<|a_pour_responsable,{st}<<|est_propose);
  Expanded_List_Substitution(Machine(TestAgl),Ajout_Stage)==(en: entreprise & em: employe & em/:dom(est_signataire) & {em|->en} <: est_affecte & st: STAGE & st/:dom(est_propose) | stage,a_pour_responsable,est_propose:=stage\/{st},a_pour_responsable\/{st|->em},est_propose\/{st|->en});
  Expanded_List_Substitution(Machine(TestAgl),Desaffecte_Signataire)==(em: employe & em: dom(est_affecte) & em: dom(est_signataire) | est_signataire:={em}<<|est_signataire);
  Expanded_List_Substitution(Machine(TestAgl),Affecte_Signataire)==(em: employe & em: dom(est_affecte) & em/:ran(a_pour_responsable) & en: entreprise & {em|->en} <: est_affecte & en/:ran(est_signataire) | est_signataire:=est_signataire\/{em|->en});
  Expanded_List_Substitution(Machine(TestAgl),Desaffecte_Employe)==(em: employe & em: dom(est_affecte) | est_affecte,est_signataire,a_pour_responsable:={em}<<|est_affecte,{em}<<|est_signataire,a_pour_responsable|>>{em});
  Expanded_List_Substitution(Machine(TestAgl),Affecte_Employe)==(em: employe & em/:dom(est_affecte) & en: entreprise | est_affecte:=est_affecte\/{em|->en});
  Expanded_List_Substitution(Machine(TestAgl),Supp_Employe)==(em: employe | employe,est_affecte,est_signataire,a_pour_responsable:=employe-{em},{em}<<|est_affecte,{em}<<|est_signataire,a_pour_responsable|>>{em});
  Expanded_List_Substitution(Machine(TestAgl),Ajout_entreprise)==(ee: ENTREPRISE-entreprise | entreprise:=entreprise\/{ee});
  List_Substitution(Machine(TestAgl),Ajout_entreprise)==(entreprise:=entreprise\/{ee});
  List_Substitution(Machine(TestAgl),Supp_Employe)==(employe:=employe-{em} || est_affecte:={em}<<|est_affecte || est_signataire:={em}<<|est_signataire || a_pour_responsable:=a_pour_responsable|>>{em});
  List_Substitution(Machine(TestAgl),Affecte_Employe)==(est_affecte:=est_affecte\/{em|->en});
  List_Substitution(Machine(TestAgl),Desaffecte_Employe)==(est_affecte:={em}<<|est_affecte || est_signataire:={em}<<|est_signataire || a_pour_responsable:=a_pour_responsable|>>{em});
  List_Substitution(Machine(TestAgl),Affecte_Signataire)==(est_signataire:=est_signataire\/{em|->en});
  List_Substitution(Machine(TestAgl),Desaffecte_Signataire)==(est_signataire:={em}<<|est_signataire);
  List_Substitution(Machine(TestAgl),Ajout_Stage)==(stage:=stage\/{st} || a_pour_responsable:=a_pour_responsable\/{st|->em} || est_propose:=est_propose\/{st|->en});
  List_Substitution(Machine(TestAgl),Supp_Stage)==(stage:=stage-{st} || a_pour_responsable:={st}<<|a_pour_responsable || est_propose:={st}<<|est_propose)
END
&
THEORY ListConstantsX IS
  List_Valuable_Constants(Machine(TestAgl))==(?);
  Inherited_List_Constants(Machine(TestAgl))==(?);
  List_Constants(Machine(TestAgl))==(?)
END
&
THEORY ListSetsX IS
  Set_Definition(Machine(TestAgl),STAGE)==(?);
  Context_List_Enumerated(Machine(TestAgl))==(?);
  Context_List_Defered(Machine(TestAgl))==(?);
  Context_List_Sets(Machine(TestAgl))==(?);
  List_Valuable_Sets(Machine(TestAgl))==(STAGE,ENTREPRISE,EMPLOYE);
  Inherited_List_Enumerated(Machine(TestAgl))==(?);
  Inherited_List_Defered(Machine(TestAgl))==(?);
  Inherited_List_Sets(Machine(TestAgl))==(?);
  List_Enumerated(Machine(TestAgl))==(?);
  List_Defered(Machine(TestAgl))==(STAGE,ENTREPRISE,EMPLOYE);
  List_Sets(Machine(TestAgl))==(STAGE,ENTREPRISE,EMPLOYE);
  Set_Definition(Machine(TestAgl),ENTREPRISE)==(?);
  Set_Definition(Machine(TestAgl),EMPLOYE)==(?)
END
&
THEORY ListHiddenConstantsX IS
  Abstract_List_HiddenConstants(Machine(TestAgl))==(?);
  Expanded_List_HiddenConstants(Machine(TestAgl))==(?);
  List_HiddenConstants(Machine(TestAgl))==(?);
  External_List_HiddenConstants(Machine(TestAgl))==(?)
END
&
THEORY ListPropertiesX IS
  Abstract_List_Properties(Machine(TestAgl))==(btrue);
  Context_List_Properties(Machine(TestAgl))==(btrue);
  Inherited_List_Properties(Machine(TestAgl))==(btrue);
  List_Properties(Machine(TestAgl))==(STAGE: FIN(INTEGER) & not(STAGE = {}) & ENTREPRISE: FIN(INTEGER) & not(ENTREPRISE = {}) & EMPLOYE: FIN(INTEGER) & not(EMPLOYE = {}))
END
&
THEORY ListSeenInfoX END
&
THEORY ListOfIdsX IS
  List_Of_Ids(Machine(TestAgl)) == (STAGE,ENTREPRISE,EMPLOYE | ? | est_propose,a_pour_responsable,est_signataire,est_affecte,employe,entreprise,stage | ? | Ajout_entreprise,Supp_Employe,Affecte_Employe,Desaffecte_Employe,Affecte_Signataire,Desaffecte_Signataire,Ajout_Stage,Supp_Stage | ? | ? | ? | TestAgl);
  List_Of_HiddenCst_Ids(Machine(TestAgl)) == (? | ?);
  List_Of_VisibleCst_Ids(Machine(TestAgl)) == (?);
  List_Of_VisibleVar_Ids(Machine(TestAgl)) == (? | ?);
  List_Of_Ids_SeenBNU(Machine(TestAgl)) == (?: ?)
END
&
THEORY SetsEnvX IS
  Sets(Machine(TestAgl)) == (Type(STAGE) == Cst(SetOf(atype(STAGE,"[STAGE","]STAGE")));Type(ENTREPRISE) == Cst(SetOf(atype(ENTREPRISE,"[ENTREPRISE","]ENTREPRISE")));Type(EMPLOYE) == Cst(SetOf(atype(EMPLOYE,"[EMPLOYE","]EMPLOYE"))))
END
&
THEORY VariablesEnvX IS
  Variables(Machine(TestAgl)) == (Type(est_propose) == Mvl(SetOf(atype(STAGE,?,?)*atype(ENTREPRISE,?,?)));Type(a_pour_responsable) == Mvl(SetOf(atype(STAGE,?,?)*atype(EMPLOYE,?,?)));Type(est_signataire) == Mvl(SetOf(atype(EMPLOYE,?,?)*atype(ENTREPRISE,?,?)));Type(est_affecte) == Mvl(SetOf(atype(EMPLOYE,?,?)*atype(ENTREPRISE,?,?)));Type(employe) == Mvl(SetOf(atype(EMPLOYE,?,?)));Type(entreprise) == Mvl(SetOf(atype(ENTREPRISE,?,?)));Type(stage) == Mvl(SetOf(atype(STAGE,?,?))))
END
&
THEORY OperationsEnvX IS
  Operations(Machine(TestAgl)) == (Type(Supp_Stage) == Cst(No_type,atype(STAGE,?,?));Type(Ajout_Stage) == Cst(No_type,atype(ENTREPRISE,?,?)*atype(EMPLOYE,?,?)*atype(STAGE,?,?));Type(Desaffecte_Signataire) == Cst(No_type,atype(EMPLOYE,?,?));Type(Affecte_Signataire) == Cst(No_type,atype(EMPLOYE,?,?)*atype(ENTREPRISE,?,?));Type(Desaffecte_Employe) == Cst(No_type,atype(EMPLOYE,?,?));Type(Affecte_Employe) == Cst(No_type,atype(EMPLOYE,?,?)*atype(ENTREPRISE,?,?));Type(Supp_Employe) == Cst(No_type,atype(EMPLOYE,?,?));Type(Ajout_entreprise) == Cst(No_type,atype(ENTREPRISE,?,?)))
END
&
THEORY TCIntRdX IS
  predB0 == OK;
  extended_sees == KO;
  B0check_tab == KO;
  local_op == OK;
  abstract_constants_visible_in_values == KO
END
)