[Imprint][Data Privacy Statement][E-Mail]



View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 1 from proof flightOffers-no-write-down (previous step)

alter(domvar, Airline-flightOffers, mkAirline(0)) ⊦ domvar ⇒ User_TravelAgency_Airline

User applied rule constructor cut

And closed the goal!

Rule argument

[var-arg: domvar]

Additional information

[[CONCRETESIMPRULES : ([CSIMPGEN : domain generated by user, user_airline, user_travelagency_airline, user->user_airline, highlow5, abort8, abort9;], [CSIMPNAMEDSEQ : observeAlter, , alter-Abort9, ⊦ alter(Abort9, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`pre9') ∧ exUser(ag) ∨ nam = state(`init') ∧ exUser(ag))], [CSIMPNAMEDSEQ : observeAlter, , alter-Abort8, ⊦ alter(Abort8, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`pre8') ∧ exUser(ag) ∨ nam = state(`init') ∧ exUser(ag))], [CSIMPNAMEDSEQ : observeAlter, , alter-HighLow5, ⊦ alter(HighLow5, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state6') ∧ exAirline(ag) ∨ nam = state(`state7') ∧ exAirline(ag))], [CSIMPNAMEDSEQ : name, , disj-06, ⊦ Airline-flightOffers ≠ declassify-count(stringvar)], [CSIMPNAMEDSEQ : observeAlter, , alter-User-User_Airline, ⊦ alter (User->User_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state3') ∧ exCreditCardCenter (ag) ∨ nam = locVar (`ccd_decl') ∧ exCreditCardCenter (ag) ∨ nam = declassify-count (`declassifyCCD') ∧ exCreditCardCenter (ag) ∨ nam = state(`state4') ∧ exCreditCardCenter (ag))], [CSIMPNAMEDSEQ : name, , disj-22, ⊦ Airline-flightOffers ≠ User-Confirm-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-20, ⊦ Airline-flightOffers ≠ User-Confirm(stringvar)], [CSIMPNAMEDSEQ : name, , disj-19, ⊦ Airline-flightOffers ≠ User-GetInput-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-17, ⊦ Airline-flightOffers ≠ User-GetInput(stringvar)], [CSIMPNAMEDSEQ : observeAlter, , alter-User_TravelAgency_Airline, ⊦ alter (User_TravelAgency_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`init') ∧ exUser(ag) ∨ nam = Mailbox (GetInputRequestData-UserCmd-1) ∧ exUser(ag) ∨ nam = Mailbox (GetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = locVar (`requestData') ∧ exTravelPlanner(ag) ∨ nam = Mailbox (GetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = Mailbox (OkConfirmBooking-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox (Confirm-UserCmd-4) ∧ exUser(ag) ∨ nam = Mailbox (GetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = locVar (`requestData') ∧ exTravelAgency(ag) ∨ nam = Mailbox (GetFlightOffers-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox (RetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = locVar (`flightOffers') ∧ exTravelAgency(ag) ∨ nam = Mailbox (RetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox (PayCommission-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = Mailbox (OkPayCommission-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox (GetFlightOffers-AirlineCmd) ∧ exAirline(ag) ∨ nam = locVar (`requestData') ∧ exAirline(ag) ∨ nam = locVar (`filteredFlightOffers') ∧ exAirline(ag) ∨ nam = Mailbox (RetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = state(`state7') ∧ exAirline(ag) ∨ nam = Mailbox (PayCommission-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = Mailbox (OkPayCommission-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox (OkConfirmBooking-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox (GetInputRequestData-UserCmd-1) ∧ exUser(ag) ∨ nam = User-GetInput (`1') ∧ exUser(ag) ∨ nam = User-GetInput-count (`1') ∧ exUser(ag) ∨ nam = state(`init') ∧ exUser(ag) ∨ nam = Mailbox (GetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox (Confirm-UserCmd-4) ∧ exUser(ag) ∨ nam = User-Confirm(`4') ∧ exUser(ag) ∨ nam = User-Confirm-count (`4') ∧ exUser(ag) ∨ nam = Mailbox (RetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = locVar (`flightOffers') ∧ exTravelPlanner(ag) ∨ nam = state(`state1') ∧ exTravelPlanner(ag))], [CSIMPNAMEDSEQ : name, , disj-10, ⊦ Airline-flightOffers ≠ User-ConfirmedRelease-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-09, ⊦ Airline-flightOffers ≠ User-ConfirmRelease-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-07, ⊦ Airline-flightOffers ≠ User-ConfirmRelease (stringvar)], [CSIMPNAMEDSEQ : observeAlter, , alter-User, ⊦ alter(User, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state2') ∧ exTravelPlanner(ag) ∨ nam = Mailbox (ReleaseCCD-CreditCardCenterCmd) ∧ exCreditCardCenter (ag) ∨ nam = Mailbox (ReleaseCCD-CreditCardCenterCmd) ∧ exCreditCardCenter (ag) ∨ nam = locVar(`airline') ∧ exCreditCardCenter (ag) ∨ nam = Mailbox (ConfirmRelease-UserCmd-3) ∧ exUser(ag) ∨ nam = Mailbox (GetDeclassifiedCCD-CreditCardCenterCmd) ∧ exCreditCardCenter (ag) ∨ nam = state(`state3') ∧ exCreditCardCenter (ag) ∨ nam = Mailbox (ConfirmRelease-UserCmd-3) ∧ exUser(ag) ∨ nam = locVar(`ccd') ∧ exUser(ag) ∨ nam = locVar(`airline') ∧ exUser(ag) ∨ nam = User-ConfirmRelease (`3') ∧ exUser(ag) ∨ nam = User-ConfirmRelease-count (`3') ∧ exUser(ag) ∨ nam = User-ConfirmedRelease-count (`3') ∧ exUser(ag) ∨ nam = state(`pre9') ∧ exUser(ag) ∨ nam = Mailbox (GetDeclassifiedCCD-CreditCardCenterCmd) ∧ exCreditCardCenter (ag))], [CSIMPNAMEDSEQ : observeAlter, , alter-User_Airline, ⊦ alter(User_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state1') ∧ exTravelPlanner(ag) ∨ nam = Mailbox (GetSingleSelection-UserCmd-2) ∧ exUser(ag) ∨ nam = Mailbox (DeclassifiedCCD-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = locVar (`ccd_decl') ∧ exTravelPlanner(ag) ∨ nam = Mailbox (BookFlightOffer-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox (GetSingleSelection-UserCmd-2) ∧ exUser(ag) ∨ nam = locVar (`flightOffers') ∧ exUser(ag) ∨ nam = User-GetSingleSelection (`2') ∧ exUser(ag) ∨ nam = User-GetSingleSelection-count (`2') ∧ exUser(ag) ∨ nam = state(`pre8') ∧ exUser(ag) ∨ nam = Mailbox (BookSelected-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox (BookSelected-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = TravelPlanner-flightOffer ∧ exTravelPlanner(ag) ∨ nam = state(`state2') ∧ exTravelPlanner(ag) ∨ nam = state(`state4') ∧ exCreditCardCenter (ag) ∨ nam = Mailbox (DeclassifiedCCD-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox (BookFlightOffer-AirlineCmd) ∧ exAirline(ag) ∨ nam = locVar(`id') ∧ exAirline(ag) ∨ nam = locVar (`ccd_decl') ∧ exAirline(ag) ∨ nam = state(`state6') ∧ exAirline(ag))], [CSIMPNAMEDSEQ : name, , disj-04, ⊦ Airline-flightOffers ≠ state(stringvar)], [CSIMPNAMEDSEQ : name, , disj-05, ⊦ Airline-flightOffers ≠ Mailbox(cmd)], [CSIMPNAMEDSEQ : name, , disj-03, ⊦ Airline-flightOffers ≠ locVar(stringvar)], [CSIMPNAMEDSEQ : name, , disj-11, ⊦ Airline-flightOffers ≠ User-GetSingleSelection (stringvar)], [CSIMPNAMEDSEQ : name, , disj-13, ⊦ Airline-flightOffers ≠ User-GetSingleSelection-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-02, ⊦ Airline-flightOffers ≠ TravelPlanner-flightOffer])]]