THEORY ProofList
END
&
THEORY Formulas IS
  ("`XAjout_Voiture preconditions in this component'" & IdParking: 0..10);
  ("`XRetire_Voiture preconditions in this component'" & IdParking: 0..10);
  ("`XNbLibre preconditions in this component'" & IdParking: 0..10);
  ("`XNbVoitures 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