This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| NUMOFAPPSANDUSERS-def | ⊦ NUMOFAPPSANDUSERS ≠ 0 | An Axiom |
| NUMOFAirline-def | ⊦ NUMOFAirline = 1 | An Axiom |
| NUMOFCreditCardCenter-def | ⊦ NUMOFCreditCardCenter = NUMOFAPPSANDUSERS | An Axiom |
| NUMOFTravelAgency-def | ⊦ NUMOFTravelAgency = 1 | An Axiom |
| NUMOFTravelPlanner-def | ⊦ NUMOFTravelPlanner = NUMOFAPPSANDUSERS | An Axiom |
| NUMOFUser-def | ⊦ NUMOFUser = NUMOFAPPSANDUSERS | An Axiom |
| exAgent-def | ⊦ exAgent(ag) ↔ exAirline(ag) ∨ exCreditCardCenter(ag) ∨ exTravelAgency(ag) ∨ exTravelPlanner(ag) ∨ exUser(ag) | An Axiom |
| exAirline-def | ⊦ exAirline(ag) ↔ isAirline(ag) ∧ ag .id < NUMOFAirline | An Axiom |
| exCreditCardCenter-def | ⊦ exCreditCardCenter(ag) ↔ isCreditCardCenter(ag) ∧ ag .id < NUMOFCreditCardCenter | An Axiom |
| exTravelAgency-def | ⊦ exTravelAgency(ag) ↔ isTravelAgency(ag) ∧ ag .id < NUMOFTravelAgency | An Axiom |
| exTravelPlanner-def | ⊦ exTravelPlanner(ag) ↔ isTravelPlanner(ag) ∧ ag .id < NUMOFTravelPlanner | An Axiom |
| exUser-def | ⊦ exUser(ag) ↔ isUser(ag) ∧ ag .id < NUMOFUser | An Axiom |
| exAirline-is | ⊦ ¬ isAirline(ag) → ¬ exAirline(ag) | An Axiom |
| exCreditCardCenter-is | ⊦ ¬ isCreditCardCenter(ag) → ¬ exCreditCardCenter(ag) | An Axiom |
| exTravelAgency-is | ⊦ ¬ isTravelAgency(ag) → ¬ exTravelAgency(ag) | An Axiom |
| exTravelPlanner-is | ⊦ ¬ isTravelPlanner(ag) → ¬ exTravelPlanner(ag) | An Axiom |
| exUser-is | ⊦ ¬ isUser(ag) → ¬ exUser(ag) | An Axiom |
| exAirline-s | ⊦ exAirline(ag) ↔ ag = mkAirline(0) | An Axiom |
| exTravelAgency-s | ⊦ exTravelAgency(ag) ↔ ag = mkTravelAgency(0) | An Axiom |
| exAirline-numof | ⊦ exAirline(mkAirline(n)) ↔ n < NUMOFAirline | An Axiom |
| exCreditCardCenter-numof | ⊦ exCreditCardCenter(mkCreditCardCenter(n)) ↔ n < NUMOFCreditCardCenter | An Axiom |
| exTravelAgency-numof | ⊦ exTravelAgency(mkTravelAgency(n)) ↔ n < NUMOFTravelAgency | An Axiom |
| exTravelPlanner-numof | ⊦ exTravelPlanner(mkTravelPlanner(n)) ↔ n < NUMOFTravelPlanner | An Axiom |
| exUser-numof | ⊦ exUser(mkUser(n)) ↔ n < NUMOFUser | An Axiom |
| exAgent-Airline-is | ⊦ isAirline(ag) → (exAgent(ag) ↔ ag .id < NUMOFAirline) | An Axiom |
| exAgent-CreditCardCenter-is | ⊦ isCreditCardCenter(ag) → (exAgent(ag) ↔ ag .id < NUMOFCreditCardCenter) | An Axiom |
| exAgent-TravelAgency-is | ⊦ isTravelAgency(ag) → (exAgent(ag) ↔ ag .id < NUMOFTravelAgency) | An Axiom |
| exAgent-TravelPlanner-is | ⊦ isTravelPlanner(ag) → (exAgent(ag) ↔ ag .id < NUMOFTravelPlanner) | An Axiom |
| exAgent-User-is | ⊦ isUser(ag) → (exAgent(ag) ↔ ag .id < NUMOFUser) | An Axiom |
| exAgent-Airline-mk | ⊦ exAgent(mkAirline(n)) ↔ n < NUMOFAirline | An Axiom |
| exAgent-CreditCardCenter-mk | ⊦ exAgent(mkCreditCardCenter(n)) ↔ n < NUMOFCreditCardCenter | An Axiom |
| exAgent-TravelAgency-mk | ⊦ exAgent(mkTravelAgency(n)) ↔ n < NUMOFTravelAgency | An Axiom |
| exAgent-TravelPlanner-mk | ⊦ exAgent(mkTravelPlanner(n)) ↔ n < NUMOFTravelPlanner | An Axiom |
| exAgent-User-mk | ⊦ exAgent(mkUser(n)) ↔ n < NUMOFUser | An Axiom |
| ex-not-CreditCardCenter | ⊦ ¬ exCreditCardCenter(mkCreditCardCenter(n)) ↔ NUMOFAPPSANDUSERS ≤ n | An Axiom |
| num-le-CreditCardCenter | ⊦ NUMOFAPPSANDUSERS ≤ ag .id → ¬ exCreditCardCenter(ag) | An Axiom |
| ex-not-TravelPlanner | ⊦ ¬ exTravelPlanner(mkTravelPlanner(n)) ↔ NUMOFAPPSANDUSERS ≤ n | An Axiom |
| num-le-TravelPlanner | ⊦ NUMOFAPPSANDUSERS ≤ ag .id → ¬ exTravelPlanner(ag) | An Axiom |
| ex-not-User | ⊦ ¬ exUser(mkUser(n)) ↔ NUMOFAPPSANDUSERS ≤ n | An Axiom |
| num-le-User | ⊦ NUMOFAPPSANDUSERS ≤ ag .id → ¬ exUser(ag) | An Axiom |
| ex-zero-01 | ⊦ ¬ exAirline(mkAirline(0)) ↔ false | An Axiom |
| ex-zero-02 | ⊦ ¬ exCreditCardCenter(mkCreditCardCenter(0)) ↔ false | An Axiom |
| ex-zero-03 | ⊦ ¬ exTravelAgency(mkTravelAgency(0)) ↔ false | An Axiom |
| ex-zero-04 | ⊦ ¬ exTravelPlanner(mkTravelPlanner(0)) ↔ false | An Axiom |
| ex-zero-05 | ⊦ ¬ exUser(mkUser(0)) ↔ false | An Axiom |
| ex-not-01 | ⊦ ¬ exAirline(mkCreditCardCenter(n)) | An Axiom |
| ex-not-02 | ⊦ exAirline(ag) → ¬ exCreditCardCenter(ag) | An Axiom |
| ex-not-03 | ⊦ ¬ exAirline(mkTravelAgency(n)) | An Axiom |
| ex-not-04 | ⊦ exAirline(ag) → ¬ exTravelAgency(ag) | An Axiom |
| ex-not-05 | ⊦ ¬ exAirline(mkTravelPlanner(n)) | An Axiom |
| ex-not-06 | ⊦ exAirline(ag) → ¬ exTravelPlanner(ag) | An Axiom |
| ex-not-07 | ⊦ ¬ exAirline(mkUser(n)) | An Axiom |
| ex-not-08 | ⊦ exAirline(ag) → ¬ exUser(ag) | An Axiom |
| ex-not-09 | ⊦ ¬ exCreditCardCenter(mkAirline(n)) | An Axiom |
| ex-not-10 | ⊦ exCreditCardCenter(ag) → ¬ exAirline(ag) | An Axiom |
| ex-not-11 | ⊦ ¬ exCreditCardCenter(mkTravelAgency(n)) | An Axiom |
| ex-not-12 | ⊦ exCreditCardCenter(ag) → ¬ exTravelAgency(ag) | An Axiom |
| ex-not-13 | ⊦ ¬ exCreditCardCenter(mkTravelPlanner(n)) | An Axiom |
| ex-not-14 | ⊦ exCreditCardCenter(ag) → ¬ exTravelPlanner(ag) | An Axiom |
| ex-not-15 | ⊦ ¬ exCreditCardCenter(mkUser(n)) | An Axiom |
| ex-not-16 | ⊦ exCreditCardCenter(ag) → ¬ exUser(ag) | An Axiom |
| ex-not-17 | ⊦ ¬ exTravelAgency(mkAirline(n)) | An Axiom |
| ex-not-18 | ⊦ exTravelAgency(ag) → ¬ exAirline(ag) | An Axiom |
| ex-not-19 | ⊦ ¬ exTravelAgency(mkCreditCardCenter(n)) | An Axiom |
| ex-not-20 | ⊦ exTravelAgency(ag) → ¬ exCreditCardCenter(ag) | An Axiom |
| ex-not-21 | ⊦ ¬ exTravelAgency(mkTravelPlanner(n)) | An Axiom |
| ex-not-22 | ⊦ exTravelAgency(ag) → ¬ exTravelPlanner(ag) | An Axiom |
| ex-not-23 | ⊦ ¬ exTravelAgency(mkUser(n)) | An Axiom |
| ex-not-24 | ⊦ exTravelAgency(ag) → ¬ exUser(ag) | An Axiom |
| ex-not-25 | ⊦ ¬ exTravelPlanner(mkAirline(n)) | An Axiom |
| ex-not-26 | ⊦ exTravelPlanner(ag) → ¬ exAirline(ag) | An Axiom |
| ex-not-27 | ⊦ ¬ exTravelPlanner(mkCreditCardCenter(n)) | An Axiom |
| ex-not-28 | ⊦ exTravelPlanner(ag) → ¬ exCreditCardCenter(ag) | An Axiom |
| ex-not-29 | ⊦ ¬ exTravelPlanner(mkTravelAgency(n)) | An Axiom |
| ex-not-30 | ⊦ exTravelPlanner(ag) → ¬ exTravelAgency(ag) | An Axiom |
| ex-not-31 | ⊦ ¬ exTravelPlanner(mkUser(n)) | An Axiom |
| ex-not-32 | ⊦ exTravelPlanner(ag) → ¬ exUser(ag) | An Axiom |
| ex-not-33 | ⊦ ¬ exUser(mkAirline(n)) | An Axiom |
| ex-not-34 | ⊦ exUser(ag) → ¬ exAirline(ag) | An Axiom |
| ex-not-35 | ⊦ ¬ exUser(mkCreditCardCenter(n)) | An Axiom |
| ex-not-36 | ⊦ exUser(ag) → ¬ exCreditCardCenter(ag) | An Axiom |
| ex-not-37 | ⊦ ¬ exUser(mkTravelAgency(n)) | An Axiom |
| ex-not-38 | ⊦ exUser(ag) → ¬ exTravelAgency(ag) | An Axiom |
| ex-not-39 | ⊦ ¬ exUser(mkTravelPlanner(n)) | An Axiom |
| ex-not-40 | ⊦ exUser(ag) → ¬ exTravelPlanner(ag) | An Axiom |