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 | ⊦ User ≠ User_Airline | An Axiom |
| disj-02 | ⊦ User ≠ User_TravelAgency_Airline | An Axiom |
| disj-03 | ⊦ User ≠ User->User_Airline | An Axiom |
| disj-04 | ⊦ User ≠ HighLow5 | An Axiom |
| disj-05 | ⊦ User ≠ Abort8 | An Axiom |
| disj-06 | ⊦ User ≠ Abort9 | An Axiom |
| disj-07 | ⊦ User_Airline ≠ User_TravelAgency_Airline | An Axiom |
| disj-08 | ⊦ User_Airline ≠ User->User_Airline | An Axiom |
| disj-09 | ⊦ User_Airline ≠ HighLow5 | An Axiom |
| disj-10 | ⊦ User_Airline ≠ Abort8 | An Axiom |
| disj-11 | ⊦ User_Airline ≠ Abort9 | An Axiom |
| disj-12 | ⊦ User_TravelAgency_Airline ≠ User->User_Airline | An Axiom |
| disj-13 | ⊦ User_TravelAgency_Airline ≠ HighLow5 | An Axiom |
| disj-14 | ⊦ User_TravelAgency_Airline ≠ Abort8 | An Axiom |
| disj-15 | ⊦ User_TravelAgency_Airline ≠ Abort9 | An Axiom |
| disj-16 | ⊦ User->User_Airline ≠ HighLow5 | An Axiom |
| disj-17 | ⊦ User->User_Airline ≠ Abort8 | An Axiom |
| disj-18 | ⊦ User->User_Airline ≠ Abort9 | An Axiom |
| disj-19 | ⊦ HighLow5 ≠ Abort8 | An Axiom |
| disj-20 | ⊦ HighLow5 ≠ Abort9 | An Axiom |
| disj-21 | ⊦ Abort8 ≠ Abort9 | An Axiom |
| test-01 | ⊦ isAbort9(Abort9) | An Axiom |
| test-02 | ⊦ ¬ isAbort9(Abort8) | An Axiom |
| test-03 | ⊦ ¬ isAbort9(HighLow5) | An Axiom |
| test-04 | ⊦ ¬ isAbort9(User->User_Airline) | An Axiom |
| test-05 | ⊦ ¬ isAbort9(User_TravelAgency_Airline) | An Axiom |
| test-06 | ⊦ ¬ isAbort9(User_Airline) | An Axiom |
| test-07 | ⊦ ¬ isAbort9(User) | An Axiom |
| test-08 | ⊦ ¬ isAbort8(Abort9) | An Axiom |
| test-09 | ⊦ isAbort8(Abort8) | An Axiom |
| test-10 | ⊦ ¬ isAbort8(HighLow5) | An Axiom |
| test-11 | ⊦ ¬ isAbort8(User->User_Airline) | An Axiom |
| test-12 | ⊦ ¬ isAbort8(User_TravelAgency_Airline) | An Axiom |
| test-13 | ⊦ ¬ isAbort8(User_Airline) | An Axiom |
| test-14 | ⊦ ¬ isAbort8(User) | An Axiom |
| test-15 | ⊦ ¬ isHighLow5(Abort9) | An Axiom |
| test-16 | ⊦ ¬ isHighLow5(Abort8) | An Axiom |
| test-17 | ⊦ isHighLow5(HighLow5) | An Axiom |
| test-18 | ⊦ ¬ isHighLow5(User->User_Airline) | An Axiom |
| test-19 | ⊦ ¬ isHighLow5(User_TravelAgency_Airline) | An Axiom |
| test-20 | ⊦ ¬ isHighLow5(User_Airline) | An Axiom |
| test-21 | ⊦ ¬ isHighLow5(User) | An Axiom |
| test-22 | ⊦ ¬ isUser->User_Airline(Abort9) | An Axiom |
| test-23 | ⊦ ¬ isUser->User_Airline(Abort8) | An Axiom |
| test-24 | ⊦ ¬ isUser->User_Airline(HighLow5) | An Axiom |
| test-25 | ⊦ isUser->User_Airline(User->User_Airline) | An Axiom |
| test-26 | ⊦ ¬ isUser->User_Airline(User_TravelAgency_Airline) | An Axiom |
| test-27 | ⊦ ¬ isUser->User_Airline(User_Airline) | An Axiom |
| test-28 | ⊦ ¬ isUser->User_Airline(User) | An Axiom |
| test-29 | ⊦ ¬ isUser_TravelAgency_Airline(Abort9) | An Axiom |
| test-30 | ⊦ ¬ isUser_TravelAgency_Airline(Abort8) | An Axiom |
| test-31 | ⊦ ¬ isUser_TravelAgency_Airline(HighLow5) | An Axiom |
| test-32 | ⊦ ¬ isUser_TravelAgency_Airline(User->User_Airline) | An Axiom |
| test-33 | ⊦ isUser_TravelAgency_Airline(User_TravelAgency_Airline) | An Axiom |
| test-34 | ⊦ ¬ isUser_TravelAgency_Airline(User_Airline) | An Axiom |
| test-35 | ⊦ ¬ isUser_TravelAgency_Airline(User) | An Axiom |
| test-36 | ⊦ ¬ isUser_Airline(Abort9) | An Axiom |
| test-37 | ⊦ ¬ isUser_Airline(Abort8) | An Axiom |
| test-38 | ⊦ ¬ isUser_Airline(HighLow5) | An Axiom |
| test-39 | ⊦ ¬ isUser_Airline(User->User_Airline) | An Axiom |
| test-40 | ⊦ ¬ isUser_Airline(User_TravelAgency_Airline) | An Axiom |
| test-41 | ⊦ isUser_Airline(User_Airline) | An Axiom |
| test-42 | ⊦ ¬ isUser_Airline(User) | An Axiom |
| test-43 | ⊦ ¬ isUser(Abort9) | An Axiom |
| test-44 | ⊦ ¬ isUser(Abort8) | An Axiom |
| test-45 | ⊦ ¬ isUser(HighLow5) | An Axiom |
| test-46 | ⊦ ¬ isUser(User->User_Airline) | An Axiom |
| test-47 | ⊦ ¬ isUser(User_TravelAgency_Airline) | An Axiom |
| test-48 | ⊦ ¬ isUser(User_Airline) | An Axiom |
| test-49 | ⊦ isUser(User) | An Axiom |
| case | ⊦ domvar = User ∨ domvar = User_Airline ∨ domvar = User_TravelAgency_Airline ∨ domvar = User->User_Airline ∨ domvar = HighLow5 ∨ domvar = Abort8 ∨ domvar = Abort9 | An Axiom |
| ex-01 | ⊦ isAbort9(domvar) ↔ domvar = Abort9 | An Axiom |
| ex-02 | ⊦ isAbort8(domvar) ↔ domvar = Abort8 | An Axiom |
| ex-03 | ⊦ isHighLow5(domvar) ↔ domvar = HighLow5 | An Axiom |
| ex-04 | ⊦ isUser->User_Airline(domvar) ↔ domvar = User->User_Airline | An Axiom |
| ex-05 | ⊦ isUser_TravelAgency_Airline(domvar) ↔ domvar = User_TravelAgency_Airline | An Axiom |
| ex-06 | ⊦ isUser_Airline(domvar) ↔ domvar = User_Airline | An Axiom |
| ex-07 | ⊦ isUser(domvar) ↔ domvar = User | An Axiom |
| gen | An Axiom |