THEORY ProofList IS
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.7,(_f(47) & _f(51) => _f(52));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.6,(_f(47) & _f(7) => _f(29));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.5,(_f(47) & _f(7) => _f(28));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.4,(_f(47) & _f(7) => _f(27));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.3,(_f(47) & _f(7) => _f(50));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.2,(_f(47) & _f(7) => _f(49));
  _f(5) & _f(21) & _f(46) & Get_NbVoitures.1,(_f(47) & _f(7) => _f(48));
  _f(5) & _f(21) & _f(42) & Get_NbLibre.1,(_f(43) & _f(44) => _f(45));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.8,(_f(40) & _f(32) => _f(41));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.7,(_f(35) & _f(7) => _f(39));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.6,(_f(35) & _f(7) => _f(29));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.5,(_f(35) & _f(7) => _f(28));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.4,(_f(35) & _f(7) => _f(27));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.3,(_f(35) & _f(7) => _f(38));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.2,(_f(35) & _f(7) => _f(37));
  _f(5) & _f(21) & _f(34) & Retire_Voiture.1,(_f(35) & _f(7) => _f(36));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.8,(_f(31) & _f(32) => _f(33));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.7,(_f(23) & _f(7) => _f(30));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.6,(_f(23) & _f(7) => _f(29));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.5,(_f(23) & _f(7) => _f(28));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.4,(_f(23) & _f(7) => _f(27));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.3,(_f(23) & _f(7) => _f(26));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.2,(_f(23) & _f(7) => _f(25));
  _f(5) & _f(21) & _f(22) & Ajout_Voiture.1,(_f(23) & _f(7) => _f(24));
  _f(5) & Initialisation.12,(_f(6) & _f(7) => _f(20));
  _f(5) & Initialisation.11,(_f(6) & _f(7) => _f(19));
  _f(5) & Initialisation.10,(_f(6) & _f(7) => _f(18));
  _f(5) & Initialisation.9,(_f(6) & _f(7) => _f(17));
  _f(5) & Initialisation.8,(_f(6) & _f(7) => _f(16));
  _f(5) & Initialisation.7,(_f(6) & _f(7) => _f(15));
  _f(5) & Initialisation.6,(_f(6) & _f(7) => _f(14));
  _f(5) & Initialisation.5,(_f(6) & _f(7) => _f(13));
  _f(5) & Initialisation.4,(_f(6) & _f(7) => _f(12));
  _f(5) & Initialisation.3,(_f(6) & _f(7) => _f(11));
  _f(5) & Initialisation.2,(_f(6) & _f(9) => _f(10));
  _f(5) & Initialisation.1,(_f(6) & _f(7) => _f(8));
  InstanciatedConstraintsLemmas.2,(_f(3) => _f(4));
  InstanciatedConstraintsLemmas.1,(_f(1) => _f(2))
