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: |
|---|---|---|
| disj-01 | ⊦ mkAirline(m) ≠ mkCreditCardCenter(m0) | An Axiom |
| disj-02 | ⊦ mkAirline(m) ≠ mkTravelAgency(m0) | An Axiom |
| disj-03 | ⊦ mkAirline(m) ≠ mkTravelPlanner(m0) | An Axiom |
| disj-04 | ⊦ mkAirline(m) ≠ mkUser(m0) | An Axiom |
| disj-05 | ⊦ mkCreditCardCenter(m) ≠ mkTravelAgency(m0) | An Axiom |
| disj-06 | ⊦ mkCreditCardCenter(m) ≠ mkTravelPlanner(m0) | An Axiom |
| disj-07 | ⊦ mkCreditCardCenter(m) ≠ mkUser(m0) | An Axiom |
| disj-08 | ⊦ mkTravelAgency(m) ≠ mkTravelPlanner(m0) | An Axiom |
| disj-09 | ⊦ mkTravelAgency(m) ≠ mkUser(m0) | An Axiom |
| disj-10 | ⊦ mkTravelPlanner(m) ≠ mkUser(m0) | An Axiom |
| sel-01 | ⊦ mkUser(m) .id = m | An Axiom |
| sel-02 | ⊦ mkTravelPlanner(m) .id = m | An Axiom |
| sel-03 | ⊦ mkTravelAgency(m) .id = m | An Axiom |
| sel-04 | ⊦ mkCreditCardCenter(m) .id = m | An Axiom |
| sel-05 | ⊦ mkAirline(m) .id = m | An Axiom |
| test-01 | ⊦ isUser(mkUser(m)) | An Axiom |
| test-02 | ⊦ ¬ isUser(mkTravelPlanner(m)) | An Axiom |
| test-03 | ⊦ ¬ isUser(mkTravelAgency(m)) | An Axiom |
| test-04 | ⊦ ¬ isUser(mkCreditCardCenter(m)) | An Axiom |
| test-05 | ⊦ ¬ isUser(mkAirline(m)) | An Axiom |
| test-06 | ⊦ ¬ isTravelPlanner(mkUser(m)) | An Axiom |
| test-07 | ⊦ isTravelPlanner(mkTravelPlanner(m)) | An Axiom |
| test-08 | ⊦ ¬ isTravelPlanner(mkTravelAgency(m)) | An Axiom |
| test-09 | ⊦ ¬ isTravelPlanner(mkCreditCardCenter(m)) | An Axiom |
| test-10 | ⊦ ¬ isTravelPlanner(mkAirline(m)) | An Axiom |
| test-11 | ⊦ ¬ isTravelAgency(mkUser(m)) | An Axiom |
| test-12 | ⊦ ¬ isTravelAgency(mkTravelPlanner(m)) | An Axiom |
| test-13 | ⊦ isTravelAgency(mkTravelAgency(m)) | An Axiom |
| test-14 | ⊦ ¬ isTravelAgency(mkCreditCardCenter(m)) | An Axiom |
| test-15 | ⊦ ¬ isTravelAgency(mkAirline(m)) | An Axiom |
| test-16 | ⊦ ¬ isCreditCardCenter(mkUser(m)) | An Axiom |
| test-17 | ⊦ ¬ isCreditCardCenter(mkTravelPlanner(m)) | An Axiom |
| test-18 | ⊦ ¬ isCreditCardCenter(mkTravelAgency(m)) | An Axiom |
| test-19 | ⊦ isCreditCardCenter(mkCreditCardCenter(m)) | An Axiom |
| test-20 | ⊦ ¬ isCreditCardCenter(mkAirline(m)) | An Axiom |
| test-21 | ⊦ ¬ isAirline(mkUser(m)) | An Axiom |
| test-22 | ⊦ ¬ isAirline(mkTravelPlanner(m)) | An Axiom |
| test-23 | ⊦ ¬ isAirline(mkTravelAgency(m)) | An Axiom |
| test-24 | ⊦ ¬ isAirline(mkCreditCardCenter(m)) | An Axiom |
| test-25 | ⊦ isAirline(mkAirline(m)) | An Axiom |
| inj-01 | ⊦ mkUser(m) = mkUser(m0) ↔ m = m0 | An Axiom |
| inj-02 | ⊦ mkTravelPlanner(m) = mkTravelPlanner(m0) ↔ m = m0 | An Axiom |
| inj-03 | ⊦ mkTravelAgency(m) = mkTravelAgency(m0) ↔ m = m0 | An Axiom |
| inj-04 | ⊦ mkCreditCardCenter(m) = mkCreditCardCenter(m0) ↔ m = m0 | An Axiom |
| inj-05 | ⊦ mkAirline(m) = mkAirline(m0) ↔ m = m0 | An Axiom |
| case | ⊦ ag = mkAirline(ag .id) ∨ ag = mkCreditCardCenter(ag .id) ∨ ag = mkTravelAgency(ag .id) ∨ ag = mkTravelPlanner(ag .id) ∨ ag = mkUser(ag .id) | An Axiom |
| ex-01 | ⊦ isUser(ag) ↔ (∃ m. ag = mkUser(m)) | An Axiom |
| ex-02 | ⊦ isTravelPlanner(ag) ↔ (∃ m. ag = mkTravelPlanner(m)) | An Axiom |
| ex-03 | ⊦ isTravelAgency(ag) ↔ (∃ m. ag = mkTravelAgency(m)) | An Axiom |
| ex-04 | ⊦ isCreditCardCenter(ag) ↔ (∃ m. ag = mkCreditCardCenter(m)) | An Axiom |
| ex-05 | ⊦ isAirline(ag) ↔ (∃ m. ag = mkAirline(m)) | An Axiom |
| elim-01 | ⊦ isUser(ag) → (m = ag .id ↔ ag = mkUser(m)) | An Axiom |
| elim-02 | ⊦ isTravelPlanner(ag) → (m = ag .id ↔ ag = mkTravelPlanner(m)) | An Axiom |
| elim-03 | ⊦ isTravelAgency(ag) → (m = ag .id ↔ ag = mkTravelAgency(m)) | An Axiom |
| elim-04 | ⊦ isCreditCardCenter(ag) → (m = ag .id ↔ ag = mkCreditCardCenter(m)) | An Axiom |
| elim-05 | ⊦ isAirline(ag) → (m = ag .id ↔ ag = mkAirline(m)) | An Axiom |
| gen | An Axiom |