THEORY ProofList IS
  _f(1) & _f(20) & _f(76) & Supp_Stage.7,(_f(43) => _f(84));
  _f(1) & _f(20) & _f(76) & Supp_Stage.6,(_f(41) => _f(83));
  _f(1) & _f(20) & _f(76) & Supp_Stage.5,(_f(27) => _f(82));
  _f(1) & _f(20) & _f(76) & Supp_Stage.4,(_f(27) => _f(81));
  _f(1) & _f(20) & _f(76) & Supp_Stage.3,(_f(38) => _f(80));
  _f(1) & _f(20) & _f(76) & Supp_Stage.2,(_f(38) => _f(79));
  _f(1) & _f(20) & _f(76) & Supp_Stage.1,(_f(77) => _f(78));
  _f(1) & _f(20) & _f(69) & Ajout_Stage.6,(_f(43) => _f(75));
  _f(1) & _f(20) & _f(69) & Ajout_Stage.5,(_f(41) => _f(74));
  _f(1) & _f(20) & _f(69) & Ajout_Stage.4,(_f(27) => _f(73));
  _f(1) & _f(20) & _f(69) & Ajout_Stage.3,(_f(27) => _f(72));
  _f(1) & _f(20) & _f(69) & Ajout_Stage.2,(_f(38) => _f(71));
  _f(1) & _f(20) & _f(69) & Ajout_Stage.1,(_f(38) => _f(70));
  _f(1) & _f(20) & _f(66) & Desaffecte_Signataire.4,(_f(41) => _f(68));
  _f(1) & _f(20) & _f(66) & Desaffecte_Signataire.3,(_f(36) => _f(67));
  _f(1) & _f(20) & _f(66) & Desaffecte_Signataire.2,(_f(24) => _f(56));
  _f(1) & _f(20) & _f(66) & Desaffecte_Signataire.1,(_f(24) => _f(55));
  _f(1) & _f(20) & _f(62) & Affecte_Signataire.3,(_f(41) => _f(65));
  _f(1) & _f(20) & _f(62) & Affecte_Signataire.2,(_f(24) => _f(64));
  _f(1) & _f(20) & _f(62) & Affecte_Signataire.1,(_f(24) => _f(63));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.9,(_f(61) => _f(44));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.8,(_f(60) => _f(42));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.7,(_f(58) => _f(40));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.6,(_f(58) => _f(59));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.5,(_f(57) => _f(37));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.4,(_f(54) => _f(56));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.3,(_f(54) => _f(55));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.2,(_f(51) => _f(53));
  _f(1) & _f(20) & _f(50) & Desaffecte_Employe.1,(_f(51) => _f(52));
  _f(1) & _f(20) & _f(45) & Affecte_Employe.4,(_f(43) => _f(49));
  _f(1) & _f(20) & _f(45) & Affecte_Employe.3,(_f(36) => _f(48));
  _f(1) & _f(20) & _f(45) & Affecte_Employe.2,(_f(22) => _f(47));
  _f(1) & _f(20) & _f(45) & Affecte_Employe.1,(_f(22) => _f(46));
  _f(1) & _f(20) & _f(29) & Supp_Employe.10,(_f(43) => _f(44));
  _f(1) & _f(20) & _f(29) & Supp_Employe.9,(_f(41) => _f(42));
  _f(1) & _f(20) & _f(29) & Supp_Employe.8,(_f(38) => _f(40));
  _f(1) & _f(20) & _f(29) & Supp_Employe.7,(_f(38) => _f(39));
  _f(1) & _f(20) & _f(29) & Supp_Employe.6,(_f(36) => _f(37));
  _f(1) & _f(20) & _f(29) & Supp_Employe.5,(_f(24) => _f(35));
  _f(1) & _f(20) & _f(29) & Supp_Employe.4,(_f(24) => _f(34));
  _f(1) & _f(20) & _f(29) & Supp_Employe.3,(_f(22) => _f(33));
  _f(1) & _f(20) & _f(29) & Supp_Employe.2,(_f(22) => _f(32));
  _f(1) & _f(20) & _f(29) & Supp_Employe.1,(_f(30) => _f(31));
  _f(1) & _f(20) & _f(21) & Ajout_entreprise.4,(_f(27) => _f(28));
  _f(1) & _f(20) & _f(21) & Ajout_entreprise.3,(_f(24) => _f(26));
  _f(1) & _f(20) & _f(21) & Ajout_entreprise.2,(_f(24) => _f(25));
  _f(1) & _f(20) & _f(21) & Ajout_entreprise.1,(_f(22) => _f(23));
  _f(1) & Initialisation.9,(_f(18) => _f(19));
  _f(1) & Initialisation.8,(_f(16) => _f(17));
  _f(1) & Initialisation.7,(_f(14) => _f(15));
  _f(1) & Initialisation.6,(_f(12) => _f(13));
  _f(1) & Initialisation.5,(_f(10) => _f(11));
  _f(1) & Initialisation.4,(_f(8) => _f(9));
  _f(1) & Initialisation.3,(_f(6) => _f(7));
  _f(1) & Initialisation.2,(_f(4) => _f(5));
  _f(1) & Initialisation.1,(_f(2) => _f(3))
