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: |
|---|---|---|
| isDeclassDom-def | ⊦ isDeclassDom(domvar) ↔ ¬ domvar ≠ User->User_Airline | An Axiom |
| isStateDom-def | ⊦ isStateDom(domvar) ↔ ¬ ¬ (domvar = HighLow5 ∨ domvar = Abort8 ∨ domvar = Abort9) | An Axiom |
| usedDom-def | ⊦ usedDom(domvar) ↔ (∃ a. dom(a) = domvar) | An Axiom |
| usedDom-constructive | ⊦ usedDom(domvar) ↔ ¬ ¬ ( isAbort9(domvar) ∨ isAbort8(domvar) ∨ isHighLow5(domvar) ∨ isUser_Airline(domvar) ∨ isUser->User_Airline(domvar) ∨ isUser_TravelAgency_Airline(domvar) ∨ isUser(domvar)) | An Axiom |
| dom-flightOffers | ⊦ dom(Airline-flightOffers, mkAirline(n)) = User_TravelAgency_Airline | An Axiom |
| dom-ccd | ⊦ dom(CreditCardCenter-ccd, mkCreditCardCenter(n)) = User | An Axiom |
| dom-Mailbox-GetFlightOffers-01 | ⊦ dom(Mailbox(GetFlightOffers-TravelPlannerCmd), mkTravelPlanner(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-DeclassifiedCCD | ⊦ dom(Mailbox(DeclassifiedCCD-TravelPlannerCmd), mkTravelPlanner(n)) = User_Airline | An Axiom |
| dom-Mailbox-OkConfirmBooking | ⊦ dom(Mailbox(OkConfirmBooking-TravelPlannerCmd), mkTravelPlanner(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-GetFlightOffers-02 | ⊦ dom(Mailbox(GetFlightOffers-TravelAgencyCmd), mkTravelAgency(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-RetFlightOffers-01 | ⊦ dom(Mailbox(RetFlightOffers-TravelAgencyCmd), mkTravelAgency(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-PayCommission | ⊦ dom(Mailbox(PayCommission-TravelAgencyCmd), mkTravelAgency(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-ReleaseCCD | ⊦ dom(Mailbox(ReleaseCCD-CreditCardCenterCmd), mkCreditCardCenter(n)) = User | An Axiom |
| dom-Mailbox-GetDeclassifiedCCD | ⊦ dom(Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd), mkCreditCardCenter(n)) = User | An Axiom |
| dom-Mailbox-GetFlightOffers-03 | ⊦ dom(Mailbox(GetFlightOffers-AirlineCmd), mkAirline(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-OkPayCommission | ⊦ dom(Mailbox(OkPayCommission-AirlineCmd), mkAirline(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-GetInputRequestData | ⊦ dom(Mailbox(GetInputRequestData-UserCmd-1), mkUser(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-GetSingleSelection | ⊦ dom(Mailbox(GetSingleSelection-UserCmd-2), mkUser(n)) = User_Airline | An Axiom |
| dom-Mailbox-ConfirmRelease | ⊦ dom(Mailbox(ConfirmRelease-UserCmd-3), mkUser(n)) = User | An Axiom |
| dom-Mailbox-Confirm | ⊦ dom(Mailbox(Confirm-UserCmd-4), mkUser(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-RetFlightOffers-02 | ⊦ dom(Mailbox(RetFlightOffers-TravelPlannerCmd), mkTravelPlanner(n)) = User_TravelAgency_Airline | An Axiom |
| dom-Mailbox-BookSelected | ⊦ dom(Mailbox(BookSelected-TravelPlannerCmd), mkTravelPlanner(n)) = User_Airline | An Axiom |
| dom-Mailbox-BookFlightOffer | ⊦ dom(Mailbox(BookFlightOffer-AirlineCmd), mkAirline(n)) = User_Airline | An Axiom |
| dom-Init-GetInputRequestData-TravelPlannerCmd | ⊦ dom(Action(ag0, Init-GetInputRequestData-TravelPlannerCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-GetFlightOffers-TravelPlannerCmd | ⊦ dom(Action(ag0, GetFlightOffers-TravelPlannerCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-RetFlightOffersstate1-TravelPlannerCmd | ⊦ dom(Action(ag0, RetFlightOffersstate1-TravelPlannerCmd, ag1)) = User_Airline | An Axiom |
| dom-BookSelectedstate2-TravelPlannerCmd | ⊦ dom(Action(ag0, BookSelectedstate2-TravelPlannerCmd, ag1)) = User | An Axiom |
| dom-DeclassifiedCCD-TravelPlannerCmd | ⊦ dom(Action(ag0, DeclassifiedCCD-TravelPlannerCmd, ag1)) = User_Airline | An Axiom |
| dom-OkConfirmBooking-TravelPlannerCmd | ⊦ dom(Action(ag0, OkConfirmBooking-TravelPlannerCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-GetFlightOffers-TravelAgencyCmd | ⊦ dom(Action(ag0, GetFlightOffers-TravelAgencyCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-RetFlightOffers-TravelAgencyCmd | ⊦ dom(Action(ag0, RetFlightOffers-TravelAgencyCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-PayCommission-TravelAgencyCmd | ⊦ dom(Action(ag0, PayCommission-TravelAgencyCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-ReleaseCCD-CreditCardCenterCmd | ⊦ dom(Action(ag0, ReleaseCCD-CreditCardCenterCmd, ag1)) = User | An Axiom |
| dom-GetDeclassifiedCCD-CreditCardCenterCmd | ⊦ dom(Action(ag0, GetDeclassifiedCCD-CreditCardCenterCmd, ag1)) = User | An Axiom |
| dom-GetFlightOffers-AirlineCmd | ⊦ dom(Action(ag0, GetFlightOffers-AirlineCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-BookFlightOfferstate7-AirlineCmd | ⊦ dom(Action(ag0, BookFlightOfferstate7-AirlineCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-OkPayCommission-AirlineCmd | ⊦ dom(Action(ag0, OkPayCommission-AirlineCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-GetInputRequestData-UserCmd-1 | ⊦ dom(Action(ag0, GetInputRequestData-UserCmd-1, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-GetSingleSelection-UserCmd-2 | ⊦ dom(Action(ag0, GetSingleSelection-UserCmd-2, ag1)) = User_Airline | An Axiom |
| dom-ConfirmRelease-UserCmd-3 | ⊦ dom(Action(ag0, ConfirmRelease-UserCmd-3, ag1)) = User | An Axiom |
| dom-Confirm-UserCmd-4 | ⊦ dom(Action(ag0, Confirm-UserCmd-4, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-RetFlightOffers-TravelPlannerCmd | ⊦ dom(Action(ag0, RetFlightOffers-TravelPlannerCmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-BookSelected-TravelPlannerCmd | ⊦ dom(Action(ag0, BookSelected-TravelPlannerCmd, ag1)) = User_Airline | An Axiom |
| dom-declassifyCCD4ASM-CreditCardCenterCmd | ⊦ dom(Action(ag0, declassifyCCD4ASM-CreditCardCenterCmd, ag1)) = User->User_Airline | An Axiom |
| dom-afterdeclassifyCCD4ASM-CreditCardCenterCmd | ⊦ dom(Action(ag0, afterdeclassifyCCD4ASM-CreditCardCenterCmd, ag1)) = User_Airline | An Axiom |
| dom-BookFlightOffer-AirlineCmd | ⊦ dom(Action(ag0, BookFlightOffer-AirlineCmd, ag1)) = User_Airline | An Axiom |
| dom-BookFlightOfferstate6-AirlineCmd | ⊦ dom(Action(ag0, BookFlightOfferstate6-AirlineCmd, ag1)) = HighLow5 | An Axiom |
| dom-Abort8-UserCmd | ⊦ dom(Action(ag0, Abort8-UserCmd, ag1)) = Abort8 | An Axiom |
| dom-Abort9-UserCmd | ⊦ dom(Action(ag0, Abort9-UserCmd, ag1)) = Abort9 | An Axiom |
| dom-isInit-GetInputRequestData-TravelPlannerCmd | ⊦ isInit-GetInputRequestData-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isGetFlightOffers-TravelPlannerCmd | ⊦ isGetFlightOffers-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isRetFlightOffersstate1-TravelPlannerCmd | ⊦ isRetFlightOffersstate1-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline | An Axiom |
| dom-isBookSelectedstate2-TravelPlannerCmd | ⊦ isBookSelectedstate2-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User | An Axiom |
| dom-isDeclassifiedCCD-TravelPlannerCmd | ⊦ isDeclassifiedCCD-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline | An Axiom |
| dom-isOkConfirmBooking-TravelPlannerCmd | ⊦ isOkConfirmBooking-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isGetFlightOffers-TravelAgencyCmd | ⊦ isGetFlightOffers-TravelAgencyCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isRetFlightOffers-TravelAgencyCmd | ⊦ isRetFlightOffers-TravelAgencyCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isPayCommission-TravelAgencyCmd | ⊦ isPayCommission-TravelAgencyCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isReleaseCCD-CreditCardCenterCmd | ⊦ isReleaseCCD-CreditCardCenterCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User | An Axiom |
| dom-isGetDeclassifiedCCD-CreditCardCenterCmd | ⊦ isGetDeclassifiedCCD-CreditCardCenterCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User | An Axiom |
| dom-isGetFlightOffers-AirlineCmd | ⊦ isGetFlightOffers-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isBookFlightOfferstate7-AirlineCmd | ⊦ isBookFlightOfferstate7-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isOkPayCommission-AirlineCmd | ⊦ isOkPayCommission-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isGetInputRequestData-UserCmd-1 | ⊦ isGetInputRequestData-UserCmd-1(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isGetSingleSelection-UserCmd-2 | ⊦ isGetSingleSelection-UserCmd-2(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline | An Axiom |
| dom-isConfirmRelease-UserCmd-3 | ⊦ isConfirmRelease-UserCmd-3(cmd) → dom(Action(ag0, cmd, ag1)) = User | An Axiom |
| dom-isConfirm-UserCmd-4 | ⊦ isConfirm-UserCmd-4(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isRetFlightOffers-TravelPlannerCmd | ⊦ isRetFlightOffers-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline | An Axiom |
| dom-isBookSelected-TravelPlannerCmd | ⊦ isBookSelected-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline | An Axiom |
| dom-isdeclassifyCCD4ASM-CreditCardCenterCmd | ⊦ isdeclassifyCCD4ASM-CreditCardCenterCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User->User_Airline | An Axiom |
| dom-isafterdeclassifyCCD4ASM-CreditCardCenterCmd | ⊦ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline | An Axiom |
| dom-isBookFlightOffer-AirlineCmd | ⊦ isBookFlightOffer-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline | An Axiom |
| dom-isBookFlightOfferstate6-AirlineCmd | ⊦ isBookFlightOfferstate6-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = HighLow5 | An Axiom |
| dom-isAbort8-UserCmd | ⊦ isAbort8-UserCmd(cmd) → dom(Action(ag0, cmd, ag1)) = Abort8 | An Axiom |
| dom-isAbort9-UserCmd | ⊦ isAbort9-UserCmd(cmd) → dom(Action(ag0, cmd, ag1)) = Abort9 | An Axiom |