THEORY ProofList IS
  _f(3) & Get_NbVoitures.7,(_f(24) => _f(25));
  _f(3) & Get_NbVoitures.6,(_f(6) => _f(12));
  _f(3) & Get_NbVoitures.5,(_f(6) => _f(11));
  _f(3) & Get_NbVoitures.4,(_f(6) => _f(10));
  _f(3) & Get_NbVoitures.3,(_f(6) => _f(23));
  _f(3) & Get_NbVoitures.2,(_f(6) => _f(22));
  _f(3) & Get_NbVoitures.1,(_f(6) => _f(21));
  _f(3) & Get_NbLibre.3,(_f(6) => _f(12));
  _f(3) & Get_NbLibre.2,(_f(6) => _f(11));
  _f(3) & Get_NbLibre.1,(_f(6) => _f(10));
  _f(3) & _f(15) & Retire_Voiture.7,(_f(16) & _f(13) => _f(20));
  _f(3) & _f(15) & Retire_Voiture.6,(_f(16) & _f(6) => _f(12));
  _f(3) & _f(15) & Retire_Voiture.5,(_f(16) & _f(6) => _f(11));
  _f(3) & _f(15) & Retire_Voiture.4,(_f(16) & _f(6) => _f(10));
  _f(3) & _f(15) & Retire_Voiture.3,(_f(16) & _f(6) => _f(19));
  _f(3) & _f(15) & Retire_Voiture.2,(_f(16) & _f(6) => _f(18));
  _f(3) & _f(15) & Retire_Voiture.1,(_f(16) & _f(6) => _f(17));
  _f(3) & _f(4) & Ajout_Voiture.7,(_f(5) & _f(13) => _f(14));
  _f(3) & _f(4) & Ajout_Voiture.6,(_f(5) & _f(6) => _f(12));
  _f(3) & _f(4) & Ajout_Voiture.5,(_f(5) & _f(6) => _f(11));
  _f(3) & _f(4) & Ajout_Voiture.4,(_f(5) & _f(6) => _f(10));
  _f(3) & _f(4) & Ajout_Voiture.3,(_f(5) & _f(6) => _f(9));
  _f(3) & _f(4) & Ajout_Voiture.2,(_f(5) & _f(6) => _f(8));
  _f(3) & _f(4) & Ajout_Voiture.1,(_f(5) & _f(6) => _f(7));
  Initialisation.1,(_f(1) => _f(2))
END
&
THEORY Formulas IS
  "`Check that the invariant (C_NbPlaces: 0..600) is established by the initialisation - ref 4.3, 5.4'";
  (600: 0..600);
  ("`Previous components invariants'" & NbPlaces: 0..600 & "`Component invariant'" & C_NbPlaces$1: 0..600 & C_NbPlaces$1 = NbPlaces);
  ("`Ajout_Voiture preconditions in previous components'" & 1<=NbPlaces);
  ("`Ajout_Voiture preconditions in this component'" & 1<=NbPlaces);
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  (C_NbPlaces$1-1: INTEGER);
  (C_NbPlaces$1-1<=2147483647);
  (-2147483647<=C_NbPlaces$1-1);
  (C_NbPlaces$1: INTEGER);
  (C_NbPlaces$1<=2147483647);
  (-2147483647<=C_NbPlaces$1);
  "`Check that the invariant (C_NbPlaces: 0..600) is preserved by the operation - ref 4.4, 5.5'";
  (C_NbPlaces$1-1: 0..600);
  ("`Retire_Voiture preconditions in previous components'" & NbPlaces: 0..599);
  ("`Retire_Voiture preconditions in this component'" & NbPlaces: 0..599);
  (C_NbPlaces$1+1: INTEGER);
  (C_NbPlaces$1+1<=2147483647);
  (-2147483647<=C_NbPlaces$1+1);
  (C_NbPlaces$1+1: 0..600);
  (600-C_NbPlaces$1: INTEGER);
  (600-C_NbPlaces$1<=2147483647);
  (-2147483647<=600-C_NbPlaces$1);
  "`Check that the invariant (NbVoitures$1 = NbVoitures) is preserved by the operation - ref 4.4, 5.5'" & "`Check operation refinement - ref 4.4, 5.5'";
  (600-C_NbPlaces$1 = 600-NbPlaces);
  ("`Concrete variables typing predicates'" & C_NbPlaces$1: INTEGER & "`Variables conservation'" & C_NbPlaces = C_NbPlaces$1);
  ("`Concrete variables typing predicates'" & C_NbPlaces: INTEGER)
END
&
THEORY EnumerateX 
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END