enrich observeAlter with
   predicates 
      eqd : (name × Agent → Data) × domain × (name × Agent → Data);
      eqdAirline : (name × Agent → Data) × name × (name × Agent → Data);
      eqdCreditCardCenter : (name × Agent → Data) × name × (name × Agent → Data);
      eqdTravelAgency : (name × Agent → Data) × name × (name × Agent → Data);
      eqdTravelPlanner : (name × Agent → Data) × name × (name × Agent → Data);
      eqdUser : (name × Agent → Data) × name × (name × Agent → Data);
   
   axioms 
      eqd-def :  ⊦ eqd(s, domvar, s0) ↔ (∀ nam, ag. observe(domvar, nam, ag) → s(nam, ag) = s0(nam, ag));
      used for : ls;
       
      eqdAirline-def :  ⊦ eqdAirline(s, nam, s0) ↔ (∀ ag. exAirline(ag) → s(nam, ag) = s0(nam, ag));
      used for : ls;
       
      eqdAirline-forward :  ⊦ eqdAirline(s, nam, s0) → s0(nam, mkAirline(0)) = s(nam, mkAirline(0));
      used for : f, lf, generated;
       
      eqdCreditCardCenter-def :  ⊦ eqdCreditCardCenter(s, nam, s0) ↔ (∀ ag. exCreditCardCenter(ag) → s(nam, ag) = s0(nam, ag));
      used for : ls;
       
      eqdCreditCardCenter-forward :  ⊦ eqdCreditCardCenter(s, nam, s0) ∧ exCreditCardCenter(ag) → s0(nam, ag) = s(nam, ag);
      used for : f, lf, generated;
       
      eqdTravelAgency-def :  ⊦ eqdTravelAgency(s, nam, s0) ↔ (∀ ag. exTravelAgency(ag) → s(nam, ag) = s0(nam, ag));
      used for : ls;
       
      eqdTravelAgency-forward :  ⊦ eqdTravelAgency(s, nam, s0) → s0(nam, mkTravelAgency(0)) = s(nam, mkTravelAgency(0));
      used for : f, lf, generated;
       
      eqdTravelPlanner-def :  ⊦ eqdTravelPlanner(s, nam, s0) ↔ (∀ ag. exTravelPlanner(ag) → s(nam, ag) = s0(nam, ag));
      used for : ls;
       
      eqdTravelPlanner-forward :  ⊦ eqdTravelPlanner(s, nam, s0) ∧ exTravelPlanner(ag) → s0(nam, ag) = s(nam, ag);
      used for : f, lf, generated;
       
      eqdUser-def :  ⊦ eqdUser(s, nam, s0) ↔ (∀ ag. exUser(ag) → s(nam, ag) = s0(nam, ag));
      used for : ls;
       
      eqdUser-forward :  ⊦ eqdUser(s, nam, s0) ∧ exUser(ag) → s0(nam, ag) = s(nam, ag);
      used for : f, lf, generated;
       
      eqd-User
      : ⊦ 
          eqd(s, User, s0)
        ↔ ¬ ¬ (  true ∧ eqdTravelPlanner(s, state(`state2'), s0) ∧ eqdTravelPlanner(s, TravelPlanner-flightOffer, s0)
               ∧ eqdCreditCardCenter(s, Mailbox(ReleaseCCD-CreditCardCenterCmd), s0) ∧ eqdCreditCardCenter(s, CreditCardCenter-ccd, s0)
               ∧ eqdCreditCardCenter(s, locVar(`airline'), s0) ∧ eqdCreditCardCenter(s, Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd), s0)
               ∧ eqdUser(s, Mailbox(ConfirmRelease-UserCmd-3), s0) ∧ eqdUser(s, User-ConfirmRelease(`3'), s0)
               ∧ eqdUser(s, User-ConfirmRelease-count(`3'), s0) ∧ eqdUser(s, User-ConfirmReleases(`3'), s0)
               ∧ eqdUser(s, User-ConfirmedRelease-count(`3'), s0));
      used for : s, ls, generated;
       
      eqd-User_Airline
      : ⊦ 
          eqd(s, User_Airline, s0)
        ↔ ¬ ¬ (  true ∧ eqdTravelPlanner(s, state(`state1'), s0) ∧ eqdTravelPlanner(s, locVar(`flightOffers'), s0)
               ∧ eqdTravelPlanner(s, Mailbox(DeclassifiedCCD-TravelPlannerCmd), s0) ∧ eqdTravelPlanner(s, TravelPlanner-flightOffer, s0)
               ∧ eqdTravelPlanner(s, locVar(`ccd_decl'), s0) ∧ eqdUser(s, Mailbox(GetSingleSelection-UserCmd-2), s0)
               ∧ eqdUser(s, User-GetSingleSelection(`2'), s0) ∧ eqdUser(s, User-GetSingleSelection-count(`2'), s0)
               ∧ eqdUser(s, User-GetSingleSelections(`2'), s0) ∧ eqdTravelPlanner(s, Mailbox(BookSelected-TravelPlannerCmd), s0)
               ∧ eqdCreditCardCenter(s, state(`state4'), s0) ∧ eqdCreditCardCenter(s, locVar(`ccd_decl'), s0)
               ∧ eqdAirline(s, Mailbox(BookFlightOffer-AirlineCmd), s0) ∧ eqdAirline(s, locVar(`id'), s0) ∧ eqdAirline(s, locVar(`ccd_decl'), s0));
      used for : s, ls, generated;
       
      eqd-User_TravelAgency_Airline
      : ⊦ 
          eqd(s, User_TravelAgency_Airline, s0)
        ↔ ¬ ¬ (  true ∧ eqdUser(s, state(`init'), s0) ∧ eqdTravelPlanner(s, Mailbox(GetFlightOffers-TravelPlannerCmd), s0)
               ∧ eqdTravelPlanner(s, locVar(`requestData'), s0) ∧ eqdTravelPlanner(s, Mailbox(OkConfirmBooking-TravelPlannerCmd), s0)
               ∧ eqdTravelAgency(s, Mailbox(GetFlightOffers-TravelAgencyCmd), s0) ∧ eqdTravelAgency(s, locVar(`requestData'), s0)
               ∧ eqdTravelAgency(s, Mailbox(RetFlightOffers-TravelAgencyCmd), s0) ∧ eqdTravelAgency(s, locVar(`flightOffers'), s0)
               ∧ eqdTravelAgency(s, Mailbox(PayCommission-TravelAgencyCmd), s0) ∧ eqdAirline(s, Mailbox(GetFlightOffers-AirlineCmd), s0)
               ∧ eqdAirline(s, locVar(`requestData'), s0) ∧ eqdAirline(s, Airline-flightOffers, s0)
               ∧ eqdAirline(s, locVar(`filteredFlightOffers'), s0) ∧ eqdAirline(s, state(`state7'), s0)
               ∧ eqdAirline(s, Mailbox(OkPayCommission-AirlineCmd), s0) ∧ eqdUser(s, Mailbox(GetInputRequestData-UserCmd-1), s0)
               ∧ eqdUser(s, User-GetInput(`1'), s0) ∧ eqdUser(s, User-GetInput-count(`1'), s0) ∧ eqdUser(s, User-GetInputs(`1'), s0)
               ∧ eqdUser(s, Mailbox(Confirm-UserCmd-4), s0) ∧ eqdUser(s, User-Confirm(`4'), s0) ∧ eqdUser(s, User-Confirm-count(`4'), s0)
               ∧ eqdUser(s, User-Confirms(`4'), s0) ∧ eqdTravelPlanner(s, Mailbox(RetFlightOffers-TravelPlannerCmd), s0));
      used for : s, ls, generated;
       
      eqd-User-User_Airline
      : ⊦ 
          eqd(s, User->User_Airline, s0)
        ↔ ¬ ¬ (  true ∧ eqdCreditCardCenter(s, state(`state3'), s0) ∧ eqdCreditCardCenter(s, CreditCardCenter-ccd, s0)
               ∧ eqdCreditCardCenter(s, declassify-count(`declassifyCCD'), s0));
      used for : s, ls, generated;
       
      eqd-HighLow5 :  ⊦ eqd(s, HighLow5, s0) ↔ ¬ ¬ (true ∧ eqdAirline(s, state(`state6'), s0));
      used for : s, ls, generated;
       
      eqd-Abort8 :  ⊦ eqd(s, Abort8, s0) ↔ ¬ ¬ (true ∧ eqdUser(s, state(`pre8'), s0));
      used for : s, ls, generated;
       
      eqd-Abort9 :  ⊦ eqd(s, Abort9, s0) ↔ ¬ ¬ (true ∧ eqdUser(s, state(`pre9'), s0));
      used for : s, ls, generated;
       
end enrich