THEORY ProofList IS
  btrue & affichageMenuParkings.11,(_f(1) => _f(19));
  btrue & affichageMenuParkings.10,(_f(1) => _f(18));
  btrue & affichageMenuParkings.9,(_f(1) => _f(17));
  btrue & affichageMenuParkings.8,(_f(1) => _f(16));
  btrue & affichageMenuParkings.7,(_f(1) => _f(15));
  btrue & affichageMenuParkings.6,(_f(1) => _f(14));
  btrue & affichageMenuParkings.5,(_f(1) => _f(13));
  btrue & affichageMenuParkings.4,(_f(1) => _f(12));
  btrue & affichageMenuParkings.3,(_f(1) => _f(11));
  btrue & affichageMenuParkings.2,(_f(1) => _f(10));
  btrue & affichageMenuParkings.1,(_f(1) => _f(9));
  btrue & affichageMenu.7,(_f(1) => _f(8));
  btrue & affichageMenu.6,(_f(1) => _f(7));
  btrue & affichageMenu.5,(_f(1) => _f(6));
  btrue & affichageMenu.4,(_f(1) => _f(5));
  btrue & affichageMenu.3,(_f(1) => _f(4));
  btrue & affichageMenu.2,(_f(1) => _f(3));
  btrue & affichageMenu.1,(_f(1) => _f(2))
END
&
THEORY Formulas IS
  "`Check preconditions of called operation, or While loop construction, or Assert predicates'";
  ("\n----- MENU -----\n": STRING);
  ("1. Entre d'une voiture\n": STRING);
  ("2. Sortie d'une voiture\n": STRING);
  ("3. Nombre de places libres\n": STRING);
  ("4. Changer de parking\n": STRING);
  ("\n": STRING);
  ("0. Quitter\n": STRING);
  ("1. Commerce\n": STRING);
  ("2. Talensac\n": STRING);
  ("3. Bretagne\n": STRING);
  ("4. Chanzy Park\n": STRING);
  ("5. Ikea Park\n": STRING);
  ("6. Leclerc Park\n": STRING);
  ("7. Auto Park\n": STRING);
  ("8. SuperParking\n": STRING);
  ("9. Parking 2000\n": STRING);
  ("10.Park Matic\n": STRING);
  ("11.Toto Park\n\n": STRING)
END
&
THEORY EnumerateX 
END
&
THEORY Version IS
  POVersion(V3.6.8)(CLT == "V3.7.2")(local_op == OK)
END