END
&
THEORY Formulas IS
  ("`Component properties'" & STAGE: FIN(INTEGER) & not(STAGE = {}) & ENTREPRISE: FIN(INTEGER) & not(ENTREPRISE = {}) & EMPLOYE: FIN(INTEGER) & not(EMPLOYE = {}));
  "`Check that the invariant (stage <: STAGE) is established by the initialisation - ref 3.3'";
  ({}: POW(STAGE));
  "`Check that the invariant (entreprise <: ENTREPRISE) is established by the initialisation - ref 3.3'";
  ({}: POW(ENTREPRISE));
  "`Check that the invariant (employe <: EMPLOYE) is established by the initialisation - ref 3.3'";
  ({}: POW(EMPLOYE));
  "`Check that the invariant (est_affecte: employe --> entreprise) is established by the initialisation - ref 3.3'" & "`Check that the invariant (est_signataire: employe >+> entreprise) is established by the initialisation - ref 3.3'" & "`Check that the invariant (a_pour_responsable: stage --> employe) is established by the initialisation - ref 3.3'" & "`Check that the invariant (est_propose: stage --> entreprise) is established by the initialisation - ref 3.3'";
  ({}: {} +-> {});
  "`Check that the invariant (est_affecte: employe --> entreprise) is established by the initialisation - ref 3.3'" & "`Check that the invariant (a_pour_responsable: stage --> employe) is established by the initialisation - ref 3.3'" & "`Check that the invariant (est_propose: stage --> entreprise) is established by the initialisation - ref 3.3'";
  (dom({}) = {});
  "`Check that the invariant (est_signataire: employe >+> entreprise) is established by the initialisation - ref 3.3'";
  ({}~: {} +-> {});
  "`Check that the invariant (est_signataire <: est_affecte) is established by the initialisation - ref 3.3'";
  ({}: POW({}));
  "`Check that the invariant (ran(a_pour_responsable)/\dom(est_signataire) = {}) is established by the initialisation - ref 3.3'";
  (ran({})/\dom({}) = {});
  "`Check that the invariant ((a_pour_responsable~;est_propose) <: est_affecte) is established by the initialisation - ref 3.3'";
  (({}~;{}): POW({}));
  ("`Component invariant'" & stage: POW(STAGE) & entreprise: POW(ENTREPRISE) & employe: POW(EMPLOYE) & est_affecte: employe +-> entreprise & dom(est_affecte) = employe & est_signataire: employe +-> entreprise & est_signataire~: entreprise +-> employe & est_signataire: POW(est_affecte) & a_pour_responsable: stage +-> employe & dom(a_pour_responsable) = stage & est_propose: stage +-> entreprise & dom(est_propose) = stage & ran(a_pour_responsable)/\dom(est_signataire) = {} & (a_pour_responsable~;est_propose): POW(est_affecte));
  ("`Ajout_entreprise preconditions in this component'" & ee: ENTREPRISE & not(ee: entreprise));
  "`Check that the invariant (est_affecte: employe --> entreprise) is preserved by the operation - ref 3.4'";
  (est_affecte: employe +-> entreprise\/{ee});
  "`Check that the invariant (est_signataire: employe >+> entreprise) is preserved by the operation - ref 3.4'";
  (est_signataire: employe +-> entreprise\/{ee});
  (est_signataire~: entreprise\/{ee} +-> employe);
  "`Check that the invariant (est_propose: stage --> entreprise) is preserved by the operation - ref 3.4'";
  (est_propose: stage +-> entreprise\/{ee});
  ("`Supp_Employe preconditions in this component'" & em: employe);
  "`Check that the invariant (employe <: EMPLOYE) is preserved by the operation - ref 3.4'";
  (employe-{em}: POW(EMPLOYE));
  ({em}<<|est_affecte: employe-{em} +-> entreprise);
  (dom({em}<<|est_affecte) = employe-{em});
  ({em}<<|est_signataire: employe-{em} +-> entreprise);
  (({em}<<|est_signataire)~: entreprise +-> employe-{em});
  "`Check that the invariant (est_signataire <: est_affecte) is preserved by the operation - ref 3.4'";
  ({em}<<|est_signataire: POW({em}<<|est_affecte));
  "`Check that the invariant (a_pour_responsable: stage --> employe) is preserved by the operation - ref 3.4'";
  (a_pour_responsable|>>{em}: stage +-> employe-{em});
  (dom(a_pour_responsable|>>{em}) = stage);
  "`Check that the invariant (ran(a_pour_responsable)/\dom(est_signataire) = {}) is preserved by the operation - ref 3.4'";
  (ran(a_pour_responsable|>>{em})/\dom({em}<<|est_signataire) = {});
  "`Check that the invariant ((a_pour_responsable~;est_propose) <: est_affecte) is preserved by the operation - ref 3.4'";
  (((a_pour_responsable|>>{em})~;est_propose): POW({em}<<|est_affecte));
  ("`Affecte_Employe preconditions in this component'" & em: employe & not(em: dom(est_affecte)) & en: entreprise);
  (est_affecte\/{em|->en}: employe +-> entreprise);
  (dom(est_affecte\/{em|->en}) = employe);
  (est_signataire: POW(est_affecte\/{em|->en}));
  ((a_pour_responsable~;est_propose): POW(est_affecte\/{em|->en}));
  ("`Desaffecte_Employe preconditions in this component'" & em: employe & em: dom(est_affecte));
  "`Check that the invariant (est_affecte: employe --> entreprise) is preserved by the operation - ref 3.4'";
  ({em}<<|est_affecte: employe +-> entreprise);
  (dom({em}<<|est_affecte) = employe);
  "`Check that the invariant (est_signataire: employe >+> entreprise) is preserved by the operation - ref 3.4'";
  ({em}<<|est_signataire: employe +-> entreprise);
  (({em}<<|est_signataire)~: entreprise +-> employe);
  "`Check that the invariant (est_signataire <: est_affecte) is preserved by the operation - ref 3.4'";
  "`Check that the invariant (a_pour_responsable: stage --> employe) is preserved by the operation - ref 3.4'";
  (a_pour_responsable|>>{em}: stage +-> employe);
  "`Check that the invariant (ran(a_pour_responsable)/\dom(est_signataire) = {}) is preserved by the operation - ref 3.4'";
  "`Check that the invariant ((a_pour_responsable~;est_propose) <: est_affecte) is preserved by the operation - ref 3.4'";
  ("`Affecte_Signataire preconditions in this component'" & em: employe & em: dom(est_affecte) & not(em: ran(a_pour_responsable)) & en: entreprise & em|->en: est_affecte & not(en: ran(est_signataire)));
  (est_signataire\/{em|->en}: employe +-> entreprise);
  ((est_signataire\/{em|->en})~: entreprise +-> employe);
  (ran(a_pour_responsable)/\dom(est_signataire\/{em|->en}) = {});
  ("`Desaffecte_Signataire preconditions in this component'" & em: employe & em: dom(est_affecte) & em: dom(est_signataire));
  ({em}<<|est_signataire: POW(est_affecte));
  (ran(a_pour_responsable)/\dom({em}<<|est_signataire) = {});
  ("`Ajout_Stage preconditions in this component'" & en: entreprise & em: employe & not(em: dom(est_signataire)) & em|->en: est_affecte & st: STAGE & not(st: dom(est_propose)));
  (a_pour_responsable\/{st|->em}: stage\/{st} +-> employe);
  (dom(a_pour_responsable\/{st|->em}) = stage\/{st});
  (est_propose\/{st|->en}: stage\/{st} +-> entreprise);
  (dom(est_propose\/{st|->en}) = stage\/{st});
  (ran(a_pour_responsable\/{st|->em})/\dom(est_signataire) = {});
  (((a_pour_responsable\/{st|->em})~;est_propose\/{st|->en}): POW(est_affecte));
  ("`Supp_Stage preconditions in this component'" & st: stage);
  "`Check that the invariant (stage <: STAGE) is preserved by the operation - ref 3.4'";
  (stage-{st}: POW(STAGE));
  ({st}<<|a_pour_responsable: stage-{st} +-> employe);
  (dom({st}<<|a_pour_responsable) = stage-{st});
  ({st}<<|est_propose: stage-{st} +-> entreprise);
  (dom({st}<<|est_propose) = stage-{st});
  (ran({st}<<|a_pour_responsable)/\dom(est_signataire) = {});
  ((({st}<<|a_pour_responsable)~;{st}<<|est_propose): POW(est_affecte))
END
&
THEORY EnumerateX 
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END