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: |
|---|---|---|
| domains-interference-def | ⊦ domsvar ⇒ domsvar0 ↔ (∃ domvar, domvar0. domvar ∈ domsvar ∧ domvar0 ∈ domsvar0 ∧ domvar ⇒ domvar0) | An Axiom |
| User-interference-def | ⊦ User ⇒ domvar ↔ domvar = User ∨ domvar = User->User_Airline ∨ domvar = Abort9 | An Axiom |
| User_Airline-interference-def | ⊦ User_Airline ⇒ domvar ↔ domvar = User_Airline ∨ domvar = User ∨ domvar = HighLow5 ∨ domvar = Abort8 | An Axiom |
| User_TravelAgency_Airline-interference-def | ⊦ User_TravelAgency_Airline ⇒ domvar ↔ domvar = User_TravelAgency_Airline ∨ domvar = User_Airline ∨ domvar = User | An Axiom |
| User-User_Airline-interference-def | ⊦ User->User_Airline ⇒ domvar ↔ domvar = User->User_Airline ∨ domvar = User_Airline | An Axiom |
| HighLow5-interference-def | ⊦ HighLow5 ⇒ domvar ↔ domvar = HighLow5 ∨ domvar = User_TravelAgency_Airline | An Axiom |
| Abort8-interference-def | ⊦ Abort8 ⇒ domvar ↔ domvar = Abort8 ∨ domvar = User_TravelAgency_Airline | An Axiom |
| Abort9-interference-def | ⊦ Abort9 ⇒ domvar ↔ domvar = Abort9 ∨ domvar = User_TravelAgency_Airline | An Axiom |