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: |
|---|---|---|
| eqd-def | ⊦ eqd(s, domvar, s0) ↔ (∀ nam, ag. observe(domvar, nam, ag) → s(nam, ag) = s0(nam, ag)) | An Axiom |
| eqdAirline-def | ⊦ eqdAirline(s, nam, s0) ↔ (∀ ag. exAirline(ag) → s(nam, ag) = s0(nam, ag)) | An Axiom |
| eqdAirline-forward | ⊦ eqdAirline(s, nam, s0) → s0(nam, mkAirline(0)) = s(nam, mkAirline(0)) | An Axiom |
| eqdCreditCardCenter-def | ⊦ eqdCreditCardCenter(s, nam, s0) ↔ (∀ ag. exCreditCardCenter(ag) → s(nam, ag) = s0(nam, ag)) | An Axiom |
| eqdCreditCardCenter-forward | ⊦ eqdCreditCardCenter(s, nam, s0) ∧ exCreditCardCenter(ag) → s0(nam, ag) = s(nam, ag) | An Axiom |
| eqdTravelAgency-def | ⊦ eqdTravelAgency(s, nam, s0) ↔ (∀ ag. exTravelAgency(ag) → s(nam, ag) = s0(nam, ag)) | An Axiom |
| eqdTravelAgency-forward | ⊦ eqdTravelAgency(s, nam, s0) → s0(nam, mkTravelAgency(0)) = s(nam, mkTravelAgency(0)) | An Axiom |
| eqdTravelPlanner-def | ⊦ eqdTravelPlanner(s, nam, s0) ↔ (∀ ag. exTravelPlanner(ag) → s(nam, ag) = s0(nam, ag)) | An Axiom |
| eqdTravelPlanner-forward | ⊦ eqdTravelPlanner(s, nam, s0) ∧ exTravelPlanner(ag) → s0(nam, ag) = s(nam, ag) | An Axiom |
| eqdUser-def | ⊦ eqdUser(s, nam, s0) ↔ (∀ ag. exUser(ag) → s(nam, ag) = s0(nam, ag)) | An Axiom |
| eqdUser-forward | ⊦ eqdUser(s, nam, s0) ∧ exUser(ag) → s0(nam, ag) = s(nam, ag) | An Axiom |
| eqd-User | ⊦ eqd(s, User, s0) ↔ ¬ ¬ ( true ∧ eqdTravelPlanner(s, state(`state2'), s0) ∧ eqdTravelPlanner(s, TravelPlanner-flightOffer, s0) ∧ eqdCreditCardCenter(s, Mailbox(ReleaseCCD-CreditCardCenterCmd), s0) ∧ eqdCreditCardCenter(s, CreditCardCenter-ccd, s0) ∧ eqdCreditCardCenter(s, locVar(`airline'), s0) ∧ eqdCreditCardCenter(s, Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd), s0) ∧ eqdUser(s, Mailbox(ConfirmRelease-UserCmd-3), s0) ∧ eqdUser(s, User-ConfirmRelease(`3'), s0) ∧ eqdUser(s, User-ConfirmRelease-count(`3'), s0) ∧ eqdUser(s, User-ConfirmReleases(`3'), s0) ∧ eqdUser(s, User-ConfirmedRelease-count(`3'), s0)) | An Axiom |
| eqd-User_Airline | ⊦ eqd(s, User_Airline, s0) ↔ ¬ ¬ ( true ∧ eqdTravelPlanner(s, state(`state1'), s0) ∧ eqdTravelPlanner(s, locVar(`flightOffers'), s0) ∧ eqdTravelPlanner(s, Mailbox(DeclassifiedCCD-TravelPlannerCmd), s0) ∧ eqdTravelPlanner(s, TravelPlanner-flightOffer, s0) ∧ eqdTravelPlanner(s, locVar(`ccd_decl'), s0) ∧ eqdUser(s, Mailbox(GetSingleSelection-UserCmd-2), s0) ∧ eqdUser(s, User-GetSingleSelection(`2'), s0) ∧ eqdUser(s, User-GetSingleSelection-count(`2'), s0) ∧ eqdUser(s, User-GetSingleSelections(`2'), s0) ∧ eqdTravelPlanner(s, Mailbox(BookSelected-TravelPlannerCmd), s0) ∧ eqdCreditCardCenter(s, state(`state4'), s0) ∧ eqdCreditCardCenter(s, locVar(`ccd_decl'), s0) ∧ eqdAirline(s, Mailbox(BookFlightOffer-AirlineCmd), s0) ∧ eqdAirline(s, locVar(`id'), s0) ∧ eqdAirline(s, locVar(`ccd_decl'), s0)) | An Axiom |
| eqd-User_TravelAgency_Airline | ⊦ eqd(s, User_TravelAgency_Airline, s0) ↔ ¬ ¬ ( true ∧ eqdUser(s, state(`init'), s0) ∧ eqdTravelPlanner(s, Mailbox(GetFlightOffers-TravelPlannerCmd), s0) ∧ eqdTravelPlanner(s, locVar(`requestData'), s0) ∧ eqdTravelPlanner(s, Mailbox(OkConfirmBooking-TravelPlannerCmd), s0) ∧ eqdTravelAgency(s, Mailbox(GetFlightOffers-TravelAgencyCmd), s0) ∧ eqdTravelAgency(s, locVar(`requestData'), s0) ∧ eqdTravelAgency(s, Mailbox(RetFlightOffers-TravelAgencyCmd), s0) ∧ eqdTravelAgency(s, locVar(`flightOffers'), s0) ∧ eqdTravelAgency(s, Mailbox(PayCommission-TravelAgencyCmd), s0) ∧ eqdAirline(s, Mailbox(GetFlightOffers-AirlineCmd), s0) ∧ eqdAirline(s, locVar(`requestData'), s0) ∧ eqdAirline(s, Airline-flightOffers, s0) ∧ eqdAirline(s, locVar(`filteredFlightOffers'), s0) ∧ eqdAirline(s, state(`state7'), s0) ∧ eqdAirline(s, Mailbox(OkPayCommission-AirlineCmd), s0) ∧ eqdUser(s, Mailbox(GetInputRequestData-UserCmd-1), s0) ∧ eqdUser(s, User-GetInput(`1'), s0) ∧ eqdUser(s, User-GetInput-count(`1'), s0) ∧ eqdUser(s, User-GetInputs(`1'), s0) ∧ eqdUser(s, Mailbox(Confirm-UserCmd-4), s0) ∧ eqdUser(s, User-Confirm(`4'), s0) ∧ eqdUser(s, User-Confirm-count(`4'), s0) ∧ eqdUser(s, User-Confirms(`4'), s0) ∧ eqdTravelPlanner(s, Mailbox(RetFlightOffers-TravelPlannerCmd), s0)) | An Axiom |
| eqd-User-User_Airline | ⊦ eqd(s, User->User_Airline, s0) ↔ ¬ ¬ ( true ∧ eqdCreditCardCenter(s, state(`state3'), s0) ∧ eqdCreditCardCenter(s, CreditCardCenter-ccd, s0) ∧ eqdCreditCardCenter(s, declassify-count(`declassifyCCD'), s0)) | An Axiom |
| eqd-HighLow5 | ⊦ eqd(s, HighLow5, s0) ↔ ¬ ¬ (true ∧ eqdAirline(s, state(`state6'), s0)) | An Axiom |
| eqd-Abort8 | ⊦ eqd(s, Abort8, s0) ↔ ¬ ¬ (true ∧ eqdUser(s, state(`pre8'), s0)) | An Axiom |
| eqd-Abort9 | ⊦ eqd(s, Abort9, s0) ↔ ¬ ¬ (true ∧ eqdUser(s, state(`pre9'), s0)) | An Axiom |