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