THEORY OPOBalanceX IS
  TP3WinnieInterfaceImp,23;
  ValuesLemmas,1;
  InstanciatedConstraintsLemmas,0;
  Initialisation,2;
  XAjout_Voiture,6;
  XRetire_Voiture,6;
  XNbLibre,4;
  XNbVoitures,4
END
&
THEORY OPOProofList IS
  _f(1) & _f(24) & XNbVoitures.4,(_f(25) & _of(11) => _of(2));
  _f(1) & _f(24) & XNbVoitures.3,(_of(17) & _of(3) => _of(8));
  _f(1) & _f(24) & XNbVoitures.2,(_of(17) & _of(3) => _of(2));
  _f(1) & _f(24) & XNbVoitures.1,(_of(6) => _of(2));
  _f(1) & _f(19) & XNbLibre.4,(_f(20) & _of(11) => _of(2));
  _f(1) & _f(19) & XNbLibre.3,(_of(16) & _of(3) => _of(8));
  _f(1) & _f(19) & XNbLibre.2,(_of(16) & _of(3) => _of(2));
  _f(1) & _f(19) & XNbLibre.1,(_of(6) => _of(2));
  _f(1) & _f(13) & XRetire_Voiture.6,(_f(17) & _of(12) => _of(2));
  _f(1) & _f(13) & XRetire_Voiture.5,(_of(15) & _of(11) => _of(2));
  _f(1) & _f(13) & XRetire_Voiture.4,(_of(14) & _of(3) => _of(8));
  _f(1) & _f(13) & XRetire_Voiture.3,(_of(13) & _of(3) => _of(8));
  _f(1) & _f(13) & XRetire_Voiture.2,(_of(13) & _of(3) => _of(2));
  _f(1) & _f(13) & XRetire_Voiture.1,(_of(6) => _of(2));
  _f(1) & _f(2) & XAjout_Voiture.6,(_f(10) & _of(12) => _of(2));
  _f(1) & _f(2) & XAjout_Voiture.5,(_of(10) & _of(11) => _of(2));
  _f(1) & _f(2) & XAjout_Voiture.4,(_of(9) & _of(3) => _of(8));
  _f(1) & _f(2) & XAjout_Voiture.3,(_of(7) & _of(3) => _of(8));
  _f(1) & _f(2) & XAjout_Voiture.2,(_of(7) & _of(3) => _of(2));
  _f(1) & _f(2) & XAjout_Voiture.1,(_of(6) => _of(2));
  _f(1) & Initialisation.2,(_of(4) & _of(5) => _of(2));
  _f(1) & Initialisation.1,(_of(3) => _of(2));
  ValuesLemmas.1,(_of(1) => _of(2))
END
&
THEORY OPOFormulas IS
  "`Check that the property (btrue) is preserved by the valuations - ref 5.2'";
  (btrue);
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  ("`Local hypotheses'" & TableParkings$0: 0..10 +-> 0..600 & dom(TableParkings$0) = 0..10);
  "`Check initialisation refinement - ref 4.3, 5.4'" & "`Check that the invariant (btrue) is established by the initialisation - ref 4.3, 5.4'";
  "`Check precondition (btrue) deduction'";
  ("`XAjout_Voiture preconditions in this component'" & IdParking: 0..10);
  (IdParking: 0..10);
  ("`XAjout_Voiture preconditions in this component'" & IdParking: 0..10 & "`Local hypotheses'" & 600-TableParkings$1(IdParking)+1<=600);
  ("`XAjout_Voiture preconditions in this component'" & IdParking: 0..10 & "`Local hypotheses'" & 600-TableParkings$1(IdParking)+1<=600 & TableParkings$1<+{IdParking|->TableParkings$1(IdParking)-1}: 0..10 +-> 0..600 & dom(TableParkings$1<+{IdParking|->TableParkings$1(IdParking)-1}) = 0..10);
  "`Check operation refinement - ref 4.4, 5.5'" & "`Check that the invariant (btrue) is preserved by the operation - ref 4.4, 5.5'";
  "`Check that the invariant (btrue) is preserved by the operation - ref 4.4, 5.5'" & "`Check that the invariant (btrue) is preserved by the operation - ref 4.4, 5.5'";
  ("`XRetire_Voiture preconditions in this component'" & IdParking: 0..10);
  ("`XRetire_Voiture preconditions in this component'" & IdParking: 0..10 & "`Local hypotheses'" & 1<=600-TableParkings$1(IdParking));
  ("`XRetire_Voiture preconditions in this component'" & IdParking: 0..10 & "`Local hypotheses'" & 1<=600-TableParkings$1(IdParking) & TableParkings$1<+{IdParking|->TableParkings$1(IdParking)+1}: 0..10 +-> 0..600 & dom(TableParkings$1<+{IdParking|->TableParkings$1(IdParking)+1}) = 0..10);
  ("`XNbLibre preconditions in this component'" & IdParking: 0..10);
  ("`XNbVoitures preconditions in this component'" & IdParking: 0..10)
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END