THEORY OPOBalanceX IS
  TP3WinnieInterfaceImp,17;
  ValuesLemmas,1;
  InstanciatedConstraintsLemmas,0;
  Initialisation,2;
  XAjout_voiture,4;
  XRetire_Voiture,4;
  XNbLibre,3;
  XNbVoitures,3
END
&
THEORY OPOProofList IS
  _f(1) & XNbVoitures.3,(_of(8) => _of(2));
  _f(1) & XNbVoitures.2,(_of(3) => _of(2));
  _f(1) & XNbVoitures.1,(_of(6) => _of(2));
  _f(1) & XNbLibre.3,(_of(8) => _of(2));
  _f(1) & XNbLibre.2,(_of(3) => _of(2));
  _f(1) & XNbLibre.1,(_of(6) => _of(2));
  _f(1) & XRetire_Voiture.4,(_f(11) & _of(9) => _of(2));
  _f(1) & XRetire_Voiture.3,(_of(10) & _of(8) => _of(2));
  _f(1) & XRetire_Voiture.2,(_of(3) => _of(2));
  _f(1) & XRetire_Voiture.1,(_of(6) => _of(2));
  _f(1) & XAjout_voiture.4,(_f(6) & _of(9) => _of(2));
  _f(1) & XAjout_voiture.3,(_of(7) & _of(8) => _of(2));
  _f(1) & XAjout_voiture.2,(_of(3) => _of(2));
  _f(1) & 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'" & 600: 0..600);
  "`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'";
  ("`Local hypotheses'" & 600-NbPlaces$1+1<=600 & NbPlaces$1-1: 0..600);
  "`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'";
  ("`Local hypotheses'" & 1<=600-NbPlaces$1 & NbPlaces$1+1: 0..600)
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END