THEORY ProofList IS
  _f(3) & _f(7) & Retire_Voiture.1,(_f(5) => _f(8));
  _f(3) & _f(4) & Ajout_Voiture.1,(_f(5) => _f(6));
  Initialisation.1,(_f(1) => _f(2))
END
&
THEORY Formulas IS
  "`Check that the invariant (NbPlaces: 0..600) is established by the initialisation - ref 3.3'";
  (600: 0..600);
  ("`Component invariant'" & NbPlaces: 0..600);
  ("`Ajout_Voiture preconditions in this component'" & 1<=NbPlaces);
  "`Check that the invariant (NbPlaces: 0..600) is preserved by the operation - ref 3.4'";
  (NbPlaces-1: 0..600);
  ("`Retire_Voiture preconditions in this component'" & NbPlaces: 0..599);
  (NbPlaces+1: 0..600)
END
&
THEORY EnumerateX 
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END