This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| disj-01 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ GetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-02 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ RetFlightOffersstate1-TravelPlannerCmd | An Axiom |
| disj-03 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ BookSelectedstate2-TravelPlannerCmd | An Axiom |
| disj-04 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ DeclassifiedCCD-TravelPlannerCmd | An Axiom |
| disj-05 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ OkConfirmBooking-TravelPlannerCmd | An Axiom |
| disj-06 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ GetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-07 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ RetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-08 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ PayCommission-TravelAgencyCmd | An Axiom |
| disj-09 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-10 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-11 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-12 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-13 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-14 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-15 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-16 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-17 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-18 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-19 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-20 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-21 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-22 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-23 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-24 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ Abort8-UserCmd | An Axiom |
| disj-25 | ⊦ Init-GetInputRequestData-TravelPlannerCmd ≠ Abort9-UserCmd | An Axiom |
| disj-26 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ RetFlightOffersstate1-TravelPlannerCmd | An Axiom |
| disj-27 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ BookSelectedstate2-TravelPlannerCmd | An Axiom |
| disj-28 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ DeclassifiedCCD-TravelPlannerCmd | An Axiom |
| disj-29 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ OkConfirmBooking-TravelPlannerCmd | An Axiom |
| disj-30 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ GetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-31 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ RetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-32 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ PayCommission-TravelAgencyCmd | An Axiom |
| disj-33 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-34 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-35 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-36 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-37 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-38 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-39 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-40 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-41 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-42 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-43 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-44 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-45 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-46 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-47 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-48 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ Abort8-UserCmd | An Axiom |
| disj-49 | ⊦ GetFlightOffers-TravelPlannerCmd ≠ Abort9-UserCmd | An Axiom |
| disj-50 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ BookSelectedstate2-TravelPlannerCmd | An Axiom |
| disj-51 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ DeclassifiedCCD-TravelPlannerCmd | An Axiom |
| disj-52 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ OkConfirmBooking-TravelPlannerCmd | An Axiom |
| disj-53 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ GetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-54 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ RetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-55 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ PayCommission-TravelAgencyCmd | An Axiom |
| disj-56 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-57 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-58 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-59 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-60 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-61 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-62 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-63 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-64 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-65 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-66 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-67 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-68 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-69 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-70 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-71 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ Abort8-UserCmd | An Axiom |
| disj-72 | ⊦ RetFlightOffersstate1-TravelPlannerCmd ≠ Abort9-UserCmd | An Axiom |
| disj-73 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ DeclassifiedCCD-TravelPlannerCmd | An Axiom |
| disj-74 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ OkConfirmBooking-TravelPlannerCmd | An Axiom |
| disj-75 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ GetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-76 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ RetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-77 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ PayCommission-TravelAgencyCmd | An Axiom |
| disj-78 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-79 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-80 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-81 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-82 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-83 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-84 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-85 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-86 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-87 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-88 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-89 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-90 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-91 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-92 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-93 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ Abort8-UserCmd | An Axiom |
| disj-94 | ⊦ BookSelectedstate2-TravelPlannerCmd ≠ Abort9-UserCmd | An Axiom |
| disj-95 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ OkConfirmBooking-TravelPlannerCmd | An Axiom |
| disj-96 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ GetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-97 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ RetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-98 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ PayCommission-TravelAgencyCmd | An Axiom |
| disj-99 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-100 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-101 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-102 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-103 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-104 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-105 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-106 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-107 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-108 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-109 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-110 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-111 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-112 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-113 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-114 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ Abort8-UserCmd | An Axiom |
| disj-115 | ⊦ DeclassifiedCCD-TravelPlannerCmd ≠ Abort9-UserCmd | An Axiom |
| disj-116 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ GetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-117 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ RetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-118 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ PayCommission-TravelAgencyCmd | An Axiom |
| disj-119 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-120 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-121 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-122 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-123 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-124 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-125 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-126 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-127 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-128 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-129 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-130 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-131 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-132 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-133 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-134 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ Abort8-UserCmd | An Axiom |
| disj-135 | ⊦ OkConfirmBooking-TravelPlannerCmd ≠ Abort9-UserCmd | An Axiom |
| disj-136 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ RetFlightOffers-TravelAgencyCmd | An Axiom |
| disj-137 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ PayCommission-TravelAgencyCmd | An Axiom |
| disj-138 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-139 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-140 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-141 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-142 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-143 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-144 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-145 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-146 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-147 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-148 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-149 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-150 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-151 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-152 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-153 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ Abort8-UserCmd | An Axiom |
| disj-154 | ⊦ GetFlightOffers-TravelAgencyCmd ≠ Abort9-UserCmd | An Axiom |
| disj-155 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ PayCommission-TravelAgencyCmd | An Axiom |
| disj-156 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-157 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-158 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-159 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-160 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-161 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-162 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-163 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-164 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-165 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-166 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-167 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-168 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-169 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-170 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-171 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ Abort8-UserCmd | An Axiom |
| disj-172 | ⊦ RetFlightOffers-TravelAgencyCmd ≠ Abort9-UserCmd | An Axiom |
| disj-173 | ⊦ PayCommission-TravelAgencyCmd ≠ ReleaseCCD-CreditCardCenterCmd | An Axiom |
| disj-174 | ⊦ PayCommission-TravelAgencyCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-175 | ⊦ PayCommission-TravelAgencyCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-176 | ⊦ PayCommission-TravelAgencyCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-177 | ⊦ PayCommission-TravelAgencyCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-178 | ⊦ PayCommission-TravelAgencyCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-179 | ⊦ PayCommission-TravelAgencyCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-180 | ⊦ PayCommission-TravelAgencyCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-181 | ⊦ PayCommission-TravelAgencyCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-182 | ⊦ PayCommission-TravelAgencyCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-183 | ⊦ PayCommission-TravelAgencyCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-184 | ⊦ PayCommission-TravelAgencyCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-185 | ⊦ PayCommission-TravelAgencyCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-186 | ⊦ PayCommission-TravelAgencyCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-187 | ⊦ PayCommission-TravelAgencyCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-188 | ⊦ PayCommission-TravelAgencyCmd ≠ Abort8-UserCmd | An Axiom |
| disj-189 | ⊦ PayCommission-TravelAgencyCmd ≠ Abort9-UserCmd | An Axiom |
| disj-190 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| disj-191 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-192 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-193 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-194 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-195 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-196 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-197 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-198 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-199 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-200 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-201 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-202 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-203 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-204 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ Abort8-UserCmd | An Axiom |
| disj-205 | ⊦ ReleaseCCD-CreditCardCenterCmd ≠ Abort9-UserCmd | An Axiom |
| disj-206 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ GetFlightOffers-AirlineCmd | An Axiom |
| disj-207 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-208 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-209 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-210 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-211 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-212 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-213 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-214 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-215 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-216 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-217 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-218 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-219 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ Abort8-UserCmd | An Axiom |
| disj-220 | ⊦ GetDeclassifiedCCD-CreditCardCenterCmd ≠ Abort9-UserCmd | An Axiom |
| disj-221 | ⊦ GetFlightOffers-AirlineCmd ≠ BookFlightOfferstate7-AirlineCmd | An Axiom |
| disj-222 | ⊦ GetFlightOffers-AirlineCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-223 | ⊦ GetFlightOffers-AirlineCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-224 | ⊦ GetFlightOffers-AirlineCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-225 | ⊦ GetFlightOffers-AirlineCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-226 | ⊦ GetFlightOffers-AirlineCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-227 | ⊦ GetFlightOffers-AirlineCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-228 | ⊦ GetFlightOffers-AirlineCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-229 | ⊦ GetFlightOffers-AirlineCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-230 | ⊦ GetFlightOffers-AirlineCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-231 | ⊦ GetFlightOffers-AirlineCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-232 | ⊦ GetFlightOffers-AirlineCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-233 | ⊦ GetFlightOffers-AirlineCmd ≠ Abort8-UserCmd | An Axiom |
| disj-234 | ⊦ GetFlightOffers-AirlineCmd ≠ Abort9-UserCmd | An Axiom |
| disj-235 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ OkPayCommission-AirlineCmd | An Axiom |
| disj-236 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-237 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-238 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-239 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-240 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-241 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-242 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-243 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-244 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-245 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-246 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ Abort8-UserCmd | An Axiom |
| disj-247 | ⊦ BookFlightOfferstate7-AirlineCmd ≠ Abort9-UserCmd | An Axiom |
| disj-248 | ⊦ OkPayCommission-AirlineCmd ≠ GetInputRequestData-UserCmd-1 | An Axiom |
| disj-249 | ⊦ OkPayCommission-AirlineCmd ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-250 | ⊦ OkPayCommission-AirlineCmd ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-251 | ⊦ OkPayCommission-AirlineCmd ≠ Confirm-UserCmd-4 | An Axiom |
| disj-252 | ⊦ OkPayCommission-AirlineCmd ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-253 | ⊦ OkPayCommission-AirlineCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-254 | ⊦ OkPayCommission-AirlineCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-255 | ⊦ OkPayCommission-AirlineCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-256 | ⊦ OkPayCommission-AirlineCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-257 | ⊦ OkPayCommission-AirlineCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-258 | ⊦ OkPayCommission-AirlineCmd ≠ Abort8-UserCmd | An Axiom |
| disj-259 | ⊦ OkPayCommission-AirlineCmd ≠ Abort9-UserCmd | An Axiom |
| disj-260 | ⊦ GetInputRequestData-UserCmd-1 ≠ GetSingleSelection-UserCmd-2 | An Axiom |
| disj-261 | ⊦ GetInputRequestData-UserCmd-1 ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-262 | ⊦ GetInputRequestData-UserCmd-1 ≠ Confirm-UserCmd-4 | An Axiom |
| disj-263 | ⊦ GetInputRequestData-UserCmd-1 ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-264 | ⊦ GetInputRequestData-UserCmd-1 ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-265 | ⊦ GetInputRequestData-UserCmd-1 ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-266 | ⊦ GetInputRequestData-UserCmd-1 ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-267 | ⊦ GetInputRequestData-UserCmd-1 ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-268 | ⊦ GetInputRequestData-UserCmd-1 ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-269 | ⊦ GetInputRequestData-UserCmd-1 ≠ Abort8-UserCmd | An Axiom |
| disj-270 | ⊦ GetInputRequestData-UserCmd-1 ≠ Abort9-UserCmd | An Axiom |
| disj-271 | ⊦ GetSingleSelection-UserCmd-2 ≠ ConfirmRelease-UserCmd-3 | An Axiom |
| disj-272 | ⊦ GetSingleSelection-UserCmd-2 ≠ Confirm-UserCmd-4 | An Axiom |
| disj-273 | ⊦ GetSingleSelection-UserCmd-2 ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-274 | ⊦ GetSingleSelection-UserCmd-2 ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-275 | ⊦ GetSingleSelection-UserCmd-2 ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-276 | ⊦ GetSingleSelection-UserCmd-2 ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-277 | ⊦ GetSingleSelection-UserCmd-2 ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-278 | ⊦ GetSingleSelection-UserCmd-2 ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-279 | ⊦ GetSingleSelection-UserCmd-2 ≠ Abort8-UserCmd | An Axiom |
| disj-280 | ⊦ GetSingleSelection-UserCmd-2 ≠ Abort9-UserCmd | An Axiom |
| disj-281 | ⊦ ConfirmRelease-UserCmd-3 ≠ Confirm-UserCmd-4 | An Axiom |
| disj-282 | ⊦ ConfirmRelease-UserCmd-3 ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-283 | ⊦ ConfirmRelease-UserCmd-3 ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-284 | ⊦ ConfirmRelease-UserCmd-3 ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-285 | ⊦ ConfirmRelease-UserCmd-3 ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-286 | ⊦ ConfirmRelease-UserCmd-3 ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-287 | ⊦ ConfirmRelease-UserCmd-3 ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-288 | ⊦ ConfirmRelease-UserCmd-3 ≠ Abort8-UserCmd | An Axiom |
| disj-289 | ⊦ ConfirmRelease-UserCmd-3 ≠ Abort9-UserCmd | An Axiom |
| disj-290 | ⊦ Confirm-UserCmd-4 ≠ RetFlightOffers-TravelPlannerCmd | An Axiom |
| disj-291 | ⊦ Confirm-UserCmd-4 ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-292 | ⊦ Confirm-UserCmd-4 ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-293 | ⊦ Confirm-UserCmd-4 ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-294 | ⊦ Confirm-UserCmd-4 ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-295 | ⊦ Confirm-UserCmd-4 ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-296 | ⊦ Confirm-UserCmd-4 ≠ Abort8-UserCmd | An Axiom |
| disj-297 | ⊦ Confirm-UserCmd-4 ≠ Abort9-UserCmd | An Axiom |
| disj-298 | ⊦ RetFlightOffers-TravelPlannerCmd ≠ BookSelected-TravelPlannerCmd | An Axiom |
| disj-299 | ⊦ RetFlightOffers-TravelPlannerCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-300 | ⊦ RetFlightOffers-TravelPlannerCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-301 | ⊦ RetFlightOffers-TravelPlannerCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-302 | ⊦ RetFlightOffers-TravelPlannerCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-303 | ⊦ RetFlightOffers-TravelPlannerCmd ≠ Abort8-UserCmd | An Axiom |
| disj-304 | ⊦ RetFlightOffers-TravelPlannerCmd ≠ Abort9-UserCmd | An Axiom |
| disj-305 | ⊦ BookSelected-TravelPlannerCmd ≠ declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-306 | ⊦ BookSelected-TravelPlannerCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-307 | ⊦ BookSelected-TravelPlannerCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-308 | ⊦ BookSelected-TravelPlannerCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-309 | ⊦ BookSelected-TravelPlannerCmd ≠ Abort8-UserCmd | An Axiom |
| disj-310 | ⊦ BookSelected-TravelPlannerCmd ≠ Abort9-UserCmd | An Axiom |
| disj-311 | ⊦ declassifyCCD4ASM-CreditCardCenterCmd ≠ afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| disj-312 | ⊦ declassifyCCD4ASM-CreditCardCenterCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-313 | ⊦ declassifyCCD4ASM-CreditCardCenterCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-314 | ⊦ declassifyCCD4ASM-CreditCardCenterCmd ≠ Abort8-UserCmd | An Axiom |
| disj-315 | ⊦ declassifyCCD4ASM-CreditCardCenterCmd ≠ Abort9-UserCmd | An Axiom |
| disj-316 | ⊦ afterdeclassifyCCD4ASM-CreditCardCenterCmd ≠ BookFlightOffer-AirlineCmd | An Axiom |
| disj-317 | ⊦ afterdeclassifyCCD4ASM-CreditCardCenterCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-318 | ⊦ afterdeclassifyCCD4ASM-CreditCardCenterCmd ≠ Abort8-UserCmd | An Axiom |
| disj-319 | ⊦ afterdeclassifyCCD4ASM-CreditCardCenterCmd ≠ Abort9-UserCmd | An Axiom |
| disj-320 | ⊦ BookFlightOffer-AirlineCmd ≠ BookFlightOfferstate6-AirlineCmd | An Axiom |
| disj-321 | ⊦ BookFlightOffer-AirlineCmd ≠ Abort8-UserCmd | An Axiom |
| disj-322 | ⊦ BookFlightOffer-AirlineCmd ≠ Abort9-UserCmd | An Axiom |
| disj-323 | ⊦ BookFlightOfferstate6-AirlineCmd ≠ Abort8-UserCmd | An Axiom |
| disj-324 | ⊦ BookFlightOfferstate6-AirlineCmd ≠ Abort9-UserCmd | An Axiom |
| disj-325 | ⊦ Abort8-UserCmd ≠ Abort9-UserCmd | An Axiom |
| test-01 | ⊦ isAbort9-UserCmd(Abort9-UserCmd) | An Axiom |
| test-02 | ⊦ ¬ isAbort9-UserCmd(Abort8-UserCmd) | An Axiom |
| test-03 | ⊦ ¬ isAbort9-UserCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-04 | ⊦ ¬ isAbort9-UserCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-05 | ⊦ ¬ isAbort9-UserCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-06 | ⊦ ¬ isAbort9-UserCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-07 | ⊦ ¬ isAbort9-UserCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-08 | ⊦ ¬ isAbort9-UserCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-09 | ⊦ ¬ isAbort9-UserCmd(Confirm-UserCmd-4) | An Axiom |
| test-10 | ⊦ ¬ isAbort9-UserCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-11 | ⊦ ¬ isAbort9-UserCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-12 | ⊦ ¬ isAbort9-UserCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-13 | ⊦ ¬ isAbort9-UserCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-14 | ⊦ ¬ isAbort9-UserCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-15 | ⊦ ¬ isAbort9-UserCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-16 | ⊦ ¬ isAbort9-UserCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-17 | ⊦ ¬ isAbort9-UserCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-18 | ⊦ ¬ isAbort9-UserCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-19 | ⊦ ¬ isAbort9-UserCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-20 | ⊦ ¬ isAbort9-UserCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-21 | ⊦ ¬ isAbort9-UserCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-22 | ⊦ ¬ isAbort9-UserCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-23 | ⊦ ¬ isAbort9-UserCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-24 | ⊦ ¬ isAbort9-UserCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-25 | ⊦ ¬ isAbort9-UserCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-26 | ⊦ ¬ isAbort9-UserCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-27 | ⊦ ¬ isAbort8-UserCmd(Abort9-UserCmd) | An Axiom |
| test-28 | ⊦ isAbort8-UserCmd(Abort8-UserCmd) | An Axiom |
| test-29 | ⊦ ¬ isAbort8-UserCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-30 | ⊦ ¬ isAbort8-UserCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-31 | ⊦ ¬ isAbort8-UserCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-32 | ⊦ ¬ isAbort8-UserCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-33 | ⊦ ¬ isAbort8-UserCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-34 | ⊦ ¬ isAbort8-UserCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-35 | ⊦ ¬ isAbort8-UserCmd(Confirm-UserCmd-4) | An Axiom |
| test-36 | ⊦ ¬ isAbort8-UserCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-37 | ⊦ ¬ isAbort8-UserCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-38 | ⊦ ¬ isAbort8-UserCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-39 | ⊦ ¬ isAbort8-UserCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-40 | ⊦ ¬ isAbort8-UserCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-41 | ⊦ ¬ isAbort8-UserCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-42 | ⊦ ¬ isAbort8-UserCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-43 | ⊦ ¬ isAbort8-UserCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-44 | ⊦ ¬ isAbort8-UserCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-45 | ⊦ ¬ isAbort8-UserCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-46 | ⊦ ¬ isAbort8-UserCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-47 | ⊦ ¬ isAbort8-UserCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-48 | ⊦ ¬ isAbort8-UserCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-49 | ⊦ ¬ isAbort8-UserCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-50 | ⊦ ¬ isAbort8-UserCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-51 | ⊦ ¬ isAbort8-UserCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-52 | ⊦ ¬ isAbort8-UserCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-53 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(Abort9-UserCmd) | An Axiom |
| test-54 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(Abort8-UserCmd) | An Axiom |
| test-55 | ⊦ isBookFlightOfferstate6-AirlineCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-56 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-57 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-58 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-59 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-60 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-61 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(Confirm-UserCmd-4) | An Axiom |
| test-62 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-63 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-64 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-65 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-66 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-67 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-68 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-69 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-70 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-71 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-72 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-73 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-74 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-75 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-76 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-77 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-78 | ⊦ ¬ isBookFlightOfferstate6-AirlineCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-79 | ⊦ ¬ isBookFlightOffer-AirlineCmd(Abort9-UserCmd) | An Axiom |
| test-80 | ⊦ ¬ isBookFlightOffer-AirlineCmd(Abort8-UserCmd) | An Axiom |
| test-81 | ⊦ ¬ isBookFlightOffer-AirlineCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-82 | ⊦ isBookFlightOffer-AirlineCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-83 | ⊦ ¬ isBookFlightOffer-AirlineCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-84 | ⊦ ¬ isBookFlightOffer-AirlineCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-85 | ⊦ ¬ isBookFlightOffer-AirlineCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-86 | ⊦ ¬ isBookFlightOffer-AirlineCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-87 | ⊦ ¬ isBookFlightOffer-AirlineCmd(Confirm-UserCmd-4) | An Axiom |
| test-88 | ⊦ ¬ isBookFlightOffer-AirlineCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-89 | ⊦ ¬ isBookFlightOffer-AirlineCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-90 | ⊦ ¬ isBookFlightOffer-AirlineCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-91 | ⊦ ¬ isBookFlightOffer-AirlineCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-92 | ⊦ ¬ isBookFlightOffer-AirlineCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-93 | ⊦ ¬ isBookFlightOffer-AirlineCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-94 | ⊦ ¬ isBookFlightOffer-AirlineCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-95 | ⊦ ¬ isBookFlightOffer-AirlineCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-96 | ⊦ ¬ isBookFlightOffer-AirlineCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-97 | ⊦ ¬ isBookFlightOffer-AirlineCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-98 | ⊦ ¬ isBookFlightOffer-AirlineCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-99 | ⊦ ¬ isBookFlightOffer-AirlineCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-100 | ⊦ ¬ isBookFlightOffer-AirlineCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-101 | ⊦ ¬ isBookFlightOffer-AirlineCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-102 | ⊦ ¬ isBookFlightOffer-AirlineCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-103 | ⊦ ¬ isBookFlightOffer-AirlineCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-104 | ⊦ ¬ isBookFlightOffer-AirlineCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-105 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(Abort9-UserCmd) | An Axiom |
| test-106 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(Abort8-UserCmd) | An Axiom |
| test-107 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-108 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-109 | ⊦ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-110 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-111 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-112 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-113 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(Confirm-UserCmd-4) | An Axiom |
| test-114 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-115 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-116 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-117 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-118 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-119 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-120 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-121 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-122 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-123 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-124 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-125 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-126 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-127 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-128 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-129 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-130 | ⊦ ¬ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-131 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(Abort9-UserCmd) | An Axiom |
| test-132 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(Abort8-UserCmd) | An Axiom |
| test-133 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-134 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-135 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-136 | ⊦ isdeclassifyCCD4ASM-CreditCardCenterCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-137 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-138 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-139 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(Confirm-UserCmd-4) | An Axiom |
| test-140 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-141 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-142 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-143 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-144 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-145 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-146 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-147 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-148 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-149 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-150 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-151 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-152 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-153 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-154 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-155 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-156 | ⊦ ¬ isdeclassifyCCD4ASM-CreditCardCenterCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-157 | ⊦ ¬ isBookSelected-TravelPlannerCmd(Abort9-UserCmd) | An Axiom |
| test-158 | ⊦ ¬ isBookSelected-TravelPlannerCmd(Abort8-UserCmd) | An Axiom |
| test-159 | ⊦ ¬ isBookSelected-TravelPlannerCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-160 | ⊦ ¬ isBookSelected-TravelPlannerCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-161 | ⊦ ¬ isBookSelected-TravelPlannerCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-162 | ⊦ ¬ isBookSelected-TravelPlannerCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-163 | ⊦ isBookSelected-TravelPlannerCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-164 | ⊦ ¬ isBookSelected-TravelPlannerCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-165 | ⊦ ¬ isBookSelected-TravelPlannerCmd(Confirm-UserCmd-4) | An Axiom |
| test-166 | ⊦ ¬ isBookSelected-TravelPlannerCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-167 | ⊦ ¬ isBookSelected-TravelPlannerCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-168 | ⊦ ¬ isBookSelected-TravelPlannerCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-169 | ⊦ ¬ isBookSelected-TravelPlannerCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-170 | ⊦ ¬ isBookSelected-TravelPlannerCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-171 | ⊦ ¬ isBookSelected-TravelPlannerCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-172 | ⊦ ¬ isBookSelected-TravelPlannerCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-173 | ⊦ ¬ isBookSelected-TravelPlannerCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-174 | ⊦ ¬ isBookSelected-TravelPlannerCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-175 | ⊦ ¬ isBookSelected-TravelPlannerCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-176 | ⊦ ¬ isBookSelected-TravelPlannerCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-177 | ⊦ ¬ isBookSelected-TravelPlannerCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-178 | ⊦ ¬ isBookSelected-TravelPlannerCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-179 | ⊦ ¬ isBookSelected-TravelPlannerCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-180 | ⊦ ¬ isBookSelected-TravelPlannerCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-181 | ⊦ ¬ isBookSelected-TravelPlannerCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-182 | ⊦ ¬ isBookSelected-TravelPlannerCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-183 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(Abort9-UserCmd) | An Axiom |
| test-184 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(Abort8-UserCmd) | An Axiom |
| test-185 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-186 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-187 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-188 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-189 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-190 | ⊦ isRetFlightOffers-TravelPlannerCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-191 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(Confirm-UserCmd-4) | An Axiom |
| test-192 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-193 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-194 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-195 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-196 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-197 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-198 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-199 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-200 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-201 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-202 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-203 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-204 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-205 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-206 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-207 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-208 | ⊦ ¬ isRetFlightOffers-TravelPlannerCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-209 | ⊦ ¬ isConfirm-UserCmd-4(Abort9-UserCmd) | An Axiom |
| test-210 | ⊦ ¬ isConfirm-UserCmd-4(Abort8-UserCmd) | An Axiom |
| test-211 | ⊦ ¬ isConfirm-UserCmd-4(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-212 | ⊦ ¬ isConfirm-UserCmd-4(BookFlightOffer-AirlineCmd) | An Axiom |
| test-213 | ⊦ ¬ isConfirm-UserCmd-4(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-214 | ⊦ ¬ isConfirm-UserCmd-4(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-215 | ⊦ ¬ isConfirm-UserCmd-4(BookSelected-TravelPlannerCmd) | An Axiom |
| test-216 | ⊦ ¬ isConfirm-UserCmd-4(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-217 | ⊦ isConfirm-UserCmd-4(Confirm-UserCmd-4) | An Axiom |
| test-218 | ⊦ ¬ isConfirm-UserCmd-4(ConfirmRelease-UserCmd-3) | An Axiom |
| test-219 | ⊦ ¬ isConfirm-UserCmd-4(GetSingleSelection-UserCmd-2) | An Axiom |
| test-220 | ⊦ ¬ isConfirm-UserCmd-4(GetInputRequestData-UserCmd-1) | An Axiom |
| test-221 | ⊦ ¬ isConfirm-UserCmd-4(OkPayCommission-AirlineCmd) | An Axiom |
| test-222 | ⊦ ¬ isConfirm-UserCmd-4(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-223 | ⊦ ¬ isConfirm-UserCmd-4(GetFlightOffers-AirlineCmd) | An Axiom |
| test-224 | ⊦ ¬ isConfirm-UserCmd-4(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-225 | ⊦ ¬ isConfirm-UserCmd-4(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-226 | ⊦ ¬ isConfirm-UserCmd-4(PayCommission-TravelAgencyCmd) | An Axiom |
| test-227 | ⊦ ¬ isConfirm-UserCmd-4(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-228 | ⊦ ¬ isConfirm-UserCmd-4(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-229 | ⊦ ¬ isConfirm-UserCmd-4(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-230 | ⊦ ¬ isConfirm-UserCmd-4(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-231 | ⊦ ¬ isConfirm-UserCmd-4(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-232 | ⊦ ¬ isConfirm-UserCmd-4(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-233 | ⊦ ¬ isConfirm-UserCmd-4(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-234 | ⊦ ¬ isConfirm-UserCmd-4(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-235 | ⊦ ¬ isConfirmRelease-UserCmd-3(Abort9-UserCmd) | An Axiom |
| test-236 | ⊦ ¬ isConfirmRelease-UserCmd-3(Abort8-UserCmd) | An Axiom |
| test-237 | ⊦ ¬ isConfirmRelease-UserCmd-3(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-238 | ⊦ ¬ isConfirmRelease-UserCmd-3(BookFlightOffer-AirlineCmd) | An Axiom |
| test-239 | ⊦ ¬ isConfirmRelease-UserCmd-3(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-240 | ⊦ ¬ isConfirmRelease-UserCmd-3(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-241 | ⊦ ¬ isConfirmRelease-UserCmd-3(BookSelected-TravelPlannerCmd) | An Axiom |
| test-242 | ⊦ ¬ isConfirmRelease-UserCmd-3(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-243 | ⊦ ¬ isConfirmRelease-UserCmd-3(Confirm-UserCmd-4) | An Axiom |
| test-244 | ⊦ isConfirmRelease-UserCmd-3(ConfirmRelease-UserCmd-3) | An Axiom |
| test-245 | ⊦ ¬ isConfirmRelease-UserCmd-3(GetSingleSelection-UserCmd-2) | An Axiom |
| test-246 | ⊦ ¬ isConfirmRelease-UserCmd-3(GetInputRequestData-UserCmd-1) | An Axiom |
| test-247 | ⊦ ¬ isConfirmRelease-UserCmd-3(OkPayCommission-AirlineCmd) | An Axiom |
| test-248 | ⊦ ¬ isConfirmRelease-UserCmd-3(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-249 | ⊦ ¬ isConfirmRelease-UserCmd-3(GetFlightOffers-AirlineCmd) | An Axiom |
| test-250 | ⊦ ¬ isConfirmRelease-UserCmd-3(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-251 | ⊦ ¬ isConfirmRelease-UserCmd-3(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-252 | ⊦ ¬ isConfirmRelease-UserCmd-3(PayCommission-TravelAgencyCmd) | An Axiom |
| test-253 | ⊦ ¬ isConfirmRelease-UserCmd-3(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-254 | ⊦ ¬ isConfirmRelease-UserCmd-3(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-255 | ⊦ ¬ isConfirmRelease-UserCmd-3(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-256 | ⊦ ¬ isConfirmRelease-UserCmd-3(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-257 | ⊦ ¬ isConfirmRelease-UserCmd-3(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-258 | ⊦ ¬ isConfirmRelease-UserCmd-3(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-259 | ⊦ ¬ isConfirmRelease-UserCmd-3(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-260 | ⊦ ¬ isConfirmRelease-UserCmd-3(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-261 | ⊦ ¬ isGetSingleSelection-UserCmd-2(Abort9-UserCmd) | An Axiom |
| test-262 | ⊦ ¬ isGetSingleSelection-UserCmd-2(Abort8-UserCmd) | An Axiom |
| test-263 | ⊦ ¬ isGetSingleSelection-UserCmd-2(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-264 | ⊦ ¬ isGetSingleSelection-UserCmd-2(BookFlightOffer-AirlineCmd) | An Axiom |
| test-265 | ⊦ ¬ isGetSingleSelection-UserCmd-2(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-266 | ⊦ ¬ isGetSingleSelection-UserCmd-2(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-267 | ⊦ ¬ isGetSingleSelection-UserCmd-2(BookSelected-TravelPlannerCmd) | An Axiom |
| test-268 | ⊦ ¬ isGetSingleSelection-UserCmd-2(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-269 | ⊦ ¬ isGetSingleSelection-UserCmd-2(Confirm-UserCmd-4) | An Axiom |
| test-270 | ⊦ ¬ isGetSingleSelection-UserCmd-2(ConfirmRelease-UserCmd-3) | An Axiom |
| test-271 | ⊦ isGetSingleSelection-UserCmd-2(GetSingleSelection-UserCmd-2) | An Axiom |
| test-272 | ⊦ ¬ isGetSingleSelection-UserCmd-2(GetInputRequestData-UserCmd-1) | An Axiom |
| test-273 | ⊦ ¬ isGetSingleSelection-UserCmd-2(OkPayCommission-AirlineCmd) | An Axiom |
| test-274 | ⊦ ¬ isGetSingleSelection-UserCmd-2(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-275 | ⊦ ¬ isGetSingleSelection-UserCmd-2(GetFlightOffers-AirlineCmd) | An Axiom |
| test-276 | ⊦ ¬ isGetSingleSelection-UserCmd-2(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-277 | ⊦ ¬ isGetSingleSelection-UserCmd-2(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-278 | ⊦ ¬ isGetSingleSelection-UserCmd-2(PayCommission-TravelAgencyCmd) | An Axiom |
| test-279 | ⊦ ¬ isGetSingleSelection-UserCmd-2(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-280 | ⊦ ¬ isGetSingleSelection-UserCmd-2(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-281 | ⊦ ¬ isGetSingleSelection-UserCmd-2(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-282 | ⊦ ¬ isGetSingleSelection-UserCmd-2(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-283 | ⊦ ¬ isGetSingleSelection-UserCmd-2(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-284 | ⊦ ¬ isGetSingleSelection-UserCmd-2(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-285 | ⊦ ¬ isGetSingleSelection-UserCmd-2(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-286 | ⊦ ¬ isGetSingleSelection-UserCmd-2(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-287 | ⊦ ¬ isGetInputRequestData-UserCmd-1(Abort9-UserCmd) | An Axiom |
| test-288 | ⊦ ¬ isGetInputRequestData-UserCmd-1(Abort8-UserCmd) | An Axiom |
| test-289 | ⊦ ¬ isGetInputRequestData-UserCmd-1(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-290 | ⊦ ¬ isGetInputRequestData-UserCmd-1(BookFlightOffer-AirlineCmd) | An Axiom |
| test-291 | ⊦ ¬ isGetInputRequestData-UserCmd-1(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-292 | ⊦ ¬ isGetInputRequestData-UserCmd-1(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-293 | ⊦ ¬ isGetInputRequestData-UserCmd-1(BookSelected-TravelPlannerCmd) | An Axiom |
| test-294 | ⊦ ¬ isGetInputRequestData-UserCmd-1(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-295 | ⊦ ¬ isGetInputRequestData-UserCmd-1(Confirm-UserCmd-4) | An Axiom |
| test-296 | ⊦ ¬ isGetInputRequestData-UserCmd-1(ConfirmRelease-UserCmd-3) | An Axiom |
| test-297 | ⊦ ¬ isGetInputRequestData-UserCmd-1(GetSingleSelection-UserCmd-2) | An Axiom |
| test-298 | ⊦ isGetInputRequestData-UserCmd-1(GetInputRequestData-UserCmd-1) | An Axiom |
| test-299 | ⊦ ¬ isGetInputRequestData-UserCmd-1(OkPayCommission-AirlineCmd) | An Axiom |
| test-300 | ⊦ ¬ isGetInputRequestData-UserCmd-1(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-301 | ⊦ ¬ isGetInputRequestData-UserCmd-1(GetFlightOffers-AirlineCmd) | An Axiom |
| test-302 | ⊦ ¬ isGetInputRequestData-UserCmd-1(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-303 | ⊦ ¬ isGetInputRequestData-UserCmd-1(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-304 | ⊦ ¬ isGetInputRequestData-UserCmd-1(PayCommission-TravelAgencyCmd) | An Axiom |
| test-305 | ⊦ ¬ isGetInputRequestData-UserCmd-1(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-306 | ⊦ ¬ isGetInputRequestData-UserCmd-1(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-307 | ⊦ ¬ isGetInputRequestData-UserCmd-1(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-308 | ⊦ ¬ isGetInputRequestData-UserCmd-1(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-309 | ⊦ ¬ isGetInputRequestData-UserCmd-1(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-310 | ⊦ ¬ isGetInputRequestData-UserCmd-1(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-311 | ⊦ ¬ isGetInputRequestData-UserCmd-1(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-312 | ⊦ ¬ isGetInputRequestData-UserCmd-1(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-313 | ⊦ ¬ isOkPayCommission-AirlineCmd(Abort9-UserCmd) | An Axiom |
| test-314 | ⊦ ¬ isOkPayCommission-AirlineCmd(Abort8-UserCmd) | An Axiom |
| test-315 | ⊦ ¬ isOkPayCommission-AirlineCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-316 | ⊦ ¬ isOkPayCommission-AirlineCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-317 | ⊦ ¬ isOkPayCommission-AirlineCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-318 | ⊦ ¬ isOkPayCommission-AirlineCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-319 | ⊦ ¬ isOkPayCommission-AirlineCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-320 | ⊦ ¬ isOkPayCommission-AirlineCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-321 | ⊦ ¬ isOkPayCommission-AirlineCmd(Confirm-UserCmd-4) | An Axiom |
| test-322 | ⊦ ¬ isOkPayCommission-AirlineCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-323 | ⊦ ¬ isOkPayCommission-AirlineCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-324 | ⊦ ¬ isOkPayCommission-AirlineCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-325 | ⊦ isOkPayCommission-AirlineCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-326 | ⊦ ¬ isOkPayCommission-AirlineCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-327 | ⊦ ¬ isOkPayCommission-AirlineCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-328 | ⊦ ¬ isOkPayCommission-AirlineCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-329 | ⊦ ¬ isOkPayCommission-AirlineCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-330 | ⊦ ¬ isOkPayCommission-AirlineCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-331 | ⊦ ¬ isOkPayCommission-AirlineCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-332 | ⊦ ¬ isOkPayCommission-AirlineCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-333 | ⊦ ¬ isOkPayCommission-AirlineCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-334 | ⊦ ¬ isOkPayCommission-AirlineCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-335 | ⊦ ¬ isOkPayCommission-AirlineCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-336 | ⊦ ¬ isOkPayCommission-AirlineCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-337 | ⊦ ¬ isOkPayCommission-AirlineCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-338 | ⊦ ¬ isOkPayCommission-AirlineCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-339 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(Abort9-UserCmd) | An Axiom |
| test-340 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(Abort8-UserCmd) | An Axiom |
| test-341 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-342 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-343 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-344 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-345 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-346 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-347 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(Confirm-UserCmd-4) | An Axiom |
| test-348 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-349 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-350 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-351 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-352 | ⊦ isBookFlightOfferstate7-AirlineCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-353 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-354 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-355 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-356 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-357 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-358 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-359 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-360 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-361 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-362 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-363 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-364 | ⊦ ¬ isBookFlightOfferstate7-AirlineCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-365 | ⊦ ¬ isGetFlightOffers-AirlineCmd(Abort9-UserCmd) | An Axiom |
| test-366 | ⊦ ¬ isGetFlightOffers-AirlineCmd(Abort8-UserCmd) | An Axiom |
| test-367 | ⊦ ¬ isGetFlightOffers-AirlineCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-368 | ⊦ ¬ isGetFlightOffers-AirlineCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-369 | ⊦ ¬ isGetFlightOffers-AirlineCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-370 | ⊦ ¬ isGetFlightOffers-AirlineCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-371 | ⊦ ¬ isGetFlightOffers-AirlineCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-372 | ⊦ ¬ isGetFlightOffers-AirlineCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-373 | ⊦ ¬ isGetFlightOffers-AirlineCmd(Confirm-UserCmd-4) | An Axiom |
| test-374 | ⊦ ¬ isGetFlightOffers-AirlineCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-375 | ⊦ ¬ isGetFlightOffers-AirlineCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-376 | ⊦ ¬ isGetFlightOffers-AirlineCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-377 | ⊦ ¬ isGetFlightOffers-AirlineCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-378 | ⊦ ¬ isGetFlightOffers-AirlineCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-379 | ⊦ isGetFlightOffers-AirlineCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-380 | ⊦ ¬ isGetFlightOffers-AirlineCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-381 | ⊦ ¬ isGetFlightOffers-AirlineCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-382 | ⊦ ¬ isGetFlightOffers-AirlineCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-383 | ⊦ ¬ isGetFlightOffers-AirlineCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-384 | ⊦ ¬ isGetFlightOffers-AirlineCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-385 | ⊦ ¬ isGetFlightOffers-AirlineCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-386 | ⊦ ¬ isGetFlightOffers-AirlineCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-387 | ⊦ ¬ isGetFlightOffers-AirlineCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-388 | ⊦ ¬ isGetFlightOffers-AirlineCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-389 | ⊦ ¬ isGetFlightOffers-AirlineCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-390 | ⊦ ¬ isGetFlightOffers-AirlineCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-391 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(Abort9-UserCmd) | An Axiom |
| test-392 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(Abort8-UserCmd) | An Axiom |
| test-393 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-394 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-395 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-396 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-397 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-398 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-399 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(Confirm-UserCmd-4) | An Axiom |
| test-400 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-401 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-402 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-403 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-404 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-405 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-406 | ⊦ isGetDeclassifiedCCD-CreditCardCenterCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-407 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-408 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-409 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-410 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-411 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-412 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-413 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-414 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-415 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-416 | ⊦ ¬ isGetDeclassifiedCCD-CreditCardCenterCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-417 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(Abort9-UserCmd) | An Axiom |
| test-418 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(Abort8-UserCmd) | An Axiom |
| test-419 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-420 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-421 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-422 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-423 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-424 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-425 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(Confirm-UserCmd-4) | An Axiom |
| test-426 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-427 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-428 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-429 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-430 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-431 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-432 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-433 | ⊦ isReleaseCCD-CreditCardCenterCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-434 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-435 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-436 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-437 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-438 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-439 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-440 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-441 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-442 | ⊦ ¬ isReleaseCCD-CreditCardCenterCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-443 | ⊦ ¬ isPayCommission-TravelAgencyCmd(Abort9-UserCmd) | An Axiom |
| test-444 | ⊦ ¬ isPayCommission-TravelAgencyCmd(Abort8-UserCmd) | An Axiom |
| test-445 | ⊦ ¬ isPayCommission-TravelAgencyCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-446 | ⊦ ¬ isPayCommission-TravelAgencyCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-447 | ⊦ ¬ isPayCommission-TravelAgencyCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-448 | ⊦ ¬ isPayCommission-TravelAgencyCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-449 | ⊦ ¬ isPayCommission-TravelAgencyCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-450 | ⊦ ¬ isPayCommission-TravelAgencyCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-451 | ⊦ ¬ isPayCommission-TravelAgencyCmd(Confirm-UserCmd-4) | An Axiom |
| test-452 | ⊦ ¬ isPayCommission-TravelAgencyCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-453 | ⊦ ¬ isPayCommission-TravelAgencyCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-454 | ⊦ ¬ isPayCommission-TravelAgencyCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-455 | ⊦ ¬ isPayCommission-TravelAgencyCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-456 | ⊦ ¬ isPayCommission-TravelAgencyCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-457 | ⊦ ¬ isPayCommission-TravelAgencyCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-458 | ⊦ ¬ isPayCommission-TravelAgencyCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-459 | ⊦ ¬ isPayCommission-TravelAgencyCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-460 | ⊦ isPayCommission-TravelAgencyCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-461 | ⊦ ¬ isPayCommission-TravelAgencyCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-462 | ⊦ ¬ isPayCommission-TravelAgencyCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-463 | ⊦ ¬ isPayCommission-TravelAgencyCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-464 | ⊦ ¬ isPayCommission-TravelAgencyCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-465 | ⊦ ¬ isPayCommission-TravelAgencyCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-466 | ⊦ ¬ isPayCommission-TravelAgencyCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-467 | ⊦ ¬ isPayCommission-TravelAgencyCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-468 | ⊦ ¬ isPayCommission-TravelAgencyCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-469 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(Abort9-UserCmd) | An Axiom |
| test-470 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(Abort8-UserCmd) | An Axiom |
| test-471 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-472 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-473 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-474 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-475 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-476 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-477 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(Confirm-UserCmd-4) | An Axiom |
| test-478 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-479 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-480 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-481 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-482 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-483 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-484 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-485 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-486 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-487 | ⊦ isRetFlightOffers-TravelAgencyCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-488 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-489 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-490 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-491 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-492 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-493 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-494 | ⊦ ¬ isRetFlightOffers-TravelAgencyCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-495 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(Abort9-UserCmd) | An Axiom |
| test-496 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(Abort8-UserCmd) | An Axiom |
| test-497 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-498 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-499 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-500 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-501 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-502 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-503 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(Confirm-UserCmd-4) | An Axiom |
| test-504 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-505 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-506 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-507 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-508 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-509 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-510 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-511 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-512 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-513 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-514 | ⊦ isGetFlightOffers-TravelAgencyCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-515 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-516 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-517 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-518 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-519 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-520 | ⊦ ¬ isGetFlightOffers-TravelAgencyCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-521 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(Abort9-UserCmd) | An Axiom |
| test-522 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(Abort8-UserCmd) | An Axiom |
| test-523 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-524 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-525 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-526 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-527 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-528 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-529 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(Confirm-UserCmd-4) | An Axiom |
| test-530 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-531 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-532 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-533 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-534 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-535 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-536 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-537 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-538 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-539 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-540 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-541 | ⊦ isOkConfirmBooking-TravelPlannerCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-542 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-543 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-544 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-545 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-546 | ⊦ ¬ isOkConfirmBooking-TravelPlannerCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-547 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(Abort9-UserCmd) | An Axiom |
| test-548 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(Abort8-UserCmd) | An Axiom |
| test-549 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-550 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-551 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-552 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-553 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-554 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-555 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(Confirm-UserCmd-4) | An Axiom |
| test-556 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-557 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-558 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-559 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-560 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-561 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-562 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-563 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-564 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-565 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-566 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-567 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-568 | ⊦ isDeclassifiedCCD-TravelPlannerCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-569 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-570 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-571 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-572 | ⊦ ¬ isDeclassifiedCCD-TravelPlannerCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-573 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(Abort9-UserCmd) | An Axiom |
| test-574 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(Abort8-UserCmd) | An Axiom |
| test-575 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-576 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-577 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-578 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-579 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-580 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-581 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(Confirm-UserCmd-4) | An Axiom |
| test-582 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-583 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-584 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-585 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-586 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-587 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-588 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-589 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-590 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-591 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-592 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-593 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-594 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-595 | ⊦ isBookSelectedstate2-TravelPlannerCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-596 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-597 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-598 | ⊦ ¬ isBookSelectedstate2-TravelPlannerCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-599 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(Abort9-UserCmd) | An Axiom |
| test-600 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(Abort8-UserCmd) | An Axiom |
| test-601 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-602 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-603 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-604 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-605 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-606 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-607 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(Confirm-UserCmd-4) | An Axiom |
| test-608 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-609 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-610 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-611 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-612 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-613 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-614 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-615 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-616 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-617 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-618 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-619 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-620 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-621 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-622 | ⊦ isRetFlightOffersstate1-TravelPlannerCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-623 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-624 | ⊦ ¬ isRetFlightOffersstate1-TravelPlannerCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-625 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(Abort9-UserCmd) | An Axiom |
| test-626 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(Abort8-UserCmd) | An Axiom |
| test-627 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-628 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-629 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-630 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-631 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-632 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-633 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(Confirm-UserCmd-4) | An Axiom |
| test-634 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-635 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-636 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-637 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-638 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-639 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-640 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-641 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-642 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-643 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-644 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-645 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-646 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-647 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-648 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-649 | ⊦ isGetFlightOffers-TravelPlannerCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-650 | ⊦ ¬ isGetFlightOffers-TravelPlannerCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| test-651 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(Abort9-UserCmd) | An Axiom |
| test-652 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(Abort8-UserCmd) | An Axiom |
| test-653 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(BookFlightOfferstate6-AirlineCmd) | An Axiom |
| test-654 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(BookFlightOffer-AirlineCmd) | An Axiom |
| test-655 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(afterdeclassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-656 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(declassifyCCD4ASM-CreditCardCenterCmd) | An Axiom |
| test-657 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(BookSelected-TravelPlannerCmd) | An Axiom |
| test-658 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(RetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-659 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(Confirm-UserCmd-4) | An Axiom |
| test-660 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(ConfirmRelease-UserCmd-3) | An Axiom |
| test-661 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(GetSingleSelection-UserCmd-2) | An Axiom |
| test-662 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(GetInputRequestData-UserCmd-1) | An Axiom |
| test-663 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(OkPayCommission-AirlineCmd) | An Axiom |
| test-664 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(BookFlightOfferstate7-AirlineCmd) | An Axiom |
| test-665 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(GetFlightOffers-AirlineCmd) | An Axiom |
| test-666 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(GetDeclassifiedCCD-CreditCardCenterCmd) | An Axiom |
| test-667 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(ReleaseCCD-CreditCardCenterCmd) | An Axiom |
| test-668 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(PayCommission-TravelAgencyCmd) | An Axiom |
| test-669 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(RetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-670 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(GetFlightOffers-TravelAgencyCmd) | An Axiom |
| test-671 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(OkConfirmBooking-TravelPlannerCmd) | An Axiom |
| test-672 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(DeclassifiedCCD-TravelPlannerCmd) | An Axiom |
| test-673 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(BookSelectedstate2-TravelPlannerCmd) | An Axiom |
| test-674 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(RetFlightOffersstate1-TravelPlannerCmd) | An Axiom |
| test-675 | ⊦ ¬ isInit-GetInputRequestData-TravelPlannerCmd(GetFlightOffers-TravelPlannerCmd) | An Axiom |
| test-676 | ⊦ isInit-GetInputRequestData-TravelPlannerCmd(Init-GetInputRequestData-TravelPlannerCmd) | An Axiom |
| case | ⊦ cmd = Init-GetInputRequestData-TravelPlannerCmd ∨ cmd = GetFlightOffers-TravelPlannerCmd ∨ cmd = RetFlightOffersstate1-TravelPlannerCmd ∨ cmd = BookSelectedstate2-TravelPlannerCmd ∨ cmd = DeclassifiedCCD-TravelPlannerCmd ∨ cmd = OkConfirmBooking-TravelPlannerCmd ∨ cmd = GetFlightOffers-TravelAgencyCmd ∨ cmd = RetFlightOffers-TravelAgencyCmd ∨ cmd = PayCommission-TravelAgencyCmd ∨ cmd = ReleaseCCD-CreditCardCenterCmd ∨ cmd = GetDeclassifiedCCD-CreditCardCenterCmd ∨ cmd = GetFlightOffers-AirlineCmd ∨ cmd = BookFlightOfferstate7-AirlineCmd ∨ cmd = OkPayCommission-AirlineCmd ∨ cmd = GetInputRequestData-UserCmd-1 ∨ cmd = GetSingleSelection-UserCmd-2 ∨ cmd = ConfirmRelease-UserCmd-3 ∨ cmd = Confirm-UserCmd-4 ∨ cmd = RetFlightOffers-TravelPlannerCmd ∨ cmd = BookSelected-TravelPlannerCmd ∨ cmd = declassifyCCD4ASM-CreditCardCenterCmd ∨ cmd = afterdeclassifyCCD4ASM-CreditCardCenterCmd ∨ cmd = BookFlightOffer-AirlineCmd ∨ cmd = BookFlightOfferstate6-AirlineCmd ∨ cmd = Abort8-UserCmd ∨ cmd = Abort9-UserCmd | An Axiom |
| ex-01 | ⊦ isAbort9-UserCmd(cmd) ↔ cmd = Abort9-UserCmd | An Axiom |
| ex-02 | ⊦ isAbort8-UserCmd(cmd) ↔ cmd = Abort8-UserCmd | An Axiom |
| ex-03 | ⊦ isBookFlightOfferstate6-AirlineCmd(cmd) ↔ cmd = BookFlightOfferstate6-AirlineCmd | An Axiom |
| ex-04 | ⊦ isBookFlightOffer-AirlineCmd(cmd) ↔ cmd = BookFlightOffer-AirlineCmd | An Axiom |
| ex-05 | ⊦ isafterdeclassifyCCD4ASM-CreditCardCenterCmd(cmd) ↔ cmd = afterdeclassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| ex-06 | ⊦ isdeclassifyCCD4ASM-CreditCardCenterCmd(cmd) ↔ cmd = declassifyCCD4ASM-CreditCardCenterCmd | An Axiom |
| ex-07 | ⊦ isBookSelected-TravelPlannerCmd(cmd) ↔ cmd = BookSelected-TravelPlannerCmd | An Axiom |
| ex-08 | ⊦ isRetFlightOffers-TravelPlannerCmd(cmd) ↔ cmd = RetFlightOffers-TravelPlannerCmd | An Axiom |
| ex-09 | ⊦ isConfirm-UserCmd-4(cmd) ↔ cmd = Confirm-UserCmd-4 | An Axiom |
| ex-10 | ⊦ isConfirmRelease-UserCmd-3(cmd) ↔ cmd = ConfirmRelease-UserCmd-3 | An Axiom |
| ex-11 | ⊦ isGetSingleSelection-UserCmd-2(cmd) ↔ cmd = GetSingleSelection-UserCmd-2 | An Axiom |
| ex-12 | ⊦ isGetInputRequestData-UserCmd-1(cmd) ↔ cmd = GetInputRequestData-UserCmd-1 | An Axiom |
| ex-13 | ⊦ isOkPayCommission-AirlineCmd(cmd) ↔ cmd = OkPayCommission-AirlineCmd | An Axiom |
| ex-14 | ⊦ isBookFlightOfferstate7-AirlineCmd(cmd) ↔ cmd = BookFlightOfferstate7-AirlineCmd | An Axiom |
| ex-15 | ⊦ isGetFlightOffers-AirlineCmd(cmd) ↔ cmd = GetFlightOffers-AirlineCmd | An Axiom |
| ex-16 | ⊦ isGetDeclassifiedCCD-CreditCardCenterCmd(cmd) ↔ cmd = GetDeclassifiedCCD-CreditCardCenterCmd | An Axiom |
| ex-17 | ⊦ isReleaseCCD-CreditCardCenterCmd(cmd) ↔ cmd = ReleaseCCD-CreditCardCenterCmd | An Axiom |
| ex-18 | ⊦ isPayCommission-TravelAgencyCmd(cmd) ↔ cmd = PayCommission-TravelAgencyCmd | An Axiom |
| ex-19 | ⊦ isRetFlightOffers-TravelAgencyCmd(cmd) ↔ cmd = RetFlightOffers-TravelAgencyCmd | An Axiom |
| ex-20 | ⊦ isGetFlightOffers-TravelAgencyCmd(cmd) ↔ cmd = GetFlightOffers-TravelAgencyCmd | An Axiom |
| ex-21 | ⊦ isOkConfirmBooking-TravelPlannerCmd(cmd) ↔ cmd = OkConfirmBooking-TravelPlannerCmd | An Axiom |
| ex-22 | ⊦ isDeclassifiedCCD-TravelPlannerCmd(cmd) ↔ cmd = DeclassifiedCCD-TravelPlannerCmd | An Axiom |
| ex-23 | ⊦ isBookSelectedstate2-TravelPlannerCmd(cmd) ↔ cmd = BookSelectedstate2-TravelPlannerCmd | An Axiom |
| ex-24 | ⊦ isRetFlightOffersstate1-TravelPlannerCmd(cmd) ↔ cmd = RetFlightOffersstate1-TravelPlannerCmd | An Axiom |
| ex-25 | ⊦ isGetFlightOffers-TravelPlannerCmd(cmd) ↔ cmd = GetFlightOffers-TravelPlannerCmd | An Axiom |
| ex-26 | ⊦ isInit-GetInputRequestData-TravelPlannerCmd(cmd) ↔ cmd = Init-GetInputRequestData-TravelPlannerCmd | An Axiom |
| gen | An Axiom |