[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 2 from proof alter-observe-respects-policy (previous step)

domvar0 = User_Airline, observe(domvar0, nam, ag) ⊦ domvar0 = User, domvar0 = User->User_Airline, domvar0 = Abort9, (nam ≠ state(`state2') ∨ ¬ exTravelPlanner(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 ≠ 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))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 1:
⊦ (nam ≠ state(`state2') ∨ ¬ exTravelPlanner(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 ≠ 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 ≠ 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) ∨ ag ≠ mkAirline(0)) ∧ (nam ≠ locVar(`id') ∨ ag ≠ mkAirline(0)) ∧ (nam ≠ locVar(`ccd_decl') ∨ ag ≠ mkAirline(0))

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ([CSIMPNAMEDSEQ : exAgent, , exAirline-s, ⊦ exAirline(ag) ↔ ag = mkAirline(0)], [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])]]