END
&
THEORY Formulas IS
  "`Check that the constraint (0..10: FIN(INTEGER)) is preserved by the parameters instanciation - ref 3.1, 4.1, 5.1'";
  (0..10: FIN(INTEGER));
  "`Check that the constraint (0..600: FIN(INTEGER)) is preserved by the parameters instanciation - ref 3.1, 4.1, 5.1'";
  (0..600: FIN(INTEGER));
  ("`Included,imported and extended machines invariants'" & C_TableParkingsarr_vrb$1: 0..10 +-> 0..600 & dom(C_TableParkingsarr_vrb$1) = 0..10);
  ("`Local hypotheses'" & arr_vrb$0: 0..10 +-> 0..600 & dom(arr_vrb$0) = 0..10);
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  (0: 0..10);
  "`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'" & "`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'" & "`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'" & "`Check preconditions of called operation, or While loop construction, or Assert predicates'" & "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  (600: 0..600);
  (1: 0..10);
  (2: 0..10);
  (3: 0..10);
  (4: 0..10);
  (5: 0..10);
  (6: 0..10);
  (7: 0..10);
  (8: 0..10);
  (9: 0..10);
  (10: 0..10);
  ("`Previous components invariants'" & TableParkings: 0..10 +-> 0..600 & dom(TableParkings) = 0..10 & "`Component invariant'" & C_TableParkingsarr_vrb$1 = TableParkings);
  ("`Ajout_Voiture preconditions in previous components'" & IdParking: 0..10 & 1<=TableParkings(IdParking));
  ("`Ajout_Voiture preconditions in this component'" & IdParking: 0..10 & 1<=TableParkings(IdParking));
  (C_TableParkingsarr_vrb$1(IdParking)-1: INTEGER);
  (C_TableParkingsarr_vrb$1(IdParking)-1<=2147483647);
  (-2147483647<=C_TableParkingsarr_vrb$1(IdParking)-1);
  (C_TableParkingsarr_vrb$1(IdParking): INTEGER);
  (C_TableParkingsarr_vrb$1(IdParking)<=2147483647);
  (-2147483647<=C_TableParkingsarr_vrb$1(IdParking));
  (C_TableParkingsarr_vrb$1(IdParking)-1: 0..600);
  ("`Ajout_Voiture preconditions in this component'" & IdParking: 0..10 & 1<=TableParkings(IdParking) & "`Local hypotheses'" & C_TableParkingsarr_vrb$1<+{IdParking|->C_TableParkingsarr_vrb$1(IdParking)-1}: 0..10 +-> 0..600 & dom(C_TableParkingsarr_vrb$1<+{IdParking|->C_TableParkingsarr_vrb$1(IdParking)-1}) = 0..10);
  "`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'";
  (C_TableParkingsarr_vrb$1<+{IdParking|->C_TableParkingsarr_vrb$1(IdParking)-1} = TableParkings<+{IdParking|->TableParkings(IdParking)-1});
  ("`Retire_Voiture preconditions in previous components'" & IdParking: 0..10 & TableParkings(IdParking): 0..599);
  ("`Retire_Voiture preconditions in this component'" & IdParking: 0..10 & TableParkings(IdParking): 0..599);
  (C_TableParkingsarr_vrb$1(IdParking)+1: INTEGER);
  (C_TableParkingsarr_vrb$1(IdParking)+1<=2147483647);
  (-2147483647<=C_TableParkingsarr_vrb$1(IdParking)+1);
  (C_TableParkingsarr_vrb$1(IdParking)+1: 0..600);
  ("`Retire_Voiture preconditions in this component'" & IdParking: 0..10 & TableParkings(IdParking): 0..599 & "`Local hypotheses'" & C_TableParkingsarr_vrb$1<+{IdParking|->C_TableParkingsarr_vrb$1(IdParking)+1}: 0..10 +-> 0..600 & dom(C_TableParkingsarr_vrb$1<+{IdParking|->C_TableParkingsarr_vrb$1(IdParking)+1}) = 0..10);
  (C_TableParkingsarr_vrb$1<+{IdParking|->C_TableParkingsarr_vrb$1(IdParking)+1} = TableParkings<+{IdParking|->TableParkings(IdParking)+1});
  ("`Get_NbLibre preconditions in previous components'" & IdParking: 0..10);
  ("`Get_NbLibre preconditions in this component'" & IdParking: 0..10);
  "`Check that the invariant (NbLibre$1 = NbLibre) is preserved by the operation - ref 4.4, 5.5'" & "`Check operation refinement - ref 4.4, 5.5'";
  (C_TableParkingsarr_vrb$1(IdParking) = TableParkings(IdParking));
  ("`Get_NbVoitures preconditions in previous components'" & IdParking: 0..10);
  ("`Get_NbVoitures preconditions in this component'" & IdParking: 0..10);
  (600-C_TableParkingsarr_vrb$1(IdParking): INTEGER);
  (600-C_TableParkingsarr_vrb$1(IdParking)<=2147483647);
  (-2147483647<=600-C_TableParkingsarr_vrb$1(IdParking));
  "`Check that the invariant (NbVoitures$1 = NbVoitures) is preserved by the operation - ref 4.4, 5.5'" & "`Check operation refinement - ref 4.4, 5.5'";
  (600-C_TableParkingsarr_vrb$1(IdParking) = 600-TableParkings(IdParking));
  ("`Variables conservation'" & C_TableParkingsarr_vrb = C_TableParkingsarr_vrb$1);
  ("`Included,imported and extended machines invariants'" & C_TableParkingsarr_vrb: 0..10 +-> 0..600 & dom(C_TableParkingsarr_vrb) = 0..10)
END
&
THEORY EnumerateX 
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END