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

⊦ (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))

User applied rule case distinction

And closed the goal!

Rule argument

[CASEDARG : pos: right 2, ()]

Additional information

[[CONCRETESIMPRULES : ([CSIMPNAMEDSEQ : command, , disj-217, ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ BookFlightOffer-AirlineCmd], [CSIMPNAMEDSEQ : command, , disj-286, ⊦ ConfirmRelease-UserCmd-3 ≠ BookFlightOffer-AirlineCmd], [CSIMPNAMEDSEQ : command, , disj-202, ⊦ ReleaseCCD-CreditCardCenterCmd ≠ BookFlightOffer-AirlineCmd], [CSIMPNAMEDSEQ : command, , disj-214, ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ BookSelected-TravelPlannerCmd], [CSIMPNAMEDSEQ : command, , disj-283, ⊦ ConfirmRelease-UserCmd-3 ≠ BookSelected-TravelPlannerCmd], [CSIMPNAMEDSEQ : command, , disj-199, ⊦ ReleaseCCD-CreditCardCenterCmd ≠ BookSelected-TravelPlannerCmd], [CSIMPNAMEDSEQ : name, , disj-197, ⊦ User-ConfirmedRelease-count (stringvar) ≠ User-GetSingleSelections (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-183, ⊦ User-ConfirmRelease-count (stringvar) ≠ User-GetSingleSelections (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-152, ⊦ User-ConfirmRelease (stringvar) ≠ User-GetSingleSelections (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-78, ⊦ locVar(stringvar) ≠ User-GetSingleSelections (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-117, ⊦ Mailbox(cmd) ≠ User-GetSingleSelections (stringvar)], [CSIMPNAMEDSEQ : name, , disj-98, ⊦ state(stringvar) ≠ User-GetSingleSelections (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-198, ⊦ User-ConfirmedRelease-count (stringvar) ≠ User-GetSingleSelection-count (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-184, ⊦ User-ConfirmRelease-count (stringvar) ≠ User-GetSingleSelection-count (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-153, ⊦ User-ConfirmRelease (stringvar) ≠ User-GetSingleSelection-count (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-79, ⊦ locVar(stringvar) ≠ User-GetSingleSelection-count (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-118, ⊦ Mailbox(cmd) ≠ User-GetSingleSelection-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-99, ⊦ state(stringvar) ≠ User-GetSingleSelection-count (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-196, ⊦ User-ConfirmedRelease-count (stringvar) ≠ User-GetSingleSelection (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-182, ⊦ User-ConfirmRelease-count (stringvar) ≠ User-GetSingleSelection (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-151, ⊦ User-ConfirmRelease (stringvar) ≠ User-GetSingleSelection (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-77, ⊦ locVar(stringvar) ≠ User-GetSingleSelection (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-116, ⊦ Mailbox(cmd) ≠ User-GetSingleSelection (stringvar)], [CSIMPNAMEDSEQ : name, , disj-97, ⊦ state(stringvar) ≠ User-GetSingleSelection (stringvar0)], [CSIMPNAMEDSEQ : command, , disj-210, ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ GetSingleSelection-UserCmd-2], [CSIMPNAMEDSEQ : command, , disj-271, ⊦ GetSingleSelection-UserCmd-2 ≠ ConfirmRelease-UserCmd-3], [CSIMPNAMEDSEQ : command, , disj-195, ⊦ ReleaseCCD-CreditCardCenterCmd ≠ GetSingleSelection-UserCmd-2], [CSIMPNAMEDSEQ : name, , disj-55, ⊦ TravelPlanner-flightOffer ≠ User-ConfirmedRelease-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-54, ⊦ TravelPlanner-flightOffer ≠ User-ConfirmRelease-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-52, ⊦ TravelPlanner-flightOffer ≠ User-ConfirmRelease (stringvar)], [CSIMPNAMEDSEQ : name, , disj-48, ⊦ TravelPlanner-flightOffer ≠ locVar(stringvar)], [CSIMPNAMEDSEQ : name, , disj-50, ⊦ TravelPlanner-flightOffer ≠ Mailbox(cmd)], [CSIMPNAMEDSEQ : name, , disj-49, ⊦ TravelPlanner-flightOffer ≠ state(stringvar)], [CSIMPNAMEDSEQ : name, , disj-115, ⊦ Mailbox(cmd) ≠ User-ConfirmedRelease-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-114, ⊦ Mailbox(cmd) ≠ User-ConfirmRelease-count (stringvar)], [CSIMPNAMEDSEQ : name, , disj-112, ⊦ Mailbox(cmd) ≠ User-ConfirmRelease (stringvar)], [CSIMPNAMEDSEQ : command, , disj-100, ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd], [CSIMPNAMEDSEQ : command, , disj-106, ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ ConfirmRelease-UserCmd-3], [CSIMPNAMEDSEQ : command, , disj-99, ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ ReleaseCCD-CreditCardCenterCmd], [CSIMPNAMEDSEQ : name, , inj-20, ⊦ Mailbox(cmd) = Mailbox(cmd0) ↔ cmd = cmd0], [CSIMPNAMEDSEQ : name, , disj-96, ⊦ state(stringvar) ≠ User-ConfirmedRelease-count (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-95, ⊦ state(stringvar) ≠ User-ConfirmRelease-count (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-93, ⊦ state(stringvar) ≠ User-ConfirmRelease (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-91, ⊦ state(stringvar) ≠ Mailbox(cmd)], [CSIMPNAMEDSEQ : name, , inj-21, ⊦ state(stringvar) = state(stringvar0) ↔ stringvar = stringvar0], [CSIMPNAMEDSEQ : name, , disj-70, ⊦ locVar(stringvar) ≠ state(stringvar0)], [CSIMPNAMEDSEQ : name, , disj-71, ⊦ locVar(stringvar) ≠ Mailbox(cmd)], [CSIMPNAMEDSEQ : name, , inj-22, ⊦ locVar(stringvar) = locVar(stringvar0) ↔ stringvar = stringvar0], [CSIMPNAMEDSEQ : name, , disj-73, ⊦ locVar(stringvar) ≠ User-ConfirmRelease (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-75, ⊦ locVar(stringvar) ≠ User-ConfirmRelease-count (stringvar0)], [CSIMPNAMEDSEQ : name, , disj-76, ⊦ locVar(stringvar) ≠ User-ConfirmedRelease-count (stringvar0)])]]