THEORY ProofList IS
  _f(1) & XNbVoitures.3,(_f(3) => _f(18));
  _f(1) & XNbVoitures.2,(_f(3) => _f(17));
  _f(1) & XNbVoitures.1,(_f(3) => _f(16));
  _f(1) & XNbLibre.3,(_f(3) => _f(15));
  _f(1) & XNbLibre.2,(_f(3) => _f(14));
  _f(1) & XNbLibre.1,(_f(3) => _f(13));
  _f(1) & XRetire_Voiture.3,(_f(11) & _f(3) => _f(12));
  _f(1) & XRetire_Voiture.2,(_f(8) & _f(3) => _f(10));
  _f(1) & XRetire_Voiture.1,(_f(8) & _f(3) => _f(9));
  _f(1) & XAjout_voiture.3,(_f(6) & _f(3) => _f(7));
  _f(1) & XAjout_voiture.2,(_f(2) & _f(3) => _f(5));
  _f(1) & XAjout_voiture.1,(_f(2) & _f(3) => _f(4))
END
&
THEORY Formulas IS
  ("`Included,imported and extended machines invariants'" & NbPlaces$1: 0..600);
  ("`Local hypotheses'" & 600-NbPlaces$1+1<=600);
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  (1<=NbPlaces$1);
  (" > Voiture ajoute": STRING);
  ("`Local hypotheses'" & not(600-NbPlaces$1+1<=600));
  (" > Parking de bananes !": STRING);
  ("`Local hypotheses'" & 1<=600-NbPlaces$1);
  (NbPlaces$1: 0..599);
  (" > Tartiflette retire": STRING);
  ("`Local hypotheses'" & not(1<=600-NbPlaces$1));
  (" > Parking vide !": STRING);
  (NbPlaces$1: INTEGER);
  (0<=NbPlaces$1);
  (NbPlaces$1<=2147483647);
  (600-NbPlaces$1: INTEGER);
  (0<=600-NbPlaces$1);
  (600-NbPlaces$1<=2147483647);
  ("`Variables conservation'" & NbPlaces = NbPlaces$1);
  ("`Included,imported and extended machines invariants'" & NbPlaces: 0..600)
END
&
THEORY EnumerateX 
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END