enrich domain , 
       state with
   functions 
      obs : (name × Agent → Data) × domain → name × Agent → Data;
   predicates 
      observe : domain × name × Agent;
      alter : domain × name × Agent;
   
   axioms 
      obs-in-domain :  ⊦ observe(domvar, nam, ag) → obs(s, domvar)(nam, ag) = s(nam, ag);
      used for : s, ls;
       
      obs-other-domain :  ⊦ ¬ observe(domvar, nam, ag) → obs(s, domvar)(nam, ag) = null;
      used for : s, ls;
       
      observe-User
      : ⊦ 
          observe(User, nam, ag)
        ↔ ¬ ¬ (  false ∨ nam = state(`state2') ∧ exTravelPlanner(ag) ∨ nam = TravelPlanner-flightOffer ∧ exTravelPlanner(ag)
               ∨ nam = Mailbox(ReleaseCCD-CreditCardCenterCmd) ∧ exCreditCardCenter(ag) ∨ nam = CreditCardCenter-ccd ∧ exCreditCardCenter(ag)
               ∨ nam = locVar(`airline') ∧ exCreditCardCenter(ag) ∨ nam = Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd) ∧ exCreditCardCenter(ag)
               ∨ nam = Mailbox(ConfirmRelease-UserCmd-3) ∧ exUser(ag) ∨ nam = User-ConfirmRelease(`3') ∧ exUser(ag)
               ∨ nam = User-ConfirmRelease-count(`3') ∧ exUser(ag) ∨ nam = User-ConfirmReleases(`3') ∧ exUser(ag)
               ∨ nam = User-ConfirmedRelease-count(`3') ∧ exUser(ag));
      used for : s, ls;
       
      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));
      used for : s, ls;
       
      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));
      used for : s, ls;
       
      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));
      used for : s, ls;
       
      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));
      used for : s, ls;
       
      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));
      used for : s, ls;
       
      observe-User-User_Airline
      : ⊦ 
          observe(User->User_Airline, nam, ag)
        ↔ ¬ ¬ (  false ∨ nam = state(`state3') ∧ exCreditCardCenter(ag) ∨ nam = CreditCardCenter-ccd ∧ exCreditCardCenter(ag)
               ∨ nam = declassify-count(`declassifyCCD') ∧ exCreditCardCenter(ag));
      used for : s, ls;
       
      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));
      used for : s, ls;
       
      observe-HighLow5 :  ⊦ observe(HighLow5, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`state6') ∧ exAirline(ag));
      used for : s, ls;
       
      alter-HighLow5 :  ⊦ alter(HighLow5, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`state6') ∧ exAirline(ag) ∨ nam = state(`state7') ∧ exAirline(ag));
      used for : s, ls;
       
      observe-Abort8 :  ⊦ observe(Abort8, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`pre8') ∧ exUser(ag));
      used for : s, ls;
       
      alter-Abort8 :  ⊦ alter(Abort8, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`pre8') ∧ exUser(ag) ∨ nam = state(`init') ∧ exUser(ag));
      used for : s, ls;
       
      observe-Abort9 :  ⊦ observe(Abort9, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`pre9') ∧ exUser(ag));
      used for : s, ls;
       
      alter-Abort9 :  ⊦ alter(Abort9, nam, ag) ↔ ¬ ¬ (false ∨ nam = state(`pre9') ∧ exUser(ag) ∨ nam = state(`init') ∧ exUser(ag));
      used for : s, ls;
       
end enrich