THEORY OPOBalanceX IS
  TP3WinnieImp,25;
  ValuesLemmas,1;
  InstanciatedConstraintsLemmas,3;
  Initialisation,3;
  Ajout_Voiture,5;
  Retire_Voiture,5;
  Get_NbLibre,3;
  Get_NbVoitures,5
END
&
THEORY OPOProofList IS
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.5,(_f(47) & _of(21) => _of(22));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.4,(_f(47) & _of(14) => _of(24));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.3,(_of(23) & _of(14) => _of(16));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.2,(_of(23) & _of(14) => _of(2));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.1,(_of(12) => _of(2));
  _f(5) & _f(21) & _f(42) & Get_NbLibre.3,(_f(43) & _of(21) => _of(22));
  _f(5) & _f(21) & _f(42) & Get_NbLibre.2,(_of(20) & _of(14) => _of(2));
  _f(5) & _f(21) & _f(42) & Get_NbLibre.1,(_of(12) => _of(2));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.5,(_f(40) & _of(18) => _of(2));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.4,(_f(35) & _of(14) => _of(17));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.3,(_of(19) & _of(15) => _of(16));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.2,(_of(19) & _of(14) => _of(2));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.1,(_of(12) => _of(2));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.5,(_f(31) & _of(18) => _of(2));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.4,(_f(23) & _of(14) => _of(17));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.3,(_of(13) & _of(15) => _of(16));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.2,(_of(13) & _of(14) => _of(2));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.1,(_of(12) => _of(2));
  _f(5) & Initialisation.3,(_of(8) & _of(9) => _of(2));
  _f(5) & Initialisation.2,(_of(8) & _of(9) => _of(11));
  _f(5) & Initialisation.1,(_of(8) & _of(9) => _of(10));
  InstanciatedConstraintsLemmas.3,(_of(7) => _of(2));
  InstanciatedConstraintsLemmas.2,(_of(5) => _of(6));
  InstanciatedConstraintsLemmas.1,(_of(3) => _of(4));
  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 that the constraint (not(0..10 = {})) is preserved by the parameters instanciation - ref 3.1, 4.1, 5.1'";
  (not(0..10 = {}));
  "`Check that the constraint (not(0..600 = {})) is preserved by the parameters instanciation - ref 3.1, 4.1, 5.1'";
  (not(0..600 = {}));
  "`Check that the precondition (btrue) is preserved by the parameters instanciation'";
  ("`Local hypotheses'" & arr_vrb$0: 0..10 +-> 0..600 & dom(arr_vrb$0) = 0..10 & arr_vrb$0<+{0|->600}<+{1|->600}<+{2|->600}<+{3|->600}<+{4|->600}<+{5|->600}<+{6|->600}<+{7|->600}<+{8|->600}<+{9|->600}<+{10|->600}: 0..10 +-> 0..600 & dom(arr_vrb$0<+{0|->600}<+{1|->600}<+{2|->600}<+{3|->600}<+{4|->600}<+{5|->600}<+{6|->600}<+{7|->600}<+{8|->600}<+{9|->600}<+{10|->600}) = 0..10);
  "`Check initialisation refinement - ref 4.3, 5.4'";
  (arr_vrb$0<+{0|->600}<+{1|->600}<+{2|->600}<+{3|->600}<+{4|->600}<+{5|->600}<+{6|->600}<+{7|->600}<+{8|->600}<+{9|->600}<+{10|->600}: 0..10 +-> 0..600);
  (dom(arr_vrb$0<+{0|->600}<+{1|->600}<+{2|->600}<+{3|->600}<+{4|->600}<+{5|->600}<+{6|->600}<+{7|->600}<+{8|->600}<+{9|->600}<+{10|->600}) = 0..10);
  "`Check precondition (btrue) deduction'";
  ("`Ajout_Voiture preconditions in this component'" & IdParking: 0..10 & 1<=TableParkings(IdParking));
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'" & "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  (IdParking: 0..10);
  (1: INT);
  "`Check that the invariant (C_TableParkingsarr_vrb = TableParkings) is preserved by the operation - ref 4.4, 5.5'" & "`Check operation refinement - ref 4.4, 5.5'";
  ("`Retire_Voiture preconditions in this component'" & IdParking: 0..10 & TableParkings(IdParking): 0..599);
  ("`Get_NbLibre preconditions in this component'" & IdParking: 0..10);
  "`Check that the invariant (C_TableParkingsarr_vrb = TableParkings) is preserved by the operation - ref 4.4, 5.5'";
  (C_TableParkingsarr_vrb$1 = TableParkings);
  ("`Get_NbVoitures preconditions in this component'" & IdParking: 0..10);
  (600: INT)
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END