[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 ccd-no-read-up (previous step)

observe(domvar, CreditCardCenter-ccd, mkCreditCardCenter(n)) ⊦ domvar = User, domvar = User->User_Airline, domvar = Abort9

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, , observe-Abort8, ⊦ observe(Abort8, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`pre8') ∧ exUser(ag))], [CSIMPNAMEDSEQ : domain, , disj-21, ⊦ Abort8 ≠ Abort9], [CSIMPNAMEDSEQ : domain, , disj-17, ⊦ User->User_Airline ≠ Abort8], [CSIMPNAMEDSEQ : domain, , disj-05, ⊦ User ≠ Abort8], [CSIMPNAMEDSEQ : observeAlter, , observe-HighLow5, ⊦ observe(HighLow5, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state6') ∧ exAirline(ag))], [CSIMPNAMEDSEQ : domain, , disj-20, ⊦ HighLow5 ≠ Abort9], [CSIMPNAMEDSEQ : domain, , disj-16, ⊦ User->User_Airline ≠ HighLow5], [CSIMPNAMEDSEQ : domain, , disj-04, ⊦ User ≠ HighLow5], [CSIMPNAMEDSEQ : name, , disj-35, ⊦ CreditCardCenter-ccd ≠ User-GetSingleSelections (stringvar)], [CSIMPNAMEDSEQ : name, , disj-36, ⊦ CreditCardCenter-ccd ≠ User-GetSingleSelection-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-34, ⊦ CreditCardCenter-ccd ≠ User-GetSingleSelection (stringvar)], [CSIMPNAMEDSEQ : name, , disj-25, ⊦ CreditCardCenter-ccd ≠ TravelPlanner-flightOffer], [CSIMPNAMEDSEQ : observeAlter, , observe-User_Airline, ⊦ observe (User_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`state1') ∧ exTravelPlanner(ag) ∨ nam = locVar (`flightOffers') ∧ exTravelPlanner(ag) ∨ nam = Mailbox (DeclassifiedCCD-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = TravelPlanner-flightOffer ∧ exTravelPlanner(ag) ∨ nam = locVar (`ccd_decl') ∧ exTravelPlanner(ag) ∨ nam = Mailbox (GetSingleSelection-UserCmd-2) ∧ exUser(ag) ∨ nam = User-GetSingleSelection (`2') ∧ exUser(ag) ∨ nam = User-GetSingleSelection-count (`2') ∧ exUser(ag) ∨ nam = User-GetSingleSelections (`2') ∧ exUser(ag) ∨ nam = Mailbox (BookSelected-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = state(`state4') ∧ exCreditCardCenter (ag) ∨ nam = locVar (`ccd_decl') ∧ exCreditCardCenter (ag) ∨ nam = Mailbox (BookFlightOffer-AirlineCmd) ∧ exAirline(ag) ∨ nam = locVar(`id') ∧ exAirline(ag) ∨ nam = locVar (`ccd_decl') ∧ exAirline(ag))], [CSIMPNAMEDSEQ : domain, , disj-11, ⊦ User_Airline ≠ Abort9], [CSIMPNAMEDSEQ : domain, , disj-08, ⊦ User_Airline ≠ User->User_Airline], [CSIMPNAMEDSEQ : domain, , disj-01, ⊦ User ≠ User_Airline], [CSIMPNAMEDSEQ : domain, , disj-02, ⊦ User ≠ User_TravelAgency_Airline], [CSIMPNAMEDSEQ : domain, , disj-12, ⊦ User_TravelAgency_Airline ≠ User->User_Airline], [CSIMPNAMEDSEQ : domain, , disj-15, ⊦ User_TravelAgency_Airline ≠ Abort9], [CSIMPNAMEDSEQ : observeAlter, , observe-User_TravelAgency_Airline, ⊦ observe (User_TravelAgency_Airline, nam, ag) ↔ ¬ ¬ ( false ∨ nam = state(`init') ∧ exUser(ag) ∨ nam = Mailbox (GetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = locVar (`requestData') ∧ exTravelPlanner(ag) ∨ nam = Mailbox (OkConfirmBooking-TravelPlannerCmd) ∧ exTravelPlanner(ag) ∨ nam = Mailbox (GetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = locVar (`requestData') ∧ exTravelAgency(ag) ∨ nam = Mailbox (RetFlightOffers-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = locVar (`flightOffers') ∧ exTravelAgency(ag) ∨ nam = Mailbox (PayCommission-TravelAgencyCmd) ∧ exTravelAgency(ag) ∨ nam = Mailbox (GetFlightOffers-AirlineCmd) ∧ exAirline(ag) ∨ nam = locVar (`requestData') ∧ exAirline(ag) ∨ nam = Airline-flightOffers ∧ exAirline(ag) ∨ nam = locVar (`filteredFlightOffers') ∧ exAirline(ag) ∨ nam = state(`state7') ∧ exAirline(ag) ∨ nam = Mailbox (OkPayCommission-AirlineCmd) ∧ exAirline(ag) ∨ nam = Mailbox (GetInputRequestData-UserCmd-1) ∧ exUser(ag) ∨ nam = User-GetInput (`1') ∧ exUser(ag) ∨ nam = User-GetInput-count (`1') ∧ exUser(ag) ∨ nam = User-GetInputs (`1') ∧ exUser(ag) ∨ nam = Mailbox (Confirm-UserCmd-4) ∧ exUser(ag) ∨ nam = User-Confirm(`4') ∧ exUser(ag) ∨ nam = User-Confirm-count (`4') ∧ exUser(ag) ∨ nam = User-Confirms (`4') ∧ exUser(ag) ∨ nam = Mailbox (RetFlightOffers-TravelPlannerCmd) ∧ exTravelPlanner(ag))], [CSIMPNAMEDSEQ : name, , disj-27, ⊦ CreditCardCenter-ccd ≠ state(stringvar)], [CSIMPNAMEDSEQ : name, , disj-28, ⊦ CreditCardCenter-ccd ≠ Mailbox(cmd)], [CSIMPNAMEDSEQ : name, , disj-26, ⊦ CreditCardCenter-ccd ≠ locVar(stringvar)], [CSIMPNAMEDSEQ : name, , disj-01, ⊦ Airline-flightOffers ≠ CreditCardCenter-ccd], [CSIMPNAMEDSEQ : name, , disj-40, ⊦ CreditCardCenter-ccd ≠ User-GetInput(stringvar)], [CSIMPNAMEDSEQ : name, , disj-42, ⊦ CreditCardCenter-ccd ≠ User-GetInput-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-41, ⊦ CreditCardCenter-ccd ≠ User-GetInputs(stringvar)], [CSIMPNAMEDSEQ : name, , disj-43, ⊦ CreditCardCenter-ccd ≠ User-Confirm(stringvar)], [CSIMPNAMEDSEQ : name, , disj-45, ⊦ CreditCardCenter-ccd ≠ User-Confirm-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-44, ⊦ CreditCardCenter-ccd ≠ User-Confirms(stringvar)])]]