enrich domains , 
       namefuns with
   functions 
      dom : action → domain;
      dom : name × Agent → domain;
   predicates 
      isDeclassDom : domain;
      isStateDom : domain;
      usedDom : domain;
   
   axioms 
      isDeclassDom-def :  ⊦ isDeclassDom(domvar) ↔ ¬ domvar ≠ User->User_Airline;
      used for : s, ls;
       
      isStateDom-def :  ⊦ isStateDom(domvar) ↔ ¬ ¬ (domvar = HighLow5 ∨ domvar = Abort8 ∨ domvar = Abort9);
      used for : s, ls;
       
      usedDom-def :  ⊦ usedDom(domvar) ↔ (∃ a. dom(a) = domvar);
      usedDom-constructive
      : ⊦ 
          usedDom(domvar)
        ↔ ¬ ¬ (  isAbort9(domvar) ∨ isAbort8(domvar) ∨ isHighLow5(domvar) ∨ isUser_Airline(domvar) ∨ isUser->User_Airline(domvar)
               ∨ isUser_TravelAgency_Airline(domvar) ∨ isUser(domvar));
      used for : s, ls, generated;
       
      dom-flightOffers :  ⊦ dom(Airline-flightOffers, mkAirline(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-ccd :  ⊦ dom(CreditCardCenter-ccd, mkCreditCardCenter(n)) = User;
      used for : s, ls;
       
      dom-Mailbox-GetFlightOffers :  ⊦ dom(Mailbox(GetFlightOffers-TravelPlannerCmd), mkTravelPlanner(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-DeclassifiedCCD :  ⊦ dom(Mailbox(DeclassifiedCCD-TravelPlannerCmd), mkTravelPlanner(n)) = User_Airline;
      used for : s, ls;
       
      dom-Mailbox-OkConfirmBooking :  ⊦ dom(Mailbox(OkConfirmBooking-TravelPlannerCmd), mkTravelPlanner(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-GetFlightOffers :  ⊦ dom(Mailbox(GetFlightOffers-TravelAgencyCmd), mkTravelAgency(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-RetFlightOffers :  ⊦ dom(Mailbox(RetFlightOffers-TravelAgencyCmd), mkTravelAgency(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-PayCommission :  ⊦ dom(Mailbox(PayCommission-TravelAgencyCmd), mkTravelAgency(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-ReleaseCCD :  ⊦ dom(Mailbox(ReleaseCCD-CreditCardCenterCmd), mkCreditCardCenter(n)) = User;
      used for : s, ls;
       
      dom-Mailbox-GetDeclassifiedCCD :  ⊦ dom(Mailbox(GetDeclassifiedCCD-CreditCardCenterCmd), mkCreditCardCenter(n)) = User;
      used for : s, ls;
       
      dom-Mailbox-GetFlightOffers :  ⊦ dom(Mailbox(GetFlightOffers-AirlineCmd), mkAirline(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-OkPayCommission :  ⊦ dom(Mailbox(OkPayCommission-AirlineCmd), mkAirline(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-GetInputRequestData :  ⊦ dom(Mailbox(GetInputRequestData-UserCmd-1), mkUser(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-GetSingleSelection :  ⊦ dom(Mailbox(GetSingleSelection-UserCmd-2), mkUser(n)) = User_Airline;
      used for : s, ls;
       
      dom-Mailbox-ConfirmRelease :  ⊦ dom(Mailbox(ConfirmRelease-UserCmd-3), mkUser(n)) = User;
      used for : s, ls;
       
      dom-Mailbox-Confirm :  ⊦ dom(Mailbox(Confirm-UserCmd-4), mkUser(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-RetFlightOffers :  ⊦ dom(Mailbox(RetFlightOffers-TravelPlannerCmd), mkTravelPlanner(n)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-Mailbox-BookSelected :  ⊦ dom(Mailbox(BookSelected-TravelPlannerCmd), mkTravelPlanner(n)) = User_Airline;
      used for : s, ls;
       
      dom-Mailbox-BookFlightOffer :  ⊦ dom(Mailbox(BookFlightOffer-AirlineCmd), mkAirline(n)) = User_Airline;
      used for : s, ls;
       
      dom-Init-GetInputRequestData-TravelPlannerCmd :  ⊦ dom(Action(ag0, Init-GetInputRequestData-TravelPlannerCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-GetFlightOffers-TravelPlannerCmd :  ⊦ dom(Action(ag0, GetFlightOffers-TravelPlannerCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-RetFlightOffersstate1-TravelPlannerCmd :  ⊦ dom(Action(ag0, RetFlightOffersstate1-TravelPlannerCmd, ag1)) = User_Airline;
      used for : s, ls;
       
      dom-BookSelectedstate2-TravelPlannerCmd :  ⊦ dom(Action(ag0, BookSelectedstate2-TravelPlannerCmd, ag1)) = User;
      used for : s, ls;
       
      dom-DeclassifiedCCD-TravelPlannerCmd :  ⊦ dom(Action(ag0, DeclassifiedCCD-TravelPlannerCmd, ag1)) = User_Airline;
      used for : s, ls;
       
      dom-OkConfirmBooking-TravelPlannerCmd :  ⊦ dom(Action(ag0, OkConfirmBooking-TravelPlannerCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-GetFlightOffers-TravelAgencyCmd :  ⊦ dom(Action(ag0, GetFlightOffers-TravelAgencyCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-RetFlightOffers-TravelAgencyCmd :  ⊦ dom(Action(ag0, RetFlightOffers-TravelAgencyCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-PayCommission-TravelAgencyCmd :  ⊦ dom(Action(ag0, PayCommission-TravelAgencyCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-ReleaseCCD-CreditCardCenterCmd :  ⊦ dom(Action(ag0, ReleaseCCD-CreditCardCenterCmd, ag1)) = User;
      used for : s, ls;
       
      dom-GetDeclassifiedCCD-CreditCardCenterCmd :  ⊦ dom(Action(ag0, GetDeclassifiedCCD-CreditCardCenterCmd, ag1)) = User;
      used for : s, ls;
       
      dom-GetFlightOffers-AirlineCmd :  ⊦ dom(Action(ag0, GetFlightOffers-AirlineCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-BookFlightOfferstate7-AirlineCmd :  ⊦ dom(Action(ag0, BookFlightOfferstate7-AirlineCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-OkPayCommission-AirlineCmd :  ⊦ dom(Action(ag0, OkPayCommission-AirlineCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-GetInputRequestData-UserCmd-1 :  ⊦ dom(Action(ag0, GetInputRequestData-UserCmd-1, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-GetSingleSelection-UserCmd-2 :  ⊦ dom(Action(ag0, GetSingleSelection-UserCmd-2, ag1)) = User_Airline;
      used for : s, ls;
       
      dom-ConfirmRelease-UserCmd-3 :  ⊦ dom(Action(ag0, ConfirmRelease-UserCmd-3, ag1)) = User;
      used for : s, ls;
       
      dom-Confirm-UserCmd-4 :  ⊦ dom(Action(ag0, Confirm-UserCmd-4, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-RetFlightOffers-TravelPlannerCmd :  ⊦ dom(Action(ag0, RetFlightOffers-TravelPlannerCmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls;
       
      dom-BookSelected-TravelPlannerCmd :  ⊦ dom(Action(ag0, BookSelected-TravelPlannerCmd, ag1)) = User_Airline;
      used for : s, ls;
       
      dom-declassifyCCD4ASM-CreditCardCenterCmd :  ⊦ dom(Action(ag0, declassifyCCD4ASM-CreditCardCenterCmd, ag1)) = User->User_Airline;
      used for : s, ls;
       
      dom-afterdeclassifyCCD4ASM-CreditCardCenterCmd :  ⊦ dom(Action(ag0, afterdeclassifyCCD4ASM-CreditCardCenterCmd, ag1)) = User_Airline;
      used for : s, ls;
       
      dom-BookFlightOffer-AirlineCmd :  ⊦ dom(Action(ag0, BookFlightOffer-AirlineCmd, ag1)) = User_Airline;
      used for : s, ls;
       
      dom-BookFlightOfferstate6-AirlineCmd :  ⊦ dom(Action(ag0, BookFlightOfferstate6-AirlineCmd, ag1)) = HighLow5;
      used for : s, ls;
       
      dom-Abort8-UserCmd :  ⊦ dom(Action(ag0, Abort8-UserCmd, ag1)) = Abort8;
      used for : s, ls;
       
      dom-Abort9-UserCmd :  ⊦ dom(Action(ag0, Abort9-UserCmd, ag1)) = Abort9;
      used for : s, ls;
       
      dom-isInit-GetInputRequestData-TravelPlannerCmd
      :  ⊦ isInit-GetInputRequestData-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isGetFlightOffers-TravelPlannerCmd :  ⊦ isGetFlightOffers-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isRetFlightOffersstate1-TravelPlannerCmd :  ⊦ isRetFlightOffersstate1-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline;
      used for : s, ls, generated;
       
      dom-isBookSelectedstate2-TravelPlannerCmd :  ⊦ isBookSelectedstate2-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User;
      used for : s, ls, generated;
       
      dom-isDeclassifiedCCD-TravelPlannerCmd :  ⊦ isDeclassifiedCCD-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline;
      used for : s, ls, generated;
       
      dom-isOkConfirmBooking-TravelPlannerCmd :  ⊦ isOkConfirmBooking-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isGetFlightOffers-TravelAgencyCmd :  ⊦ isGetFlightOffers-TravelAgencyCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isRetFlightOffers-TravelAgencyCmd :  ⊦ isRetFlightOffers-TravelAgencyCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isPayCommission-TravelAgencyCmd :  ⊦ isPayCommission-TravelAgencyCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isReleaseCCD-CreditCardCenterCmd :  ⊦ isReleaseCCD-CreditCardCenterCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User;
      used for : s, ls, generated;
       
      dom-isGetDeclassifiedCCD-CreditCardCenterCmd :  ⊦ isGetDeclassifiedCCD-CreditCardCenterCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User;
      used for : s, ls, generated;
       
      dom-isGetFlightOffers-AirlineCmd :  ⊦ isGetFlightOffers-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isBookFlightOfferstate7-AirlineCmd :  ⊦ isBookFlightOfferstate7-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isOkPayCommission-AirlineCmd :  ⊦ isOkPayCommission-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isGetInputRequestData-UserCmd-1 :  ⊦ isGetInputRequestData-UserCmd-1(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isGetSingleSelection-UserCmd-2 :  ⊦ isGetSingleSelection-UserCmd-2(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline;
      used for : s, ls, generated;
       
      dom-isConfirmRelease-UserCmd-3 :  ⊦ isConfirmRelease-UserCmd-3(cmd) → dom(Action(ag0, cmd, ag1)) = User;
      used for : s, ls, generated;
       
      dom-isConfirm-UserCmd-4 :  ⊦ isConfirm-UserCmd-4(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isRetFlightOffers-TravelPlannerCmd :  ⊦ isRetFlightOffers-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_TravelAgency_Airline;
      used for : s, ls, generated;
       
      dom-isBookSelected-TravelPlannerCmd :  ⊦ isBookSelected-TravelPlannerCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline;
      used for : s, ls, generated;
       
      dom-isdeclassifyCCD4ASM-CreditCardCenterCmd :  ⊦ isdeclassifyCCD4ASM-CreditCardCenterCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User->User_Airline;
      used for : s, ls, generated;
       
      dom-isafterdeclassifyCCD4ASM-CreditCardCenterCmd
      :  ⊦ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline;
      used for : s, ls, generated;
       
      dom-isBookFlightOffer-AirlineCmd :  ⊦ isBookFlightOffer-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = User_Airline;
      used for : s, ls, generated;
       
      dom-isBookFlightOfferstate6-AirlineCmd :  ⊦ isBookFlightOfferstate6-AirlineCmd(cmd) → dom(Action(ag0, cmd, ag1)) = HighLow5;
      used for : s, ls, generated;
       
      dom-isAbort8-UserCmd :  ⊦ isAbort8-UserCmd(cmd) → dom(Action(ag0, cmd, ag1)) = Abort8;
      used for : s, ls, generated;
       
      dom-isAbort9-UserCmd :  ⊦ isAbort9-UserCmd(cmd) → dom(Action(ag0, cmd, ag1)) = Abort9;
      used for : s, ls, generated;
       
end enrich