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 | ⊦ [] ≠ d + dl | An Axiom |
| disj-02 | ⊦ [] ≠ a_GPSPos + a_ListOfGPSPos | An Axiom |
| disj-03 | ⊦ [] ≠ a_FlightOffer + a_ListOfFlightOffer | An Axiom |
| disj-04 | ⊦ wrapMessage2Data(msg) ≠ wrapBoolean2Data(a_Boolean) | An Axiom |
| disj-05 | ⊦ wrapMessage2Data(msg) ≠ wrapCreditCardDetails2Data(a_CreditCardDetails) | An Axiom |
| disj-06 | ⊦ wrapMessage2Data(msg) ≠ wrapFlightOffer2Data(a_FlightOffer) | An Axiom |
| disj-07 | ⊦ wrapMessage2Data(msg) ≠ wrapGPSPos2Data(a_GPSPos) | An Axiom |
| disj-08 | ⊦ wrapMessage2Data(msg) ≠ wrapInteger2Data(a_Integer) | An Axiom |
| disj-09 | ⊦ wrapMessage2Data(msg) ≠ wrapRequestData2Data(a_RequestData) | An Axiom |
| disj-10 | ⊦ wrapMessage2Data(msg) ≠ wrapString2Data(a_String) | An Axiom |
| disj-11 | ⊦ wrapMessage2Data(msg) ≠ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) | An Axiom |
| disj-12 | ⊦ wrapMessage2Data(msg) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-13 | ⊦ wrapMessage2Data(msg) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-14 | ⊦ wrapMessage2Data(msg) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-15 | ⊦ wrapMessage2Data(msg) ≠ mkNat(m) | An Axiom |
| disj-16 | ⊦ wrapMessage2Data(msg) ≠ mkDataPair(d, d0) | An Axiom |
| disj-17 | ⊦ wrapMessage2Data(msg) ≠ null | An Axiom |
| disj-18 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapCreditCardDetails2Data(a_CreditCardDetails) | An Axiom |
| disj-19 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapFlightOffer2Data(a_FlightOffer) | An Axiom |
| disj-20 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapGPSPos2Data(a_GPSPos) | An Axiom |
| disj-21 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapInteger2Data(a_Integer) | An Axiom |
| disj-22 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapRequestData2Data(a_RequestData) | An Axiom |
| disj-23 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapString2Data(a_String) | An Axiom |
| disj-24 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) | An Axiom |
| disj-25 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-26 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-27 | ⊦ wrapBoolean2Data(a_Boolean) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-28 | ⊦ wrapBoolean2Data(a_Boolean) ≠ mkNat(m) | An Axiom |
| disj-29 | ⊦ wrapBoolean2Data(a_Boolean) ≠ mkDataPair(d, d0) | An Axiom |
| disj-30 | ⊦ wrapBoolean2Data(a_Boolean) ≠ null | An Axiom |
| disj-31 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapFlightOffer2Data(a_FlightOffer) | An Axiom |
| disj-32 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapGPSPos2Data(a_GPSPos) | An Axiom |
| disj-33 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapInteger2Data(a_Integer) | An Axiom |
| disj-34 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapRequestData2Data(a_RequestData) | An Axiom |
| disj-35 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapString2Data(a_String) | An Axiom |
| disj-36 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) | An Axiom |
| disj-37 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-38 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-39 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-40 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ mkNat(m) | An Axiom |
| disj-41 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ mkDataPair(d, d0) | An Axiom |
| disj-42 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) ≠ null | An Axiom |
| disj-43 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ wrapGPSPos2Data(a_GPSPos) | An Axiom |
| disj-44 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ wrapInteger2Data(a_Integer) | An Axiom |
| disj-45 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ wrapRequestData2Data(a_RequestData) | An Axiom |
| disj-46 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ wrapString2Data(a_String) | An Axiom |
| disj-47 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) | An Axiom |
| disj-48 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-49 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-50 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-51 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ mkNat(m) | An Axiom |
| disj-52 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ mkDataPair(d, d0) | An Axiom |
| disj-53 | ⊦ wrapFlightOffer2Data(a_FlightOffer) ≠ null | An Axiom |
| disj-54 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ wrapInteger2Data(a_Integer) | An Axiom |
| disj-55 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ wrapRequestData2Data(a_RequestData) | An Axiom |
| disj-56 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ wrapString2Data(a_String) | An Axiom |
| disj-57 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) | An Axiom |
| disj-58 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-59 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-60 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-61 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ mkNat(m) | An Axiom |
| disj-62 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ mkDataPair(d, d0) | An Axiom |
| disj-63 | ⊦ wrapGPSPos2Data(a_GPSPos) ≠ null | An Axiom |
| disj-64 | ⊦ wrapInteger2Data(a_Integer) ≠ wrapRequestData2Data(a_RequestData) | An Axiom |
| disj-65 | ⊦ wrapInteger2Data(a_Integer) ≠ wrapString2Data(a_String) | An Axiom |
| disj-66 | ⊦ wrapInteger2Data(a_Integer) ≠ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) | An Axiom |
| disj-67 | ⊦ wrapInteger2Data(a_Integer) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-68 | ⊦ wrapInteger2Data(a_Integer) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-69 | ⊦ wrapInteger2Data(a_Integer) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-70 | ⊦ wrapInteger2Data(a_Integer) ≠ mkNat(m) | An Axiom |
| disj-71 | ⊦ wrapInteger2Data(a_Integer) ≠ mkDataPair(d, d0) | An Axiom |
| disj-72 | ⊦ wrapInteger2Data(a_Integer) ≠ null | An Axiom |
| disj-73 | ⊦ wrapRequestData2Data(a_RequestData) ≠ wrapString2Data(a_String) | An Axiom |
| disj-74 | ⊦ wrapRequestData2Data(a_RequestData) ≠ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) | An Axiom |
| disj-75 | ⊦ wrapRequestData2Data(a_RequestData) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-76 | ⊦ wrapRequestData2Data(a_RequestData) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-77 | ⊦ wrapRequestData2Data(a_RequestData) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-78 | ⊦ wrapRequestData2Data(a_RequestData) ≠ mkNat(m) | An Axiom |
| disj-79 | ⊦ wrapRequestData2Data(a_RequestData) ≠ mkDataPair(d, d0) | An Axiom |
| disj-80 | ⊦ wrapRequestData2Data(a_RequestData) ≠ null | An Axiom |
| disj-81 | ⊦ wrapString2Data(a_String) ≠ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) | An Axiom |
| disj-82 | ⊦ wrapString2Data(a_String) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-83 | ⊦ wrapString2Data(a_String) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-84 | ⊦ wrapString2Data(a_String) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-85 | ⊦ wrapString2Data(a_String) ≠ mkNat(m) | An Axiom |
| disj-86 | ⊦ wrapString2Data(a_String) ≠ mkDataPair(d, d0) | An Axiom |
| disj-87 | ⊦ wrapString2Data(a_String) ≠ null | An Axiom |
| disj-88 | ⊦ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) ≠ wrapListOfGPSPos2Data(a_ListOfGPSPos) | An Axiom |
| disj-89 | ⊦ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-90 | ⊦ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-91 | ⊦ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) ≠ mkNat(m) | An Axiom |
| disj-92 | ⊦ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) ≠ mkDataPair(d, d0) | An Axiom |
| disj-93 | ⊦ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) ≠ null | An Axiom |
| disj-94 | ⊦ wrapListOfGPSPos2Data(a_ListOfGPSPos) ≠ wrapListOfData2Data(dl) | An Axiom |
| disj-95 | ⊦ wrapListOfGPSPos2Data(a_ListOfGPSPos) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-96 | ⊦ wrapListOfGPSPos2Data(a_ListOfGPSPos) ≠ mkNat(m) | An Axiom |
| disj-97 | ⊦ wrapListOfGPSPos2Data(a_ListOfGPSPos) ≠ mkDataPair(d, d0) | An Axiom |
| disj-98 | ⊦ wrapListOfGPSPos2Data(a_ListOfGPSPos) ≠ null | An Axiom |
| disj-99 | ⊦ wrapListOfData2Data(dl) ≠ wrapAgent2Data(ag) | An Axiom |
| disj-100 | ⊦ wrapListOfData2Data(dl) ≠ mkNat(m) | An Axiom |
| disj-101 | ⊦ wrapListOfData2Data(dl) ≠ mkDataPair(d, d0) | An Axiom |
| disj-102 | ⊦ wrapListOfData2Data(dl) ≠ null | An Axiom |
| disj-103 | ⊦ wrapAgent2Data(ag) ≠ mkNat(m) | An Axiom |
| disj-104 | ⊦ wrapAgent2Data(ag) ≠ mkDataPair(d, d0) | An Axiom |
| disj-105 | ⊦ wrapAgent2Data(ag) ≠ null | An Axiom |
| disj-106 | ⊦ mkNat(m) ≠ mkDataPair(d, d0) | An Axiom |
| disj-107 | ⊦ mkNat(m) ≠ null | An Axiom |
| disj-108 | ⊦ mkDataPair(d, d0) ≠ null | An Axiom |
| disj-109 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkBookSelected(a_FlightOffer) | An Axiom |
| disj-110 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkConfirm | An Axiom |
| disj-111 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkConfirmBooking(a_Integer0) | An Axiom |
| disj-112 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkConfirmRelease(d, a_String) | An Axiom |
| disj-113 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkDeclassifiedCCD(a_CreditCardDetails0) | An Axiom |
| disj-114 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetDeclassifiedCCD | An Axiom |
| disj-115 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetFlightOffers(a_RequestData) | An Axiom |
| disj-116 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputAgent | An Axiom |
| disj-117 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputAirline | An Axiom |
| disj-118 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputBoolean | An Axiom |
| disj-119 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-120 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-121 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputData | An Axiom |
| disj-122 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputFlightOffer | An Axiom |
| disj-123 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputGPSPos | An Axiom |
| disj-124 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputIFlowUtil | An Axiom |
| disj-125 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputInteger | An Axiom |
| disj-126 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputRequestData | An Axiom |
| disj-127 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputString | An Axiom |
| disj-128 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputTravelAgency | An Axiom |
| disj-129 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetInputTravelPlanner | An Axiom |
| disj-130 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-131 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-132 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkOkConfirmBooking | An Axiom |
| disj-133 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkOkPayCommission | An Axiom |
| disj-134 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkPayCommission | An Axiom |
| disj-135 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-136 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-137 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkShow(d) | An Axiom |
| disj-138 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) ≠ mkStart | An Axiom |
| disj-139 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkConfirm | An Axiom |
| disj-140 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkConfirmBooking(a_Integer) | An Axiom |
| disj-141 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkConfirmRelease(d, a_String) | An Axiom |
| disj-142 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkDeclassifiedCCD(a_CreditCardDetails) | An Axiom |
| disj-143 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetDeclassifiedCCD | An Axiom |
| disj-144 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetFlightOffers(a_RequestData) | An Axiom |
| disj-145 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputAgent | An Axiom |
| disj-146 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputAirline | An Axiom |
| disj-147 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputBoolean | An Axiom |
| disj-148 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-149 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-150 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputData | An Axiom |
| disj-151 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputFlightOffer | An Axiom |
| disj-152 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputGPSPos | An Axiom |
| disj-153 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputIFlowUtil | An Axiom |
| disj-154 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputInteger | An Axiom |
| disj-155 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputRequestData | An Axiom |
| disj-156 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputString | An Axiom |
| disj-157 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputTravelAgency | An Axiom |
| disj-158 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetInputTravelPlanner | An Axiom |
| disj-159 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-160 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-161 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkOkConfirmBooking | An Axiom |
| disj-162 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkOkPayCommission | An Axiom |
| disj-163 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkPayCommission | An Axiom |
| disj-164 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-165 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-166 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkShow(d) | An Axiom |
| disj-167 | ⊦ mkBookSelected(a_FlightOffer) ≠ mkStart | An Axiom |
| disj-168 | ⊦ mkConfirm ≠ mkConfirmBooking(a_Integer) | An Axiom |
| disj-169 | ⊦ mkConfirm ≠ mkConfirmRelease(d, a_String) | An Axiom |
| disj-170 | ⊦ mkConfirm ≠ mkDeclassifiedCCD(a_CreditCardDetails) | An Axiom |
| disj-171 | ⊦ mkConfirm ≠ mkGetDeclassifiedCCD | An Axiom |
| disj-172 | ⊦ mkConfirm ≠ mkGetFlightOffers(a_RequestData) | An Axiom |
| disj-173 | ⊦ mkConfirm ≠ mkGetInputAgent | An Axiom |
| disj-174 | ⊦ mkConfirm ≠ mkGetInputAirline | An Axiom |
| disj-175 | ⊦ mkConfirm ≠ mkGetInputBoolean | An Axiom |
| disj-176 | ⊦ mkConfirm ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-177 | ⊦ mkConfirm ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-178 | ⊦ mkConfirm ≠ mkGetInputData | An Axiom |
| disj-179 | ⊦ mkConfirm ≠ mkGetInputFlightOffer | An Axiom |
| disj-180 | ⊦ mkConfirm ≠ mkGetInputGPSPos | An Axiom |
| disj-181 | ⊦ mkConfirm ≠ mkGetInputIFlowUtil | An Axiom |
| disj-182 | ⊦ mkConfirm ≠ mkGetInputInteger | An Axiom |
| disj-183 | ⊦ mkConfirm ≠ mkGetInputRequestData | An Axiom |
| disj-184 | ⊦ mkConfirm ≠ mkGetInputString | An Axiom |
| disj-185 | ⊦ mkConfirm ≠ mkGetInputTravelAgency | An Axiom |
| disj-186 | ⊦ mkConfirm ≠ mkGetInputTravelPlanner | An Axiom |
| disj-187 | ⊦ mkConfirm ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-188 | ⊦ mkConfirm ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-189 | ⊦ mkConfirm ≠ mkOkConfirmBooking | An Axiom |
| disj-190 | ⊦ mkConfirm ≠ mkOkPayCommission | An Axiom |
| disj-191 | ⊦ mkConfirm ≠ mkPayCommission | An Axiom |
| disj-192 | ⊦ mkConfirm ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-193 | ⊦ mkConfirm ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-194 | ⊦ mkConfirm ≠ mkShow(d) | An Axiom |
| disj-195 | ⊦ mkConfirm ≠ mkStart | An Axiom |
| disj-196 | ⊦ mkConfirmBooking(a_Integer) ≠ mkConfirmRelease(d, a_String) | An Axiom |
| disj-197 | ⊦ mkConfirmBooking(a_Integer) ≠ mkDeclassifiedCCD(a_CreditCardDetails) | An Axiom |
| disj-198 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetDeclassifiedCCD | An Axiom |
| disj-199 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetFlightOffers(a_RequestData) | An Axiom |
| disj-200 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputAgent | An Axiom |
| disj-201 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputAirline | An Axiom |
| disj-202 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputBoolean | An Axiom |
| disj-203 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-204 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-205 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputData | An Axiom |
| disj-206 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputFlightOffer | An Axiom |
| disj-207 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputGPSPos | An Axiom |
| disj-208 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputIFlowUtil | An Axiom |
| disj-209 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputInteger | An Axiom |
| disj-210 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputRequestData | An Axiom |
| disj-211 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputString | An Axiom |
| disj-212 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputTravelAgency | An Axiom |
| disj-213 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetInputTravelPlanner | An Axiom |
| disj-214 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-215 | ⊦ mkConfirmBooking(a_Integer) ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-216 | ⊦ mkConfirmBooking(a_Integer) ≠ mkOkConfirmBooking | An Axiom |
| disj-217 | ⊦ mkConfirmBooking(a_Integer) ≠ mkOkPayCommission | An Axiom |
| disj-218 | ⊦ mkConfirmBooking(a_Integer) ≠ mkPayCommission | An Axiom |
| disj-219 | ⊦ mkConfirmBooking(a_Integer) ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-220 | ⊦ mkConfirmBooking(a_Integer) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-221 | ⊦ mkConfirmBooking(a_Integer) ≠ mkShow(d) | An Axiom |
| disj-222 | ⊦ mkConfirmBooking(a_Integer) ≠ mkStart | An Axiom |
| disj-223 | ⊦ mkConfirmRelease(d, a_String) ≠ mkDeclassifiedCCD(a_CreditCardDetails) | An Axiom |
| disj-224 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetDeclassifiedCCD | An Axiom |
| disj-225 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetFlightOffers(a_RequestData) | An Axiom |
| disj-226 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputAgent | An Axiom |
| disj-227 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputAirline | An Axiom |
| disj-228 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputBoolean | An Axiom |
| disj-229 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-230 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-231 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputData | An Axiom |
| disj-232 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputFlightOffer | An Axiom |
| disj-233 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputGPSPos | An Axiom |
| disj-234 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputIFlowUtil | An Axiom |
| disj-235 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputInteger | An Axiom |
| disj-236 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputRequestData | An Axiom |
| disj-237 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputString | An Axiom |
| disj-238 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputTravelAgency | An Axiom |
| disj-239 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetInputTravelPlanner | An Axiom |
| disj-240 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-241 | ⊦ mkConfirmRelease(d, a_String) ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-242 | ⊦ mkConfirmRelease(d, a_String) ≠ mkOkConfirmBooking | An Axiom |
| disj-243 | ⊦ mkConfirmRelease(d, a_String) ≠ mkOkPayCommission | An Axiom |
| disj-244 | ⊦ mkConfirmRelease(d, a_String) ≠ mkPayCommission | An Axiom |
| disj-245 | ⊦ mkConfirmRelease(d, a_String) ≠ mkReleaseCCD(a_String0) | An Axiom |
| disj-246 | ⊦ mkConfirmRelease(d, a_String) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-247 | ⊦ mkConfirmRelease(d, a_String) ≠ mkShow(d0) | An Axiom |
| disj-248 | ⊦ mkConfirmRelease(d, a_String) ≠ mkStart | An Axiom |
| disj-249 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetDeclassifiedCCD | An Axiom |
| disj-250 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetFlightOffers(a_RequestData) | An Axiom |
| disj-251 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputAgent | An Axiom |
| disj-252 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputAirline | An Axiom |
| disj-253 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputBoolean | An Axiom |
| disj-254 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-255 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-256 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputData | An Axiom |
| disj-257 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputFlightOffer | An Axiom |
| disj-258 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputGPSPos | An Axiom |
| disj-259 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputIFlowUtil | An Axiom |
| disj-260 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputInteger | An Axiom |
| disj-261 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputRequestData | An Axiom |
| disj-262 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputString | An Axiom |
| disj-263 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputTravelAgency | An Axiom |
| disj-264 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetInputTravelPlanner | An Axiom |
| disj-265 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-266 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-267 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkOkConfirmBooking | An Axiom |
| disj-268 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkOkPayCommission | An Axiom |
| disj-269 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkPayCommission | An Axiom |
| disj-270 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-271 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-272 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkShow(d) | An Axiom |
| disj-273 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) ≠ mkStart | An Axiom |
| disj-274 | ⊦ mkGetDeclassifiedCCD ≠ mkGetFlightOffers(a_RequestData) | An Axiom |
| disj-275 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputAgent | An Axiom |
| disj-276 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputAirline | An Axiom |
| disj-277 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputBoolean | An Axiom |
| disj-278 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-279 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-280 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputData | An Axiom |
| disj-281 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputFlightOffer | An Axiom |
| disj-282 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputGPSPos | An Axiom |
| disj-283 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputIFlowUtil | An Axiom |
| disj-284 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputInteger | An Axiom |
| disj-285 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputRequestData | An Axiom |
| disj-286 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputString | An Axiom |
| disj-287 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputTravelAgency | An Axiom |
| disj-288 | ⊦ mkGetDeclassifiedCCD ≠ mkGetInputTravelPlanner | An Axiom |
| disj-289 | ⊦ mkGetDeclassifiedCCD ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-290 | ⊦ mkGetDeclassifiedCCD ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-291 | ⊦ mkGetDeclassifiedCCD ≠ mkOkConfirmBooking | An Axiom |
| disj-292 | ⊦ mkGetDeclassifiedCCD ≠ mkOkPayCommission | An Axiom |
| disj-293 | ⊦ mkGetDeclassifiedCCD ≠ mkPayCommission | An Axiom |
| disj-294 | ⊦ mkGetDeclassifiedCCD ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-295 | ⊦ mkGetDeclassifiedCCD ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-296 | ⊦ mkGetDeclassifiedCCD ≠ mkShow(d) | An Axiom |
| disj-297 | ⊦ mkGetDeclassifiedCCD ≠ mkStart | An Axiom |
| disj-298 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputAgent | An Axiom |
| disj-299 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputAirline | An Axiom |
| disj-300 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputBoolean | An Axiom |
| disj-301 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-302 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-303 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputData | An Axiom |
| disj-304 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputFlightOffer | An Axiom |
| disj-305 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputGPSPos | An Axiom |
| disj-306 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputIFlowUtil | An Axiom |
| disj-307 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputInteger | An Axiom |
| disj-308 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputRequestData | An Axiom |
| disj-309 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputString | An Axiom |
| disj-310 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputTravelAgency | An Axiom |
| disj-311 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetInputTravelPlanner | An Axiom |
| disj-312 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-313 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-314 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkOkConfirmBooking | An Axiom |
| disj-315 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkOkPayCommission | An Axiom |
| disj-316 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkPayCommission | An Axiom |
| disj-317 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-318 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-319 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkShow(d) | An Axiom |
| disj-320 | ⊦ mkGetFlightOffers(a_RequestData) ≠ mkStart | An Axiom |
| disj-321 | ⊦ mkGetInputAgent ≠ mkGetInputAirline | An Axiom |
| disj-322 | ⊦ mkGetInputAgent ≠ mkGetInputBoolean | An Axiom |
| disj-323 | ⊦ mkGetInputAgent ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-324 | ⊦ mkGetInputAgent ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-325 | ⊦ mkGetInputAgent ≠ mkGetInputData | An Axiom |
| disj-326 | ⊦ mkGetInputAgent ≠ mkGetInputFlightOffer | An Axiom |
| disj-327 | ⊦ mkGetInputAgent ≠ mkGetInputGPSPos | An Axiom |
| disj-328 | ⊦ mkGetInputAgent ≠ mkGetInputIFlowUtil | An Axiom |
| disj-329 | ⊦ mkGetInputAgent ≠ mkGetInputInteger | An Axiom |
| disj-330 | ⊦ mkGetInputAgent ≠ mkGetInputRequestData | An Axiom |
| disj-331 | ⊦ mkGetInputAgent ≠ mkGetInputString | An Axiom |
| disj-332 | ⊦ mkGetInputAgent ≠ mkGetInputTravelAgency | An Axiom |
| disj-333 | ⊦ mkGetInputAgent ≠ mkGetInputTravelPlanner | An Axiom |
| disj-334 | ⊦ mkGetInputAgent ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-335 | ⊦ mkGetInputAgent ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-336 | ⊦ mkGetInputAgent ≠ mkOkConfirmBooking | An Axiom |
| disj-337 | ⊦ mkGetInputAgent ≠ mkOkPayCommission | An Axiom |
| disj-338 | ⊦ mkGetInputAgent ≠ mkPayCommission | An Axiom |
| disj-339 | ⊦ mkGetInputAgent ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-340 | ⊦ mkGetInputAgent ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-341 | ⊦ mkGetInputAgent ≠ mkShow(d) | An Axiom |
| disj-342 | ⊦ mkGetInputAgent ≠ mkStart | An Axiom |
| disj-343 | ⊦ mkGetInputAirline ≠ mkGetInputBoolean | An Axiom |
| disj-344 | ⊦ mkGetInputAirline ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-345 | ⊦ mkGetInputAirline ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-346 | ⊦ mkGetInputAirline ≠ mkGetInputData | An Axiom |
| disj-347 | ⊦ mkGetInputAirline ≠ mkGetInputFlightOffer | An Axiom |
| disj-348 | ⊦ mkGetInputAirline ≠ mkGetInputGPSPos | An Axiom |
| disj-349 | ⊦ mkGetInputAirline ≠ mkGetInputIFlowUtil | An Axiom |
| disj-350 | ⊦ mkGetInputAirline ≠ mkGetInputInteger | An Axiom |
| disj-351 | ⊦ mkGetInputAirline ≠ mkGetInputRequestData | An Axiom |
| disj-352 | ⊦ mkGetInputAirline ≠ mkGetInputString | An Axiom |
| disj-353 | ⊦ mkGetInputAirline ≠ mkGetInputTravelAgency | An Axiom |
| disj-354 | ⊦ mkGetInputAirline ≠ mkGetInputTravelPlanner | An Axiom |
| disj-355 | ⊦ mkGetInputAirline ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-356 | ⊦ mkGetInputAirline ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-357 | ⊦ mkGetInputAirline ≠ mkOkConfirmBooking | An Axiom |
| disj-358 | ⊦ mkGetInputAirline ≠ mkOkPayCommission | An Axiom |
| disj-359 | ⊦ mkGetInputAirline ≠ mkPayCommission | An Axiom |
| disj-360 | ⊦ mkGetInputAirline ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-361 | ⊦ mkGetInputAirline ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-362 | ⊦ mkGetInputAirline ≠ mkShow(d) | An Axiom |
| disj-363 | ⊦ mkGetInputAirline ≠ mkStart | An Axiom |
| disj-364 | ⊦ mkGetInputBoolean ≠ mkGetInputCreditCardCenter | An Axiom |
| disj-365 | ⊦ mkGetInputBoolean ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-366 | ⊦ mkGetInputBoolean ≠ mkGetInputData | An Axiom |
| disj-367 | ⊦ mkGetInputBoolean ≠ mkGetInputFlightOffer | An Axiom |
| disj-368 | ⊦ mkGetInputBoolean ≠ mkGetInputGPSPos | An Axiom |
| disj-369 | ⊦ mkGetInputBoolean ≠ mkGetInputIFlowUtil | An Axiom |
| disj-370 | ⊦ mkGetInputBoolean ≠ mkGetInputInteger | An Axiom |
| disj-371 | ⊦ mkGetInputBoolean ≠ mkGetInputRequestData | An Axiom |
| disj-372 | ⊦ mkGetInputBoolean ≠ mkGetInputString | An Axiom |
| disj-373 | ⊦ mkGetInputBoolean ≠ mkGetInputTravelAgency | An Axiom |
| disj-374 | ⊦ mkGetInputBoolean ≠ mkGetInputTravelPlanner | An Axiom |
| disj-375 | ⊦ mkGetInputBoolean ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-376 | ⊦ mkGetInputBoolean ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-377 | ⊦ mkGetInputBoolean ≠ mkOkConfirmBooking | An Axiom |
| disj-378 | ⊦ mkGetInputBoolean ≠ mkOkPayCommission | An Axiom |
| disj-379 | ⊦ mkGetInputBoolean ≠ mkPayCommission | An Axiom |
| disj-380 | ⊦ mkGetInputBoolean ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-381 | ⊦ mkGetInputBoolean ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-382 | ⊦ mkGetInputBoolean ≠ mkShow(d) | An Axiom |
| disj-383 | ⊦ mkGetInputBoolean ≠ mkStart | An Axiom |
| disj-384 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputCreditCardDetails | An Axiom |
| disj-385 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputData | An Axiom |
| disj-386 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputFlightOffer | An Axiom |
| disj-387 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputGPSPos | An Axiom |
| disj-388 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputIFlowUtil | An Axiom |
| disj-389 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputInteger | An Axiom |
| disj-390 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputRequestData | An Axiom |
| disj-391 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputString | An Axiom |
| disj-392 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputTravelAgency | An Axiom |
| disj-393 | ⊦ mkGetInputCreditCardCenter ≠ mkGetInputTravelPlanner | An Axiom |
| disj-394 | ⊦ mkGetInputCreditCardCenter ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-395 | ⊦ mkGetInputCreditCardCenter ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-396 | ⊦ mkGetInputCreditCardCenter ≠ mkOkConfirmBooking | An Axiom |
| disj-397 | ⊦ mkGetInputCreditCardCenter ≠ mkOkPayCommission | An Axiom |
| disj-398 | ⊦ mkGetInputCreditCardCenter ≠ mkPayCommission | An Axiom |
| disj-399 | ⊦ mkGetInputCreditCardCenter ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-400 | ⊦ mkGetInputCreditCardCenter ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-401 | ⊦ mkGetInputCreditCardCenter ≠ mkShow(d) | An Axiom |
| disj-402 | ⊦ mkGetInputCreditCardCenter ≠ mkStart | An Axiom |
| disj-403 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputData | An Axiom |
| disj-404 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputFlightOffer | An Axiom |
| disj-405 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputGPSPos | An Axiom |
| disj-406 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputIFlowUtil | An Axiom |
| disj-407 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputInteger | An Axiom |
| disj-408 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputRequestData | An Axiom |
| disj-409 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputString | An Axiom |
| disj-410 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputTravelAgency | An Axiom |
| disj-411 | ⊦ mkGetInputCreditCardDetails ≠ mkGetInputTravelPlanner | An Axiom |
| disj-412 | ⊦ mkGetInputCreditCardDetails ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-413 | ⊦ mkGetInputCreditCardDetails ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-414 | ⊦ mkGetInputCreditCardDetails ≠ mkOkConfirmBooking | An Axiom |
| disj-415 | ⊦ mkGetInputCreditCardDetails ≠ mkOkPayCommission | An Axiom |
| disj-416 | ⊦ mkGetInputCreditCardDetails ≠ mkPayCommission | An Axiom |
| disj-417 | ⊦ mkGetInputCreditCardDetails ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-418 | ⊦ mkGetInputCreditCardDetails ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-419 | ⊦ mkGetInputCreditCardDetails ≠ mkShow(d) | An Axiom |
| disj-420 | ⊦ mkGetInputCreditCardDetails ≠ mkStart | An Axiom |
| disj-421 | ⊦ mkGetInputData ≠ mkGetInputFlightOffer | An Axiom |
| disj-422 | ⊦ mkGetInputData ≠ mkGetInputGPSPos | An Axiom |
| disj-423 | ⊦ mkGetInputData ≠ mkGetInputIFlowUtil | An Axiom |
| disj-424 | ⊦ mkGetInputData ≠ mkGetInputInteger | An Axiom |
| disj-425 | ⊦ mkGetInputData ≠ mkGetInputRequestData | An Axiom |
| disj-426 | ⊦ mkGetInputData ≠ mkGetInputString | An Axiom |
| disj-427 | ⊦ mkGetInputData ≠ mkGetInputTravelAgency | An Axiom |
| disj-428 | ⊦ mkGetInputData ≠ mkGetInputTravelPlanner | An Axiom |
| disj-429 | ⊦ mkGetInputData ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-430 | ⊦ mkGetInputData ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-431 | ⊦ mkGetInputData ≠ mkOkConfirmBooking | An Axiom |
| disj-432 | ⊦ mkGetInputData ≠ mkOkPayCommission | An Axiom |
| disj-433 | ⊦ mkGetInputData ≠ mkPayCommission | An Axiom |
| disj-434 | ⊦ mkGetInputData ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-435 | ⊦ mkGetInputData ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-436 | ⊦ mkGetInputData ≠ mkShow(d) | An Axiom |
| disj-437 | ⊦ mkGetInputData ≠ mkStart | An Axiom |
| disj-438 | ⊦ mkGetInputFlightOffer ≠ mkGetInputGPSPos | An Axiom |
| disj-439 | ⊦ mkGetInputFlightOffer ≠ mkGetInputIFlowUtil | An Axiom |
| disj-440 | ⊦ mkGetInputFlightOffer ≠ mkGetInputInteger | An Axiom |
| disj-441 | ⊦ mkGetInputFlightOffer ≠ mkGetInputRequestData | An Axiom |
| disj-442 | ⊦ mkGetInputFlightOffer ≠ mkGetInputString | An Axiom |
| disj-443 | ⊦ mkGetInputFlightOffer ≠ mkGetInputTravelAgency | An Axiom |
| disj-444 | ⊦ mkGetInputFlightOffer ≠ mkGetInputTravelPlanner | An Axiom |
| disj-445 | ⊦ mkGetInputFlightOffer ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-446 | ⊦ mkGetInputFlightOffer ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-447 | ⊦ mkGetInputFlightOffer ≠ mkOkConfirmBooking | An Axiom |
| disj-448 | ⊦ mkGetInputFlightOffer ≠ mkOkPayCommission | An Axiom |
| disj-449 | ⊦ mkGetInputFlightOffer ≠ mkPayCommission | An Axiom |
| disj-450 | ⊦ mkGetInputFlightOffer ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-451 | ⊦ mkGetInputFlightOffer ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-452 | ⊦ mkGetInputFlightOffer ≠ mkShow(d) | An Axiom |
| disj-453 | ⊦ mkGetInputFlightOffer ≠ mkStart | An Axiom |
| disj-454 | ⊦ mkGetInputGPSPos ≠ mkGetInputIFlowUtil | An Axiom |
| disj-455 | ⊦ mkGetInputGPSPos ≠ mkGetInputInteger | An Axiom |
| disj-456 | ⊦ mkGetInputGPSPos ≠ mkGetInputRequestData | An Axiom |
| disj-457 | ⊦ mkGetInputGPSPos ≠ mkGetInputString | An Axiom |
| disj-458 | ⊦ mkGetInputGPSPos ≠ mkGetInputTravelAgency | An Axiom |
| disj-459 | ⊦ mkGetInputGPSPos ≠ mkGetInputTravelPlanner | An Axiom |
| disj-460 | ⊦ mkGetInputGPSPos ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-461 | ⊦ mkGetInputGPSPos ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-462 | ⊦ mkGetInputGPSPos ≠ mkOkConfirmBooking | An Axiom |
| disj-463 | ⊦ mkGetInputGPSPos ≠ mkOkPayCommission | An Axiom |
| disj-464 | ⊦ mkGetInputGPSPos ≠ mkPayCommission | An Axiom |
| disj-465 | ⊦ mkGetInputGPSPos ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-466 | ⊦ mkGetInputGPSPos ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-467 | ⊦ mkGetInputGPSPos ≠ mkShow(d) | An Axiom |
| disj-468 | ⊦ mkGetInputGPSPos ≠ mkStart | An Axiom |
| disj-469 | ⊦ mkGetInputIFlowUtil ≠ mkGetInputInteger | An Axiom |
| disj-470 | ⊦ mkGetInputIFlowUtil ≠ mkGetInputRequestData | An Axiom |
| disj-471 | ⊦ mkGetInputIFlowUtil ≠ mkGetInputString | An Axiom |
| disj-472 | ⊦ mkGetInputIFlowUtil ≠ mkGetInputTravelAgency | An Axiom |
| disj-473 | ⊦ mkGetInputIFlowUtil ≠ mkGetInputTravelPlanner | An Axiom |
| disj-474 | ⊦ mkGetInputIFlowUtil ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-475 | ⊦ mkGetInputIFlowUtil ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-476 | ⊦ mkGetInputIFlowUtil ≠ mkOkConfirmBooking | An Axiom |
| disj-477 | ⊦ mkGetInputIFlowUtil ≠ mkOkPayCommission | An Axiom |
| disj-478 | ⊦ mkGetInputIFlowUtil ≠ mkPayCommission | An Axiom |
| disj-479 | ⊦ mkGetInputIFlowUtil ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-480 | ⊦ mkGetInputIFlowUtil ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-481 | ⊦ mkGetInputIFlowUtil ≠ mkShow(d) | An Axiom |
| disj-482 | ⊦ mkGetInputIFlowUtil ≠ mkStart | An Axiom |
| disj-483 | ⊦ mkGetInputInteger ≠ mkGetInputRequestData | An Axiom |
| disj-484 | ⊦ mkGetInputInteger ≠ mkGetInputString | An Axiom |
| disj-485 | ⊦ mkGetInputInteger ≠ mkGetInputTravelAgency | An Axiom |
| disj-486 | ⊦ mkGetInputInteger ≠ mkGetInputTravelPlanner | An Axiom |
| disj-487 | ⊦ mkGetInputInteger ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-488 | ⊦ mkGetInputInteger ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-489 | ⊦ mkGetInputInteger ≠ mkOkConfirmBooking | An Axiom |
| disj-490 | ⊦ mkGetInputInteger ≠ mkOkPayCommission | An Axiom |
| disj-491 | ⊦ mkGetInputInteger ≠ mkPayCommission | An Axiom |
| disj-492 | ⊦ mkGetInputInteger ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-493 | ⊦ mkGetInputInteger ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-494 | ⊦ mkGetInputInteger ≠ mkShow(d) | An Axiom |
| disj-495 | ⊦ mkGetInputInteger ≠ mkStart | An Axiom |
| disj-496 | ⊦ mkGetInputRequestData ≠ mkGetInputString | An Axiom |
| disj-497 | ⊦ mkGetInputRequestData ≠ mkGetInputTravelAgency | An Axiom |
| disj-498 | ⊦ mkGetInputRequestData ≠ mkGetInputTravelPlanner | An Axiom |
| disj-499 | ⊦ mkGetInputRequestData ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-500 | ⊦ mkGetInputRequestData ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-501 | ⊦ mkGetInputRequestData ≠ mkOkConfirmBooking | An Axiom |
| disj-502 | ⊦ mkGetInputRequestData ≠ mkOkPayCommission | An Axiom |
| disj-503 | ⊦ mkGetInputRequestData ≠ mkPayCommission | An Axiom |
| disj-504 | ⊦ mkGetInputRequestData ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-505 | ⊦ mkGetInputRequestData ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-506 | ⊦ mkGetInputRequestData ≠ mkShow(d) | An Axiom |
| disj-507 | ⊦ mkGetInputRequestData ≠ mkStart | An Axiom |
| disj-508 | ⊦ mkGetInputString ≠ mkGetInputTravelAgency | An Axiom |
| disj-509 | ⊦ mkGetInputString ≠ mkGetInputTravelPlanner | An Axiom |
| disj-510 | ⊦ mkGetInputString ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-511 | ⊦ mkGetInputString ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-512 | ⊦ mkGetInputString ≠ mkOkConfirmBooking | An Axiom |
| disj-513 | ⊦ mkGetInputString ≠ mkOkPayCommission | An Axiom |
| disj-514 | ⊦ mkGetInputString ≠ mkPayCommission | An Axiom |
| disj-515 | ⊦ mkGetInputString ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-516 | ⊦ mkGetInputString ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-517 | ⊦ mkGetInputString ≠ mkShow(d) | An Axiom |
| disj-518 | ⊦ mkGetInputString ≠ mkStart | An Axiom |
| disj-519 | ⊦ mkGetInputTravelAgency ≠ mkGetInputTravelPlanner | An Axiom |
| disj-520 | ⊦ mkGetInputTravelAgency ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-521 | ⊦ mkGetInputTravelAgency ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-522 | ⊦ mkGetInputTravelAgency ≠ mkOkConfirmBooking | An Axiom |
| disj-523 | ⊦ mkGetInputTravelAgency ≠ mkOkPayCommission | An Axiom |
| disj-524 | ⊦ mkGetInputTravelAgency ≠ mkPayCommission | An Axiom |
| disj-525 | ⊦ mkGetInputTravelAgency ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-526 | ⊦ mkGetInputTravelAgency ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-527 | ⊦ mkGetInputTravelAgency ≠ mkShow(d) | An Axiom |
| disj-528 | ⊦ mkGetInputTravelAgency ≠ mkStart | An Axiom |
| disj-529 | ⊦ mkGetInputTravelPlanner ≠ mkGetMultipleSelection(dl) | An Axiom |
| disj-530 | ⊦ mkGetInputTravelPlanner ≠ mkGetSingleSelection(dl) | An Axiom |
| disj-531 | ⊦ mkGetInputTravelPlanner ≠ mkOkConfirmBooking | An Axiom |
| disj-532 | ⊦ mkGetInputTravelPlanner ≠ mkOkPayCommission | An Axiom |
| disj-533 | ⊦ mkGetInputTravelPlanner ≠ mkPayCommission | An Axiom |
| disj-534 | ⊦ mkGetInputTravelPlanner ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-535 | ⊦ mkGetInputTravelPlanner ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-536 | ⊦ mkGetInputTravelPlanner ≠ mkShow(d) | An Axiom |
| disj-537 | ⊦ mkGetInputTravelPlanner ≠ mkStart | An Axiom |
| disj-538 | ⊦ mkGetMultipleSelection(dl) ≠ mkGetSingleSelection(dl0) | An Axiom |
| disj-539 | ⊦ mkGetMultipleSelection(dl) ≠ mkOkConfirmBooking | An Axiom |
| disj-540 | ⊦ mkGetMultipleSelection(dl) ≠ mkOkPayCommission | An Axiom |
| disj-541 | ⊦ mkGetMultipleSelection(dl) ≠ mkPayCommission | An Axiom |
| disj-542 | ⊦ mkGetMultipleSelection(dl) ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-543 | ⊦ mkGetMultipleSelection(dl) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-544 | ⊦ mkGetMultipleSelection(dl) ≠ mkShow(d) | An Axiom |
| disj-545 | ⊦ mkGetMultipleSelection(dl) ≠ mkStart | An Axiom |
| disj-546 | ⊦ mkGetSingleSelection(dl) ≠ mkOkConfirmBooking | An Axiom |
| disj-547 | ⊦ mkGetSingleSelection(dl) ≠ mkOkPayCommission | An Axiom |
| disj-548 | ⊦ mkGetSingleSelection(dl) ≠ mkPayCommission | An Axiom |
| disj-549 | ⊦ mkGetSingleSelection(dl) ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-550 | ⊦ mkGetSingleSelection(dl) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-551 | ⊦ mkGetSingleSelection(dl) ≠ mkShow(d) | An Axiom |
| disj-552 | ⊦ mkGetSingleSelection(dl) ≠ mkStart | An Axiom |
| disj-553 | ⊦ mkOkConfirmBooking ≠ mkOkPayCommission | An Axiom |
| disj-554 | ⊦ mkOkConfirmBooking ≠ mkPayCommission | An Axiom |
| disj-555 | ⊦ mkOkConfirmBooking ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-556 | ⊦ mkOkConfirmBooking ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-557 | ⊦ mkOkConfirmBooking ≠ mkShow(d) | An Axiom |
| disj-558 | ⊦ mkOkConfirmBooking ≠ mkStart | An Axiom |
| disj-559 | ⊦ mkOkPayCommission ≠ mkPayCommission | An Axiom |
| disj-560 | ⊦ mkOkPayCommission ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-561 | ⊦ mkOkPayCommission ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-562 | ⊦ mkOkPayCommission ≠ mkShow(d) | An Axiom |
| disj-563 | ⊦ mkOkPayCommission ≠ mkStart | An Axiom |
| disj-564 | ⊦ mkPayCommission ≠ mkReleaseCCD(a_String) | An Axiom |
| disj-565 | ⊦ mkPayCommission ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-566 | ⊦ mkPayCommission ≠ mkShow(d) | An Axiom |
| disj-567 | ⊦ mkPayCommission ≠ mkStart | An Axiom |
| disj-568 | ⊦ mkReleaseCCD(a_String) ≠ mkRetFlightOffers(a_ListOfFlightOffer) | An Axiom |
| disj-569 | ⊦ mkReleaseCCD(a_String) ≠ mkShow(d) | An Axiom |
| disj-570 | ⊦ mkReleaseCCD(a_String) ≠ mkStart | An Axiom |
| disj-571 | ⊦ mkRetFlightOffers(a_ListOfFlightOffer) ≠ mkShow(d) | An Axiom |
| disj-572 | ⊦ mkRetFlightOffers(a_ListOfFlightOffer) ≠ mkStart | An Axiom |
| disj-573 | ⊦ mkShow(d) ≠ mkStart | An Axiom |
| sel-01 | ⊦ (d + dl) .rest = dl | An Axiom |
| sel-02 | ⊦ (d + dl) .first = d | An Axiom |
| sel-03 | ⊦ (a_GPSPos + a_ListOfGPSPos) .rest = a_ListOfGPSPos | An Axiom |
| sel-04 | ⊦ (a_GPSPos + a_ListOfGPSPos) .first = a_GPSPos | An Axiom |
| sel-05 | ⊦ (a_FlightOffer + a_ListOfFlightOffer) .rest = a_ListOfFlightOffer | An Axiom |
| sel-06 | ⊦ (a_FlightOffer + a_ListOfFlightOffer) .first = a_FlightOffer | An Axiom |
| sel-07 | ⊦ mkDataPair(d, d0) .2 = d0 | An Axiom |
| sel-08 | ⊦ mkDataPair(d, d0) .1 = d | An Axiom |
| sel-09 | ⊦ mkNat(m) .nat = m | An Axiom |
| sel-10 | ⊦ wrapAgent2Data(ag) .Agent = ag | An Axiom |
| sel-11 | ⊦ wrapListOfData2Data(dl) .ListOfData = dl | An Axiom |
| sel-12 | ⊦ wrapListOfGPSPos2Data(a_ListOfGPSPos) .ListOfGPSPos = a_ListOfGPSPos | An Axiom |
| sel-13 | ⊦ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) .ListOfFlightOffer = a_ListOfFlightOffer | An Axiom |
| sel-14 | ⊦ wrapString2Data(a_String) .String = a_String | An Axiom |
| sel-15 | ⊦ wrapRequestData2Data(a_RequestData) .RequestData = a_RequestData | An Axiom |
| sel-16 | ⊦ wrapInteger2Data(a_Integer) .Integer = a_Integer | An Axiom |
| sel-17 | ⊦ wrapGPSPos2Data(a_GPSPos) .GPSPos = a_GPSPos | An Axiom |
| sel-18 | ⊦ wrapFlightOffer2Data(a_FlightOffer) .FlightOffer = a_FlightOffer | An Axiom |
| sel-19 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) .CreditCardDetails = a_CreditCardDetails | An Axiom |
| sel-20 | ⊦ wrapBoolean2Data(a_Boolean) .Boolean = a_Boolean | An Axiom |
| sel-21 | ⊦ wrapMessage2Data(msg) .msg = msg | An Axiom |
| sel-22 | ⊦ mkString(stringvar) .value = stringvar | An Axiom |
| sel-23 | ⊦ mkRequestData(a_String) .date = a_String | An Axiom |
| sel-24 | ⊦ mkInteger(i) .value = i | An Axiom |
| sel-25 | ⊦ mkGPSPos(a_String, a_String0) .longitude = a_String0 | An Axiom |
| sel-26 | ⊦ mkGPSPos(a_String, a_String0) .latitude = a_String | An Axiom |
| sel-27 | ⊦ mkFlightOffer(a_Integer, a_String) .airline = a_String | An Axiom |
| sel-28 | ⊦ mkFlightOffer(a_Integer, a_String) .id = a_Integer | An Axiom |
| sel-29 | ⊦ mkBoolean(boolvar) .value ↔ boolvar | An Axiom |
| sel-30 | ⊦ mkShow(d) .data = d | An Axiom |
| sel-31 | ⊦ mkRetFlightOffers(a_ListOfFlightOffer) .flightOffers = a_ListOfFlightOffer | An Axiom |
| sel-32 | ⊦ mkReleaseCCD(a_String) .receiver = a_String | An Axiom |
| sel-33 | ⊦ mkGetSingleSelection(dl) .selection = dl | An Axiom |
| sel-34 | ⊦ mkGetMultipleSelection(dl) .selection = dl | An Axiom |
| sel-35 | ⊦ mkGetFlightOffers(a_RequestData) .requestData = a_RequestData | An Axiom |
| sel-36 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) .ccd = a_CreditCardDetails | An Axiom |
| sel-37 | ⊦ mkConfirmRelease(d, a_String) .receiver = a_String | An Axiom |
| sel-38 | ⊦ mkConfirmRelease(d, a_String) .what = d | An Axiom |
| sel-39 | ⊦ mkConfirmBooking(a_Integer) .id = a_Integer | An Axiom |
| sel-40 | ⊦ mkBookSelected(a_FlightOffer) .flightOffer = a_FlightOffer | An Axiom |
| sel-41 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) .ccd = a_CreditCardDetails | An Axiom |
| sel-42 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) .id = a_Integer | An Axiom |
| sel-43 | ⊦ mkMessage(agl, cntnt) .content = cntnt | An Axiom |
| sel-44 | ⊦ mkMessage(agl, cntnt) .agentlist = agl | An Axiom |
| test-01 | ⊦ ¬ isPair(null) | An Axiom |
| test-02 | ⊦ isPair(mkDataPair(d, d0)) | An Axiom |
| test-03 | ⊦ ¬ isPair(mkNat(m)) | An Axiom |
| test-04 | ⊦ ¬ isPair(wrapAgent2Data(ag)) | An Axiom |
| test-05 | ⊦ ¬ isPair(wrapListOfData2Data(dl)) | An Axiom |
| test-06 | ⊦ ¬ isPair(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-07 | ⊦ ¬ isPair(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-08 | ⊦ ¬ isPair(wrapString2Data(a_String)) | An Axiom |
| test-09 | ⊦ ¬ isPair(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-10 | ⊦ ¬ isPair(wrapInteger2Data(a_Integer)) | An Axiom |
| test-11 | ⊦ ¬ isPair(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-12 | ⊦ ¬ isPair(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-13 | ⊦ ¬ isPair(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-14 | ⊦ ¬ isPair(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-15 | ⊦ ¬ isPair(wrapMessage2Data(msg)) | An Axiom |
| test-16 | ⊦ ¬ isNat(null) | An Axiom |
| test-17 | ⊦ ¬ isNat(mkDataPair(d, d0)) | An Axiom |
| test-18 | ⊦ isNat(mkNat(m)) | An Axiom |
| test-19 | ⊦ ¬ isNat(wrapAgent2Data(ag)) | An Axiom |
| test-20 | ⊦ ¬ isNat(wrapListOfData2Data(dl)) | An Axiom |
| test-21 | ⊦ ¬ isNat(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-22 | ⊦ ¬ isNat(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-23 | ⊦ ¬ isNat(wrapString2Data(a_String)) | An Axiom |
| test-24 | ⊦ ¬ isNat(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-25 | ⊦ ¬ isNat(wrapInteger2Data(a_Integer)) | An Axiom |
| test-26 | ⊦ ¬ isNat(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-27 | ⊦ ¬ isNat(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-28 | ⊦ ¬ isNat(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-29 | ⊦ ¬ isNat(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-30 | ⊦ ¬ isNat(wrapMessage2Data(msg)) | An Axiom |
| test-31 | ⊦ ¬ isAgent(null) | An Axiom |
| test-32 | ⊦ ¬ isAgent(mkDataPair(d, d0)) | An Axiom |
| test-33 | ⊦ ¬ isAgent(mkNat(m)) | An Axiom |
| test-34 | ⊦ isAgent(wrapAgent2Data(ag)) | An Axiom |
| test-35 | ⊦ ¬ isAgent(wrapListOfData2Data(dl)) | An Axiom |
| test-36 | ⊦ ¬ isAgent(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-37 | ⊦ ¬ isAgent(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-38 | ⊦ ¬ isAgent(wrapString2Data(a_String)) | An Axiom |
| test-39 | ⊦ ¬ isAgent(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-40 | ⊦ ¬ isAgent(wrapInteger2Data(a_Integer)) | An Axiom |
| test-41 | ⊦ ¬ isAgent(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-42 | ⊦ ¬ isAgent(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-43 | ⊦ ¬ isAgent(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-44 | ⊦ ¬ isAgent(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-45 | ⊦ ¬ isAgent(wrapMessage2Data(msg)) | An Axiom |
| test-46 | ⊦ ¬ isListOfData(null) | An Axiom |
| test-47 | ⊦ ¬ isListOfData(mkDataPair(d, d0)) | An Axiom |
| test-48 | ⊦ ¬ isListOfData(mkNat(m)) | An Axiom |
| test-49 | ⊦ ¬ isListOfData(wrapAgent2Data(ag)) | An Axiom |
| test-50 | ⊦ isListOfData(wrapListOfData2Data(dl)) | An Axiom |
| test-51 | ⊦ ¬ isListOfData(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-52 | ⊦ ¬ isListOfData(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-53 | ⊦ ¬ isListOfData(wrapString2Data(a_String)) | An Axiom |
| test-54 | ⊦ ¬ isListOfData(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-55 | ⊦ ¬ isListOfData(wrapInteger2Data(a_Integer)) | An Axiom |
| test-56 | ⊦ ¬ isListOfData(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-57 | ⊦ ¬ isListOfData(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-58 | ⊦ ¬ isListOfData(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-59 | ⊦ ¬ isListOfData(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-60 | ⊦ ¬ isListOfData(wrapMessage2Data(msg)) | An Axiom |
| test-61 | ⊦ ¬ isListOfGPSPos(null) | An Axiom |
| test-62 | ⊦ ¬ isListOfGPSPos(mkDataPair(d, d0)) | An Axiom |
| test-63 | ⊦ ¬ isListOfGPSPos(mkNat(m)) | An Axiom |
| test-64 | ⊦ ¬ isListOfGPSPos(wrapAgent2Data(ag)) | An Axiom |
| test-65 | ⊦ ¬ isListOfGPSPos(wrapListOfData2Data(dl)) | An Axiom |
| test-66 | ⊦ isListOfGPSPos(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-67 | ⊦ ¬ isListOfGPSPos(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-68 | ⊦ ¬ isListOfGPSPos(wrapString2Data(a_String)) | An Axiom |
| test-69 | ⊦ ¬ isListOfGPSPos(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-70 | ⊦ ¬ isListOfGPSPos(wrapInteger2Data(a_Integer)) | An Axiom |
| test-71 | ⊦ ¬ isListOfGPSPos(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-72 | ⊦ ¬ isListOfGPSPos(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-73 | ⊦ ¬ isListOfGPSPos(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-74 | ⊦ ¬ isListOfGPSPos(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-75 | ⊦ ¬ isListOfGPSPos(wrapMessage2Data(msg)) | An Axiom |
| test-76 | ⊦ ¬ isListOfFlightOffer(null) | An Axiom |
| test-77 | ⊦ ¬ isListOfFlightOffer(mkDataPair(d, d0)) | An Axiom |
| test-78 | ⊦ ¬ isListOfFlightOffer(mkNat(m)) | An Axiom |
| test-79 | ⊦ ¬ isListOfFlightOffer(wrapAgent2Data(ag)) | An Axiom |
| test-80 | ⊦ ¬ isListOfFlightOffer(wrapListOfData2Data(dl)) | An Axiom |
| test-81 | ⊦ ¬ isListOfFlightOffer(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-82 | ⊦ isListOfFlightOffer(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-83 | ⊦ ¬ isListOfFlightOffer(wrapString2Data(a_String)) | An Axiom |
| test-84 | ⊦ ¬ isListOfFlightOffer(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-85 | ⊦ ¬ isListOfFlightOffer(wrapInteger2Data(a_Integer)) | An Axiom |
| test-86 | ⊦ ¬ isListOfFlightOffer(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-87 | ⊦ ¬ isListOfFlightOffer(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-88 | ⊦ ¬ isListOfFlightOffer(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-89 | ⊦ ¬ isListOfFlightOffer(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-90 | ⊦ ¬ isListOfFlightOffer(wrapMessage2Data(msg)) | An Axiom |
| test-91 | ⊦ ¬ isString(null) | An Axiom |
| test-92 | ⊦ ¬ isString(mkDataPair(d, d0)) | An Axiom |
| test-93 | ⊦ ¬ isString(mkNat(m)) | An Axiom |
| test-94 | ⊦ ¬ isString(wrapAgent2Data(ag)) | An Axiom |
| test-95 | ⊦ ¬ isString(wrapListOfData2Data(dl)) | An Axiom |
| test-96 | ⊦ ¬ isString(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-97 | ⊦ ¬ isString(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-98 | ⊦ isString(wrapString2Data(a_String)) | An Axiom |
| test-99 | ⊦ ¬ isString(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-100 | ⊦ ¬ isString(wrapInteger2Data(a_Integer)) | An Axiom |
| test-101 | ⊦ ¬ isString(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-102 | ⊦ ¬ isString(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-103 | ⊦ ¬ isString(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-104 | ⊦ ¬ isString(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-105 | ⊦ ¬ isString(wrapMessage2Data(msg)) | An Axiom |
| test-106 | ⊦ ¬ isRequestData(null) | An Axiom |
| test-107 | ⊦ ¬ isRequestData(mkDataPair(d, d0)) | An Axiom |
| test-108 | ⊦ ¬ isRequestData(mkNat(m)) | An Axiom |
| test-109 | ⊦ ¬ isRequestData(wrapAgent2Data(ag)) | An Axiom |
| test-110 | ⊦ ¬ isRequestData(wrapListOfData2Data(dl)) | An Axiom |
| test-111 | ⊦ ¬ isRequestData(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-112 | ⊦ ¬ isRequestData(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-113 | ⊦ ¬ isRequestData(wrapString2Data(a_String)) | An Axiom |
| test-114 | ⊦ isRequestData(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-115 | ⊦ ¬ isRequestData(wrapInteger2Data(a_Integer)) | An Axiom |
| test-116 | ⊦ ¬ isRequestData(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-117 | ⊦ ¬ isRequestData(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-118 | ⊦ ¬ isRequestData(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-119 | ⊦ ¬ isRequestData(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-120 | ⊦ ¬ isRequestData(wrapMessage2Data(msg)) | An Axiom |
| test-121 | ⊦ ¬ isInteger(null) | An Axiom |
| test-122 | ⊦ ¬ isInteger(mkDataPair(d, d0)) | An Axiom |
| test-123 | ⊦ ¬ isInteger(mkNat(m)) | An Axiom |
| test-124 | ⊦ ¬ isInteger(wrapAgent2Data(ag)) | An Axiom |
| test-125 | ⊦ ¬ isInteger(wrapListOfData2Data(dl)) | An Axiom |
| test-126 | ⊦ ¬ isInteger(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-127 | ⊦ ¬ isInteger(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-128 | ⊦ ¬ isInteger(wrapString2Data(a_String)) | An Axiom |
| test-129 | ⊦ ¬ isInteger(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-130 | ⊦ isInteger(wrapInteger2Data(a_Integer)) | An Axiom |
| test-131 | ⊦ ¬ isInteger(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-132 | ⊦ ¬ isInteger(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-133 | ⊦ ¬ isInteger(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-134 | ⊦ ¬ isInteger(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-135 | ⊦ ¬ isInteger(wrapMessage2Data(msg)) | An Axiom |
| test-136 | ⊦ ¬ isGPSPos(null) | An Axiom |
| test-137 | ⊦ ¬ isGPSPos(mkDataPair(d, d0)) | An Axiom |
| test-138 | ⊦ ¬ isGPSPos(mkNat(m)) | An Axiom |
| test-139 | ⊦ ¬ isGPSPos(wrapAgent2Data(ag)) | An Axiom |
| test-140 | ⊦ ¬ isGPSPos(wrapListOfData2Data(dl)) | An Axiom |
| test-141 | ⊦ ¬ isGPSPos(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-142 | ⊦ ¬ isGPSPos(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-143 | ⊦ ¬ isGPSPos(wrapString2Data(a_String)) | An Axiom |
| test-144 | ⊦ ¬ isGPSPos(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-145 | ⊦ ¬ isGPSPos(wrapInteger2Data(a_Integer)) | An Axiom |
| test-146 | ⊦ isGPSPos(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-147 | ⊦ ¬ isGPSPos(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-148 | ⊦ ¬ isGPSPos(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-149 | ⊦ ¬ isGPSPos(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-150 | ⊦ ¬ isGPSPos(wrapMessage2Data(msg)) | An Axiom |
| test-151 | ⊦ ¬ isFlightOffer(null) | An Axiom |
| test-152 | ⊦ ¬ isFlightOffer(mkDataPair(d, d0)) | An Axiom |
| test-153 | ⊦ ¬ isFlightOffer(mkNat(m)) | An Axiom |
| test-154 | ⊦ ¬ isFlightOffer(wrapAgent2Data(ag)) | An Axiom |
| test-155 | ⊦ ¬ isFlightOffer(wrapListOfData2Data(dl)) | An Axiom |
| test-156 | ⊦ ¬ isFlightOffer(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-157 | ⊦ ¬ isFlightOffer(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-158 | ⊦ ¬ isFlightOffer(wrapString2Data(a_String)) | An Axiom |
| test-159 | ⊦ ¬ isFlightOffer(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-160 | ⊦ ¬ isFlightOffer(wrapInteger2Data(a_Integer)) | An Axiom |
| test-161 | ⊦ ¬ isFlightOffer(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-162 | ⊦ isFlightOffer(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-163 | ⊦ ¬ isFlightOffer(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-164 | ⊦ ¬ isFlightOffer(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-165 | ⊦ ¬ isFlightOffer(wrapMessage2Data(msg)) | An Axiom |
| test-166 | ⊦ ¬ isCreditCardDetails(null) | An Axiom |
| test-167 | ⊦ ¬ isCreditCardDetails(mkDataPair(d, d0)) | An Axiom |
| test-168 | ⊦ ¬ isCreditCardDetails(mkNat(m)) | An Axiom |
| test-169 | ⊦ ¬ isCreditCardDetails(wrapAgent2Data(ag)) | An Axiom |
| test-170 | ⊦ ¬ isCreditCardDetails(wrapListOfData2Data(dl)) | An Axiom |
| test-171 | ⊦ ¬ isCreditCardDetails(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-172 | ⊦ ¬ isCreditCardDetails(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-173 | ⊦ ¬ isCreditCardDetails(wrapString2Data(a_String)) | An Axiom |
| test-174 | ⊦ ¬ isCreditCardDetails(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-175 | ⊦ ¬ isCreditCardDetails(wrapInteger2Data(a_Integer)) | An Axiom |
| test-176 | ⊦ ¬ isCreditCardDetails(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-177 | ⊦ ¬ isCreditCardDetails(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-178 | ⊦ isCreditCardDetails(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-179 | ⊦ ¬ isCreditCardDetails(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-180 | ⊦ ¬ isCreditCardDetails(wrapMessage2Data(msg)) | An Axiom |
| test-181 | ⊦ ¬ isBoolean(null) | An Axiom |
| test-182 | ⊦ ¬ isBoolean(mkDataPair(d, d0)) | An Axiom |
| test-183 | ⊦ ¬ isBoolean(mkNat(m)) | An Axiom |
| test-184 | ⊦ ¬ isBoolean(wrapAgent2Data(ag)) | An Axiom |
| test-185 | ⊦ ¬ isBoolean(wrapListOfData2Data(dl)) | An Axiom |
| test-186 | ⊦ ¬ isBoolean(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-187 | ⊦ ¬ isBoolean(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-188 | ⊦ ¬ isBoolean(wrapString2Data(a_String)) | An Axiom |
| test-189 | ⊦ ¬ isBoolean(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-190 | ⊦ ¬ isBoolean(wrapInteger2Data(a_Integer)) | An Axiom |
| test-191 | ⊦ ¬ isBoolean(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-192 | ⊦ ¬ isBoolean(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-193 | ⊦ ¬ isBoolean(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-194 | ⊦ isBoolean(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-195 | ⊦ ¬ isBoolean(wrapMessage2Data(msg)) | An Axiom |
| test-196 | ⊦ ¬ isMessage(null) | An Axiom |
| test-197 | ⊦ ¬ isMessage(mkDataPair(d, d0)) | An Axiom |
| test-198 | ⊦ ¬ isMessage(mkNat(m)) | An Axiom |
| test-199 | ⊦ ¬ isMessage(wrapAgent2Data(ag)) | An Axiom |
| test-200 | ⊦ ¬ isMessage(wrapListOfData2Data(dl)) | An Axiom |
| test-201 | ⊦ ¬ isMessage(wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| test-202 | ⊦ ¬ isMessage(wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| test-203 | ⊦ ¬ isMessage(wrapString2Data(a_String)) | An Axiom |
| test-204 | ⊦ ¬ isMessage(wrapRequestData2Data(a_RequestData)) | An Axiom |
| test-205 | ⊦ ¬ isMessage(wrapInteger2Data(a_Integer)) | An Axiom |
| test-206 | ⊦ ¬ isMessage(wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| test-207 | ⊦ ¬ isMessage(wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| test-208 | ⊦ ¬ isMessage(wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| test-209 | ⊦ ¬ isMessage(wrapBoolean2Data(a_Boolean)) | An Axiom |
| test-210 | ⊦ isMessage(wrapMessage2Data(msg)) | An Axiom |
| test-211 | ⊦ isStart(mkStart) | An Axiom |
| test-212 | ⊦ ¬ isStart(mkShow(d)) | An Axiom |
| test-213 | ⊦ ¬ isStart(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-214 | ⊦ ¬ isStart(mkReleaseCCD(a_String)) | An Axiom |
| test-215 | ⊦ ¬ isStart(mkPayCommission) | An Axiom |
| test-216 | ⊦ ¬ isStart(mkOkPayCommission) | An Axiom |
| test-217 | ⊦ ¬ isStart(mkOkConfirmBooking) | An Axiom |
| test-218 | ⊦ ¬ isStart(mkGetSingleSelection(dl)) | An Axiom |
| test-219 | ⊦ ¬ isStart(mkGetMultipleSelection(dl)) | An Axiom |
| test-220 | ⊦ ¬ isStart(mkGetInputTravelPlanner) | An Axiom |
| test-221 | ⊦ ¬ isStart(mkGetInputTravelAgency) | An Axiom |
| test-222 | ⊦ ¬ isStart(mkGetInputString) | An Axiom |
| test-223 | ⊦ ¬ isStart(mkGetInputRequestData) | An Axiom |
| test-224 | ⊦ ¬ isStart(mkGetInputInteger) | An Axiom |
| test-225 | ⊦ ¬ isStart(mkGetInputIFlowUtil) | An Axiom |
| test-226 | ⊦ ¬ isStart(mkGetInputGPSPos) | An Axiom |
| test-227 | ⊦ ¬ isStart(mkGetInputFlightOffer) | An Axiom |
| test-228 | ⊦ ¬ isStart(mkGetInputData) | An Axiom |
| test-229 | ⊦ ¬ isStart(mkGetInputCreditCardDetails) | An Axiom |
| test-230 | ⊦ ¬ isStart(mkGetInputCreditCardCenter) | An Axiom |
| test-231 | ⊦ ¬ isStart(mkGetInputBoolean) | An Axiom |
| test-232 | ⊦ ¬ isStart(mkGetInputAirline) | An Axiom |
| test-233 | ⊦ ¬ isStart(mkGetInputAgent) | An Axiom |
| test-234 | ⊦ ¬ isStart(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-235 | ⊦ ¬ isStart(mkGetDeclassifiedCCD) | An Axiom |
| test-236 | ⊦ ¬ isStart(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-237 | ⊦ ¬ isStart(mkConfirmRelease(d, a_String)) | An Axiom |
| test-238 | ⊦ ¬ isStart(mkConfirmBooking(a_Integer)) | An Axiom |
| test-239 | ⊦ ¬ isStart(mkConfirm) | An Axiom |
| test-240 | ⊦ ¬ isStart(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-241 | ⊦ ¬ isStart(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-242 | ⊦ ¬ isShow(mkStart) | An Axiom |
| test-243 | ⊦ isShow(mkShow(d)) | An Axiom |
| test-244 | ⊦ ¬ isShow(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-245 | ⊦ ¬ isShow(mkReleaseCCD(a_String)) | An Axiom |
| test-246 | ⊦ ¬ isShow(mkPayCommission) | An Axiom |
| test-247 | ⊦ ¬ isShow(mkOkPayCommission) | An Axiom |
| test-248 | ⊦ ¬ isShow(mkOkConfirmBooking) | An Axiom |
| test-249 | ⊦ ¬ isShow(mkGetSingleSelection(dl)) | An Axiom |
| test-250 | ⊦ ¬ isShow(mkGetMultipleSelection(dl)) | An Axiom |
| test-251 | ⊦ ¬ isShow(mkGetInputTravelPlanner) | An Axiom |
| test-252 | ⊦ ¬ isShow(mkGetInputTravelAgency) | An Axiom |
| test-253 | ⊦ ¬ isShow(mkGetInputString) | An Axiom |
| test-254 | ⊦ ¬ isShow(mkGetInputRequestData) | An Axiom |
| test-255 | ⊦ ¬ isShow(mkGetInputInteger) | An Axiom |
| test-256 | ⊦ ¬ isShow(mkGetInputIFlowUtil) | An Axiom |
| test-257 | ⊦ ¬ isShow(mkGetInputGPSPos) | An Axiom |
| test-258 | ⊦ ¬ isShow(mkGetInputFlightOffer) | An Axiom |
| test-259 | ⊦ ¬ isShow(mkGetInputData) | An Axiom |
| test-260 | ⊦ ¬ isShow(mkGetInputCreditCardDetails) | An Axiom |
| test-261 | ⊦ ¬ isShow(mkGetInputCreditCardCenter) | An Axiom |
| test-262 | ⊦ ¬ isShow(mkGetInputBoolean) | An Axiom |
| test-263 | ⊦ ¬ isShow(mkGetInputAirline) | An Axiom |
| test-264 | ⊦ ¬ isShow(mkGetInputAgent) | An Axiom |
| test-265 | ⊦ ¬ isShow(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-266 | ⊦ ¬ isShow(mkGetDeclassifiedCCD) | An Axiom |
| test-267 | ⊦ ¬ isShow(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-268 | ⊦ ¬ isShow(mkConfirmRelease(d, a_String)) | An Axiom |
| test-269 | ⊦ ¬ isShow(mkConfirmBooking(a_Integer)) | An Axiom |
| test-270 | ⊦ ¬ isShow(mkConfirm) | An Axiom |
| test-271 | ⊦ ¬ isShow(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-272 | ⊦ ¬ isShow(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-273 | ⊦ ¬ isRetFlightOffers(mkStart) | An Axiom |
| test-274 | ⊦ ¬ isRetFlightOffers(mkShow(d)) | An Axiom |
| test-275 | ⊦ isRetFlightOffers(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-276 | ⊦ ¬ isRetFlightOffers(mkReleaseCCD(a_String)) | An Axiom |
| test-277 | ⊦ ¬ isRetFlightOffers(mkPayCommission) | An Axiom |
| test-278 | ⊦ ¬ isRetFlightOffers(mkOkPayCommission) | An Axiom |
| test-279 | ⊦ ¬ isRetFlightOffers(mkOkConfirmBooking) | An Axiom |
| test-280 | ⊦ ¬ isRetFlightOffers(mkGetSingleSelection(dl)) | An Axiom |
| test-281 | ⊦ ¬ isRetFlightOffers(mkGetMultipleSelection(dl)) | An Axiom |
| test-282 | ⊦ ¬ isRetFlightOffers(mkGetInputTravelPlanner) | An Axiom |
| test-283 | ⊦ ¬ isRetFlightOffers(mkGetInputTravelAgency) | An Axiom |
| test-284 | ⊦ ¬ isRetFlightOffers(mkGetInputString) | An Axiom |
| test-285 | ⊦ ¬ isRetFlightOffers(mkGetInputRequestData) | An Axiom |
| test-286 | ⊦ ¬ isRetFlightOffers(mkGetInputInteger) | An Axiom |
| test-287 | ⊦ ¬ isRetFlightOffers(mkGetInputIFlowUtil) | An Axiom |
| test-288 | ⊦ ¬ isRetFlightOffers(mkGetInputGPSPos) | An Axiom |
| test-289 | ⊦ ¬ isRetFlightOffers(mkGetInputFlightOffer) | An Axiom |
| test-290 | ⊦ ¬ isRetFlightOffers(mkGetInputData) | An Axiom |
| test-291 | ⊦ ¬ isRetFlightOffers(mkGetInputCreditCardDetails) | An Axiom |
| test-292 | ⊦ ¬ isRetFlightOffers(mkGetInputCreditCardCenter) | An Axiom |
| test-293 | ⊦ ¬ isRetFlightOffers(mkGetInputBoolean) | An Axiom |
| test-294 | ⊦ ¬ isRetFlightOffers(mkGetInputAirline) | An Axiom |
| test-295 | ⊦ ¬ isRetFlightOffers(mkGetInputAgent) | An Axiom |
| test-296 | ⊦ ¬ isRetFlightOffers(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-297 | ⊦ ¬ isRetFlightOffers(mkGetDeclassifiedCCD) | An Axiom |
| test-298 | ⊦ ¬ isRetFlightOffers(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-299 | ⊦ ¬ isRetFlightOffers(mkConfirmRelease(d, a_String)) | An Axiom |
| test-300 | ⊦ ¬ isRetFlightOffers(mkConfirmBooking(a_Integer)) | An Axiom |
| test-301 | ⊦ ¬ isRetFlightOffers(mkConfirm) | An Axiom |
| test-302 | ⊦ ¬ isRetFlightOffers(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-303 | ⊦ ¬ isRetFlightOffers(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-304 | ⊦ ¬ isReleaseCCD(mkStart) | An Axiom |
| test-305 | ⊦ ¬ isReleaseCCD(mkShow(d)) | An Axiom |
| test-306 | ⊦ ¬ isReleaseCCD(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-307 | ⊦ isReleaseCCD(mkReleaseCCD(a_String)) | An Axiom |
| test-308 | ⊦ ¬ isReleaseCCD(mkPayCommission) | An Axiom |
| test-309 | ⊦ ¬ isReleaseCCD(mkOkPayCommission) | An Axiom |
| test-310 | ⊦ ¬ isReleaseCCD(mkOkConfirmBooking) | An Axiom |
| test-311 | ⊦ ¬ isReleaseCCD(mkGetSingleSelection(dl)) | An Axiom |
| test-312 | ⊦ ¬ isReleaseCCD(mkGetMultipleSelection(dl)) | An Axiom |
| test-313 | ⊦ ¬ isReleaseCCD(mkGetInputTravelPlanner) | An Axiom |
| test-314 | ⊦ ¬ isReleaseCCD(mkGetInputTravelAgency) | An Axiom |
| test-315 | ⊦ ¬ isReleaseCCD(mkGetInputString) | An Axiom |
| test-316 | ⊦ ¬ isReleaseCCD(mkGetInputRequestData) | An Axiom |
| test-317 | ⊦ ¬ isReleaseCCD(mkGetInputInteger) | An Axiom |
| test-318 | ⊦ ¬ isReleaseCCD(mkGetInputIFlowUtil) | An Axiom |
| test-319 | ⊦ ¬ isReleaseCCD(mkGetInputGPSPos) | An Axiom |
| test-320 | ⊦ ¬ isReleaseCCD(mkGetInputFlightOffer) | An Axiom |
| test-321 | ⊦ ¬ isReleaseCCD(mkGetInputData) | An Axiom |
| test-322 | ⊦ ¬ isReleaseCCD(mkGetInputCreditCardDetails) | An Axiom |
| test-323 | ⊦ ¬ isReleaseCCD(mkGetInputCreditCardCenter) | An Axiom |
| test-324 | ⊦ ¬ isReleaseCCD(mkGetInputBoolean) | An Axiom |
| test-325 | ⊦ ¬ isReleaseCCD(mkGetInputAirline) | An Axiom |
| test-326 | ⊦ ¬ isReleaseCCD(mkGetInputAgent) | An Axiom |
| test-327 | ⊦ ¬ isReleaseCCD(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-328 | ⊦ ¬ isReleaseCCD(mkGetDeclassifiedCCD) | An Axiom |
| test-329 | ⊦ ¬ isReleaseCCD(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-330 | ⊦ ¬ isReleaseCCD(mkConfirmRelease(d, a_String)) | An Axiom |
| test-331 | ⊦ ¬ isReleaseCCD(mkConfirmBooking(a_Integer)) | An Axiom |
| test-332 | ⊦ ¬ isReleaseCCD(mkConfirm) | An Axiom |
| test-333 | ⊦ ¬ isReleaseCCD(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-334 | ⊦ ¬ isReleaseCCD(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-335 | ⊦ ¬ isPayCommission(mkStart) | An Axiom |
| test-336 | ⊦ ¬ isPayCommission(mkShow(d)) | An Axiom |
| test-337 | ⊦ ¬ isPayCommission(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-338 | ⊦ ¬ isPayCommission(mkReleaseCCD(a_String)) | An Axiom |
| test-339 | ⊦ isPayCommission(mkPayCommission) | An Axiom |
| test-340 | ⊦ ¬ isPayCommission(mkOkPayCommission) | An Axiom |
| test-341 | ⊦ ¬ isPayCommission(mkOkConfirmBooking) | An Axiom |
| test-342 | ⊦ ¬ isPayCommission(mkGetSingleSelection(dl)) | An Axiom |
| test-343 | ⊦ ¬ isPayCommission(mkGetMultipleSelection(dl)) | An Axiom |
| test-344 | ⊦ ¬ isPayCommission(mkGetInputTravelPlanner) | An Axiom |
| test-345 | ⊦ ¬ isPayCommission(mkGetInputTravelAgency) | An Axiom |
| test-346 | ⊦ ¬ isPayCommission(mkGetInputString) | An Axiom |
| test-347 | ⊦ ¬ isPayCommission(mkGetInputRequestData) | An Axiom |
| test-348 | ⊦ ¬ isPayCommission(mkGetInputInteger) | An Axiom |
| test-349 | ⊦ ¬ isPayCommission(mkGetInputIFlowUtil) | An Axiom |
| test-350 | ⊦ ¬ isPayCommission(mkGetInputGPSPos) | An Axiom |
| test-351 | ⊦ ¬ isPayCommission(mkGetInputFlightOffer) | An Axiom |
| test-352 | ⊦ ¬ isPayCommission(mkGetInputData) | An Axiom |
| test-353 | ⊦ ¬ isPayCommission(mkGetInputCreditCardDetails) | An Axiom |
| test-354 | ⊦ ¬ isPayCommission(mkGetInputCreditCardCenter) | An Axiom |
| test-355 | ⊦ ¬ isPayCommission(mkGetInputBoolean) | An Axiom |
| test-356 | ⊦ ¬ isPayCommission(mkGetInputAirline) | An Axiom |
| test-357 | ⊦ ¬ isPayCommission(mkGetInputAgent) | An Axiom |
| test-358 | ⊦ ¬ isPayCommission(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-359 | ⊦ ¬ isPayCommission(mkGetDeclassifiedCCD) | An Axiom |
| test-360 | ⊦ ¬ isPayCommission(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-361 | ⊦ ¬ isPayCommission(mkConfirmRelease(d, a_String)) | An Axiom |
| test-362 | ⊦ ¬ isPayCommission(mkConfirmBooking(a_Integer)) | An Axiom |
| test-363 | ⊦ ¬ isPayCommission(mkConfirm) | An Axiom |
| test-364 | ⊦ ¬ isPayCommission(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-365 | ⊦ ¬ isPayCommission(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-366 | ⊦ ¬ isOkPayCommission(mkStart) | An Axiom |
| test-367 | ⊦ ¬ isOkPayCommission(mkShow(d)) | An Axiom |
| test-368 | ⊦ ¬ isOkPayCommission(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-369 | ⊦ ¬ isOkPayCommission(mkReleaseCCD(a_String)) | An Axiom |
| test-370 | ⊦ ¬ isOkPayCommission(mkPayCommission) | An Axiom |
| test-371 | ⊦ isOkPayCommission(mkOkPayCommission) | An Axiom |
| test-372 | ⊦ ¬ isOkPayCommission(mkOkConfirmBooking) | An Axiom |
| test-373 | ⊦ ¬ isOkPayCommission(mkGetSingleSelection(dl)) | An Axiom |
| test-374 | ⊦ ¬ isOkPayCommission(mkGetMultipleSelection(dl)) | An Axiom |
| test-375 | ⊦ ¬ isOkPayCommission(mkGetInputTravelPlanner) | An Axiom |
| test-376 | ⊦ ¬ isOkPayCommission(mkGetInputTravelAgency) | An Axiom |
| test-377 | ⊦ ¬ isOkPayCommission(mkGetInputString) | An Axiom |
| test-378 | ⊦ ¬ isOkPayCommission(mkGetInputRequestData) | An Axiom |
| test-379 | ⊦ ¬ isOkPayCommission(mkGetInputInteger) | An Axiom |
| test-380 | ⊦ ¬ isOkPayCommission(mkGetInputIFlowUtil) | An Axiom |
| test-381 | ⊦ ¬ isOkPayCommission(mkGetInputGPSPos) | An Axiom |
| test-382 | ⊦ ¬ isOkPayCommission(mkGetInputFlightOffer) | An Axiom |
| test-383 | ⊦ ¬ isOkPayCommission(mkGetInputData) | An Axiom |
| test-384 | ⊦ ¬ isOkPayCommission(mkGetInputCreditCardDetails) | An Axiom |
| test-385 | ⊦ ¬ isOkPayCommission(mkGetInputCreditCardCenter) | An Axiom |
| test-386 | ⊦ ¬ isOkPayCommission(mkGetInputBoolean) | An Axiom |
| test-387 | ⊦ ¬ isOkPayCommission(mkGetInputAirline) | An Axiom |
| test-388 | ⊦ ¬ isOkPayCommission(mkGetInputAgent) | An Axiom |
| test-389 | ⊦ ¬ isOkPayCommission(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-390 | ⊦ ¬ isOkPayCommission(mkGetDeclassifiedCCD) | An Axiom |
| test-391 | ⊦ ¬ isOkPayCommission(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-392 | ⊦ ¬ isOkPayCommission(mkConfirmRelease(d, a_String)) | An Axiom |
| test-393 | ⊦ ¬ isOkPayCommission(mkConfirmBooking(a_Integer)) | An Axiom |
| test-394 | ⊦ ¬ isOkPayCommission(mkConfirm) | An Axiom |
| test-395 | ⊦ ¬ isOkPayCommission(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-396 | ⊦ ¬ isOkPayCommission(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-397 | ⊦ ¬ isOkConfirmBooking(mkStart) | An Axiom |
| test-398 | ⊦ ¬ isOkConfirmBooking(mkShow(d)) | An Axiom |
| test-399 | ⊦ ¬ isOkConfirmBooking(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-400 | ⊦ ¬ isOkConfirmBooking(mkReleaseCCD(a_String)) | An Axiom |
| test-401 | ⊦ ¬ isOkConfirmBooking(mkPayCommission) | An Axiom |
| test-402 | ⊦ ¬ isOkConfirmBooking(mkOkPayCommission) | An Axiom |
| test-403 | ⊦ isOkConfirmBooking(mkOkConfirmBooking) | An Axiom |
| test-404 | ⊦ ¬ isOkConfirmBooking(mkGetSingleSelection(dl)) | An Axiom |
| test-405 | ⊦ ¬ isOkConfirmBooking(mkGetMultipleSelection(dl)) | An Axiom |
| test-406 | ⊦ ¬ isOkConfirmBooking(mkGetInputTravelPlanner) | An Axiom |
| test-407 | ⊦ ¬ isOkConfirmBooking(mkGetInputTravelAgency) | An Axiom |
| test-408 | ⊦ ¬ isOkConfirmBooking(mkGetInputString) | An Axiom |
| test-409 | ⊦ ¬ isOkConfirmBooking(mkGetInputRequestData) | An Axiom |
| test-410 | ⊦ ¬ isOkConfirmBooking(mkGetInputInteger) | An Axiom |
| test-411 | ⊦ ¬ isOkConfirmBooking(mkGetInputIFlowUtil) | An Axiom |
| test-412 | ⊦ ¬ isOkConfirmBooking(mkGetInputGPSPos) | An Axiom |
| test-413 | ⊦ ¬ isOkConfirmBooking(mkGetInputFlightOffer) | An Axiom |
| test-414 | ⊦ ¬ isOkConfirmBooking(mkGetInputData) | An Axiom |
| test-415 | ⊦ ¬ isOkConfirmBooking(mkGetInputCreditCardDetails) | An Axiom |
| test-416 | ⊦ ¬ isOkConfirmBooking(mkGetInputCreditCardCenter) | An Axiom |
| test-417 | ⊦ ¬ isOkConfirmBooking(mkGetInputBoolean) | An Axiom |
| test-418 | ⊦ ¬ isOkConfirmBooking(mkGetInputAirline) | An Axiom |
| test-419 | ⊦ ¬ isOkConfirmBooking(mkGetInputAgent) | An Axiom |
| test-420 | ⊦ ¬ isOkConfirmBooking(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-421 | ⊦ ¬ isOkConfirmBooking(mkGetDeclassifiedCCD) | An Axiom |
| test-422 | ⊦ ¬ isOkConfirmBooking(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-423 | ⊦ ¬ isOkConfirmBooking(mkConfirmRelease(d, a_String)) | An Axiom |
| test-424 | ⊦ ¬ isOkConfirmBooking(mkConfirmBooking(a_Integer)) | An Axiom |
| test-425 | ⊦ ¬ isOkConfirmBooking(mkConfirm) | An Axiom |
| test-426 | ⊦ ¬ isOkConfirmBooking(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-427 | ⊦ ¬ isOkConfirmBooking(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-428 | ⊦ ¬ isGetSingleSelection(mkStart) | An Axiom |
| test-429 | ⊦ ¬ isGetSingleSelection(mkShow(d)) | An Axiom |
| test-430 | ⊦ ¬ isGetSingleSelection(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-431 | ⊦ ¬ isGetSingleSelection(mkReleaseCCD(a_String)) | An Axiom |
| test-432 | ⊦ ¬ isGetSingleSelection(mkPayCommission) | An Axiom |
| test-433 | ⊦ ¬ isGetSingleSelection(mkOkPayCommission) | An Axiom |
| test-434 | ⊦ ¬ isGetSingleSelection(mkOkConfirmBooking) | An Axiom |
| test-435 | ⊦ isGetSingleSelection(mkGetSingleSelection(dl)) | An Axiom |
| test-436 | ⊦ ¬ isGetSingleSelection(mkGetMultipleSelection(dl)) | An Axiom |
| test-437 | ⊦ ¬ isGetSingleSelection(mkGetInputTravelPlanner) | An Axiom |
| test-438 | ⊦ ¬ isGetSingleSelection(mkGetInputTravelAgency) | An Axiom |
| test-439 | ⊦ ¬ isGetSingleSelection(mkGetInputString) | An Axiom |
| test-440 | ⊦ ¬ isGetSingleSelection(mkGetInputRequestData) | An Axiom |
| test-441 | ⊦ ¬ isGetSingleSelection(mkGetInputInteger) | An Axiom |
| test-442 | ⊦ ¬ isGetSingleSelection(mkGetInputIFlowUtil) | An Axiom |
| test-443 | ⊦ ¬ isGetSingleSelection(mkGetInputGPSPos) | An Axiom |
| test-444 | ⊦ ¬ isGetSingleSelection(mkGetInputFlightOffer) | An Axiom |
| test-445 | ⊦ ¬ isGetSingleSelection(mkGetInputData) | An Axiom |
| test-446 | ⊦ ¬ isGetSingleSelection(mkGetInputCreditCardDetails) | An Axiom |
| test-447 | ⊦ ¬ isGetSingleSelection(mkGetInputCreditCardCenter) | An Axiom |
| test-448 | ⊦ ¬ isGetSingleSelection(mkGetInputBoolean) | An Axiom |
| test-449 | ⊦ ¬ isGetSingleSelection(mkGetInputAirline) | An Axiom |
| test-450 | ⊦ ¬ isGetSingleSelection(mkGetInputAgent) | An Axiom |
| test-451 | ⊦ ¬ isGetSingleSelection(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-452 | ⊦ ¬ isGetSingleSelection(mkGetDeclassifiedCCD) | An Axiom |
| test-453 | ⊦ ¬ isGetSingleSelection(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-454 | ⊦ ¬ isGetSingleSelection(mkConfirmRelease(d, a_String)) | An Axiom |
| test-455 | ⊦ ¬ isGetSingleSelection(mkConfirmBooking(a_Integer)) | An Axiom |
| test-456 | ⊦ ¬ isGetSingleSelection(mkConfirm) | An Axiom |
| test-457 | ⊦ ¬ isGetSingleSelection(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-458 | ⊦ ¬ isGetSingleSelection(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-459 | ⊦ ¬ isGetMultipleSelection(mkStart) | An Axiom |
| test-460 | ⊦ ¬ isGetMultipleSelection(mkShow(d)) | An Axiom |
| test-461 | ⊦ ¬ isGetMultipleSelection(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-462 | ⊦ ¬ isGetMultipleSelection(mkReleaseCCD(a_String)) | An Axiom |
| test-463 | ⊦ ¬ isGetMultipleSelection(mkPayCommission) | An Axiom |
| test-464 | ⊦ ¬ isGetMultipleSelection(mkOkPayCommission) | An Axiom |
| test-465 | ⊦ ¬ isGetMultipleSelection(mkOkConfirmBooking) | An Axiom |
| test-466 | ⊦ ¬ isGetMultipleSelection(mkGetSingleSelection(dl)) | An Axiom |
| test-467 | ⊦ isGetMultipleSelection(mkGetMultipleSelection(dl)) | An Axiom |
| test-468 | ⊦ ¬ isGetMultipleSelection(mkGetInputTravelPlanner) | An Axiom |
| test-469 | ⊦ ¬ isGetMultipleSelection(mkGetInputTravelAgency) | An Axiom |
| test-470 | ⊦ ¬ isGetMultipleSelection(mkGetInputString) | An Axiom |
| test-471 | ⊦ ¬ isGetMultipleSelection(mkGetInputRequestData) | An Axiom |
| test-472 | ⊦ ¬ isGetMultipleSelection(mkGetInputInteger) | An Axiom |
| test-473 | ⊦ ¬ isGetMultipleSelection(mkGetInputIFlowUtil) | An Axiom |
| test-474 | ⊦ ¬ isGetMultipleSelection(mkGetInputGPSPos) | An Axiom |
| test-475 | ⊦ ¬ isGetMultipleSelection(mkGetInputFlightOffer) | An Axiom |
| test-476 | ⊦ ¬ isGetMultipleSelection(mkGetInputData) | An Axiom |
| test-477 | ⊦ ¬ isGetMultipleSelection(mkGetInputCreditCardDetails) | An Axiom |
| test-478 | ⊦ ¬ isGetMultipleSelection(mkGetInputCreditCardCenter) | An Axiom |
| test-479 | ⊦ ¬ isGetMultipleSelection(mkGetInputBoolean) | An Axiom |
| test-480 | ⊦ ¬ isGetMultipleSelection(mkGetInputAirline) | An Axiom |
| test-481 | ⊦ ¬ isGetMultipleSelection(mkGetInputAgent) | An Axiom |
| test-482 | ⊦ ¬ isGetMultipleSelection(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-483 | ⊦ ¬ isGetMultipleSelection(mkGetDeclassifiedCCD) | An Axiom |
| test-484 | ⊦ ¬ isGetMultipleSelection(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-485 | ⊦ ¬ isGetMultipleSelection(mkConfirmRelease(d, a_String)) | An Axiom |
| test-486 | ⊦ ¬ isGetMultipleSelection(mkConfirmBooking(a_Integer)) | An Axiom |
| test-487 | ⊦ ¬ isGetMultipleSelection(mkConfirm) | An Axiom |
| test-488 | ⊦ ¬ isGetMultipleSelection(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-489 | ⊦ ¬ isGetMultipleSelection(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-490 | ⊦ ¬ isGetInputTravelPlanner(mkStart) | An Axiom |
| test-491 | ⊦ ¬ isGetInputTravelPlanner(mkShow(d)) | An Axiom |
| test-492 | ⊦ ¬ isGetInputTravelPlanner(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-493 | ⊦ ¬ isGetInputTravelPlanner(mkReleaseCCD(a_String)) | An Axiom |
| test-494 | ⊦ ¬ isGetInputTravelPlanner(mkPayCommission) | An Axiom |
| test-495 | ⊦ ¬ isGetInputTravelPlanner(mkOkPayCommission) | An Axiom |
| test-496 | ⊦ ¬ isGetInputTravelPlanner(mkOkConfirmBooking) | An Axiom |
| test-497 | ⊦ ¬ isGetInputTravelPlanner(mkGetSingleSelection(dl)) | An Axiom |
| test-498 | ⊦ ¬ isGetInputTravelPlanner(mkGetMultipleSelection(dl)) | An Axiom |
| test-499 | ⊦ isGetInputTravelPlanner(mkGetInputTravelPlanner) | An Axiom |
| test-500 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputTravelAgency) | An Axiom |
| test-501 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputString) | An Axiom |
| test-502 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputRequestData) | An Axiom |
| test-503 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputInteger) | An Axiom |
| test-504 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputIFlowUtil) | An Axiom |
| test-505 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputGPSPos) | An Axiom |
| test-506 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputFlightOffer) | An Axiom |
| test-507 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputData) | An Axiom |
| test-508 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputCreditCardDetails) | An Axiom |
| test-509 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputCreditCardCenter) | An Axiom |
| test-510 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputBoolean) | An Axiom |
| test-511 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputAirline) | An Axiom |
| test-512 | ⊦ ¬ isGetInputTravelPlanner(mkGetInputAgent) | An Axiom |
| test-513 | ⊦ ¬ isGetInputTravelPlanner(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-514 | ⊦ ¬ isGetInputTravelPlanner(mkGetDeclassifiedCCD) | An Axiom |
| test-515 | ⊦ ¬ isGetInputTravelPlanner(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-516 | ⊦ ¬ isGetInputTravelPlanner(mkConfirmRelease(d, a_String)) | An Axiom |
| test-517 | ⊦ ¬ isGetInputTravelPlanner(mkConfirmBooking(a_Integer)) | An Axiom |
| test-518 | ⊦ ¬ isGetInputTravelPlanner(mkConfirm) | An Axiom |
| test-519 | ⊦ ¬ isGetInputTravelPlanner(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-520 | ⊦ ¬ isGetInputTravelPlanner(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-521 | ⊦ ¬ isGetInputTravelAgency(mkStart) | An Axiom |
| test-522 | ⊦ ¬ isGetInputTravelAgency(mkShow(d)) | An Axiom |
| test-523 | ⊦ ¬ isGetInputTravelAgency(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-524 | ⊦ ¬ isGetInputTravelAgency(mkReleaseCCD(a_String)) | An Axiom |
| test-525 | ⊦ ¬ isGetInputTravelAgency(mkPayCommission) | An Axiom |
| test-526 | ⊦ ¬ isGetInputTravelAgency(mkOkPayCommission) | An Axiom |
| test-527 | ⊦ ¬ isGetInputTravelAgency(mkOkConfirmBooking) | An Axiom |
| test-528 | ⊦ ¬ isGetInputTravelAgency(mkGetSingleSelection(dl)) | An Axiom |
| test-529 | ⊦ ¬ isGetInputTravelAgency(mkGetMultipleSelection(dl)) | An Axiom |
| test-530 | ⊦ ¬ isGetInputTravelAgency(mkGetInputTravelPlanner) | An Axiom |
| test-531 | ⊦ isGetInputTravelAgency(mkGetInputTravelAgency) | An Axiom |
| test-532 | ⊦ ¬ isGetInputTravelAgency(mkGetInputString) | An Axiom |
| test-533 | ⊦ ¬ isGetInputTravelAgency(mkGetInputRequestData) | An Axiom |
| test-534 | ⊦ ¬ isGetInputTravelAgency(mkGetInputInteger) | An Axiom |
| test-535 | ⊦ ¬ isGetInputTravelAgency(mkGetInputIFlowUtil) | An Axiom |
| test-536 | ⊦ ¬ isGetInputTravelAgency(mkGetInputGPSPos) | An Axiom |
| test-537 | ⊦ ¬ isGetInputTravelAgency(mkGetInputFlightOffer) | An Axiom |
| test-538 | ⊦ ¬ isGetInputTravelAgency(mkGetInputData) | An Axiom |
| test-539 | ⊦ ¬ isGetInputTravelAgency(mkGetInputCreditCardDetails) | An Axiom |
| test-540 | ⊦ ¬ isGetInputTravelAgency(mkGetInputCreditCardCenter) | An Axiom |
| test-541 | ⊦ ¬ isGetInputTravelAgency(mkGetInputBoolean) | An Axiom |
| test-542 | ⊦ ¬ isGetInputTravelAgency(mkGetInputAirline) | An Axiom |
| test-543 | ⊦ ¬ isGetInputTravelAgency(mkGetInputAgent) | An Axiom |
| test-544 | ⊦ ¬ isGetInputTravelAgency(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-545 | ⊦ ¬ isGetInputTravelAgency(mkGetDeclassifiedCCD) | An Axiom |
| test-546 | ⊦ ¬ isGetInputTravelAgency(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-547 | ⊦ ¬ isGetInputTravelAgency(mkConfirmRelease(d, a_String)) | An Axiom |
| test-548 | ⊦ ¬ isGetInputTravelAgency(mkConfirmBooking(a_Integer)) | An Axiom |
| test-549 | ⊦ ¬ isGetInputTravelAgency(mkConfirm) | An Axiom |
| test-550 | ⊦ ¬ isGetInputTravelAgency(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-551 | ⊦ ¬ isGetInputTravelAgency(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-552 | ⊦ ¬ isGetInputString(mkStart) | An Axiom |
| test-553 | ⊦ ¬ isGetInputString(mkShow(d)) | An Axiom |
| test-554 | ⊦ ¬ isGetInputString(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-555 | ⊦ ¬ isGetInputString(mkReleaseCCD(a_String)) | An Axiom |
| test-556 | ⊦ ¬ isGetInputString(mkPayCommission) | An Axiom |
| test-557 | ⊦ ¬ isGetInputString(mkOkPayCommission) | An Axiom |
| test-558 | ⊦ ¬ isGetInputString(mkOkConfirmBooking) | An Axiom |
| test-559 | ⊦ ¬ isGetInputString(mkGetSingleSelection(dl)) | An Axiom |
| test-560 | ⊦ ¬ isGetInputString(mkGetMultipleSelection(dl)) | An Axiom |
| test-561 | ⊦ ¬ isGetInputString(mkGetInputTravelPlanner) | An Axiom |
| test-562 | ⊦ ¬ isGetInputString(mkGetInputTravelAgency) | An Axiom |
| test-563 | ⊦ isGetInputString(mkGetInputString) | An Axiom |
| test-564 | ⊦ ¬ isGetInputString(mkGetInputRequestData) | An Axiom |
| test-565 | ⊦ ¬ isGetInputString(mkGetInputInteger) | An Axiom |
| test-566 | ⊦ ¬ isGetInputString(mkGetInputIFlowUtil) | An Axiom |
| test-567 | ⊦ ¬ isGetInputString(mkGetInputGPSPos) | An Axiom |
| test-568 | ⊦ ¬ isGetInputString(mkGetInputFlightOffer) | An Axiom |
| test-569 | ⊦ ¬ isGetInputString(mkGetInputData) | An Axiom |
| test-570 | ⊦ ¬ isGetInputString(mkGetInputCreditCardDetails) | An Axiom |
| test-571 | ⊦ ¬ isGetInputString(mkGetInputCreditCardCenter) | An Axiom |
| test-572 | ⊦ ¬ isGetInputString(mkGetInputBoolean) | An Axiom |
| test-573 | ⊦ ¬ isGetInputString(mkGetInputAirline) | An Axiom |
| test-574 | ⊦ ¬ isGetInputString(mkGetInputAgent) | An Axiom |
| test-575 | ⊦ ¬ isGetInputString(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-576 | ⊦ ¬ isGetInputString(mkGetDeclassifiedCCD) | An Axiom |
| test-577 | ⊦ ¬ isGetInputString(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-578 | ⊦ ¬ isGetInputString(mkConfirmRelease(d, a_String)) | An Axiom |
| test-579 | ⊦ ¬ isGetInputString(mkConfirmBooking(a_Integer)) | An Axiom |
| test-580 | ⊦ ¬ isGetInputString(mkConfirm) | An Axiom |
| test-581 | ⊦ ¬ isGetInputString(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-582 | ⊦ ¬ isGetInputString(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-583 | ⊦ ¬ isGetInputRequestData(mkStart) | An Axiom |
| test-584 | ⊦ ¬ isGetInputRequestData(mkShow(d)) | An Axiom |
| test-585 | ⊦ ¬ isGetInputRequestData(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-586 | ⊦ ¬ isGetInputRequestData(mkReleaseCCD(a_String)) | An Axiom |
| test-587 | ⊦ ¬ isGetInputRequestData(mkPayCommission) | An Axiom |
| test-588 | ⊦ ¬ isGetInputRequestData(mkOkPayCommission) | An Axiom |
| test-589 | ⊦ ¬ isGetInputRequestData(mkOkConfirmBooking) | An Axiom |
| test-590 | ⊦ ¬ isGetInputRequestData(mkGetSingleSelection(dl)) | An Axiom |
| test-591 | ⊦ ¬ isGetInputRequestData(mkGetMultipleSelection(dl)) | An Axiom |
| test-592 | ⊦ ¬ isGetInputRequestData(mkGetInputTravelPlanner) | An Axiom |
| test-593 | ⊦ ¬ isGetInputRequestData(mkGetInputTravelAgency) | An Axiom |
| test-594 | ⊦ ¬ isGetInputRequestData(mkGetInputString) | An Axiom |
| test-595 | ⊦ isGetInputRequestData(mkGetInputRequestData) | An Axiom |
| test-596 | ⊦ ¬ isGetInputRequestData(mkGetInputInteger) | An Axiom |
| test-597 | ⊦ ¬ isGetInputRequestData(mkGetInputIFlowUtil) | An Axiom |
| test-598 | ⊦ ¬ isGetInputRequestData(mkGetInputGPSPos) | An Axiom |
| test-599 | ⊦ ¬ isGetInputRequestData(mkGetInputFlightOffer) | An Axiom |
| test-600 | ⊦ ¬ isGetInputRequestData(mkGetInputData) | An Axiom |
| test-601 | ⊦ ¬ isGetInputRequestData(mkGetInputCreditCardDetails) | An Axiom |
| test-602 | ⊦ ¬ isGetInputRequestData(mkGetInputCreditCardCenter) | An Axiom |
| test-603 | ⊦ ¬ isGetInputRequestData(mkGetInputBoolean) | An Axiom |
| test-604 | ⊦ ¬ isGetInputRequestData(mkGetInputAirline) | An Axiom |
| test-605 | ⊦ ¬ isGetInputRequestData(mkGetInputAgent) | An Axiom |
| test-606 | ⊦ ¬ isGetInputRequestData(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-607 | ⊦ ¬ isGetInputRequestData(mkGetDeclassifiedCCD) | An Axiom |
| test-608 | ⊦ ¬ isGetInputRequestData(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-609 | ⊦ ¬ isGetInputRequestData(mkConfirmRelease(d, a_String)) | An Axiom |
| test-610 | ⊦ ¬ isGetInputRequestData(mkConfirmBooking(a_Integer)) | An Axiom |
| test-611 | ⊦ ¬ isGetInputRequestData(mkConfirm) | An Axiom |
| test-612 | ⊦ ¬ isGetInputRequestData(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-613 | ⊦ ¬ isGetInputRequestData(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-614 | ⊦ ¬ isGetInputInteger(mkStart) | An Axiom |
| test-615 | ⊦ ¬ isGetInputInteger(mkShow(d)) | An Axiom |
| test-616 | ⊦ ¬ isGetInputInteger(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-617 | ⊦ ¬ isGetInputInteger(mkReleaseCCD(a_String)) | An Axiom |
| test-618 | ⊦ ¬ isGetInputInteger(mkPayCommission) | An Axiom |
| test-619 | ⊦ ¬ isGetInputInteger(mkOkPayCommission) | An Axiom |
| test-620 | ⊦ ¬ isGetInputInteger(mkOkConfirmBooking) | An Axiom |
| test-621 | ⊦ ¬ isGetInputInteger(mkGetSingleSelection(dl)) | An Axiom |
| test-622 | ⊦ ¬ isGetInputInteger(mkGetMultipleSelection(dl)) | An Axiom |
| test-623 | ⊦ ¬ isGetInputInteger(mkGetInputTravelPlanner) | An Axiom |
| test-624 | ⊦ ¬ isGetInputInteger(mkGetInputTravelAgency) | An Axiom |
| test-625 | ⊦ ¬ isGetInputInteger(mkGetInputString) | An Axiom |
| test-626 | ⊦ ¬ isGetInputInteger(mkGetInputRequestData) | An Axiom |
| test-627 | ⊦ isGetInputInteger(mkGetInputInteger) | An Axiom |
| test-628 | ⊦ ¬ isGetInputInteger(mkGetInputIFlowUtil) | An Axiom |
| test-629 | ⊦ ¬ isGetInputInteger(mkGetInputGPSPos) | An Axiom |
| test-630 | ⊦ ¬ isGetInputInteger(mkGetInputFlightOffer) | An Axiom |
| test-631 | ⊦ ¬ isGetInputInteger(mkGetInputData) | An Axiom |
| test-632 | ⊦ ¬ isGetInputInteger(mkGetInputCreditCardDetails) | An Axiom |
| test-633 | ⊦ ¬ isGetInputInteger(mkGetInputCreditCardCenter) | An Axiom |
| test-634 | ⊦ ¬ isGetInputInteger(mkGetInputBoolean) | An Axiom |
| test-635 | ⊦ ¬ isGetInputInteger(mkGetInputAirline) | An Axiom |
| test-636 | ⊦ ¬ isGetInputInteger(mkGetInputAgent) | An Axiom |
| test-637 | ⊦ ¬ isGetInputInteger(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-638 | ⊦ ¬ isGetInputInteger(mkGetDeclassifiedCCD) | An Axiom |
| test-639 | ⊦ ¬ isGetInputInteger(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-640 | ⊦ ¬ isGetInputInteger(mkConfirmRelease(d, a_String)) | An Axiom |
| test-641 | ⊦ ¬ isGetInputInteger(mkConfirmBooking(a_Integer)) | An Axiom |
| test-642 | ⊦ ¬ isGetInputInteger(mkConfirm) | An Axiom |
| test-643 | ⊦ ¬ isGetInputInteger(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-644 | ⊦ ¬ isGetInputInteger(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-645 | ⊦ ¬ isGetInputIFlowUtil(mkStart) | An Axiom |
| test-646 | ⊦ ¬ isGetInputIFlowUtil(mkShow(d)) | An Axiom |
| test-647 | ⊦ ¬ isGetInputIFlowUtil(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-648 | ⊦ ¬ isGetInputIFlowUtil(mkReleaseCCD(a_String)) | An Axiom |
| test-649 | ⊦ ¬ isGetInputIFlowUtil(mkPayCommission) | An Axiom |
| test-650 | ⊦ ¬ isGetInputIFlowUtil(mkOkPayCommission) | An Axiom |
| test-651 | ⊦ ¬ isGetInputIFlowUtil(mkOkConfirmBooking) | An Axiom |
| test-652 | ⊦ ¬ isGetInputIFlowUtil(mkGetSingleSelection(dl)) | An Axiom |
| test-653 | ⊦ ¬ isGetInputIFlowUtil(mkGetMultipleSelection(dl)) | An Axiom |
| test-654 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputTravelPlanner) | An Axiom |
| test-655 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputTravelAgency) | An Axiom |
| test-656 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputString) | An Axiom |
| test-657 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputRequestData) | An Axiom |
| test-658 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputInteger) | An Axiom |
| test-659 | ⊦ isGetInputIFlowUtil(mkGetInputIFlowUtil) | An Axiom |
| test-660 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputGPSPos) | An Axiom |
| test-661 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputFlightOffer) | An Axiom |
| test-662 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputData) | An Axiom |
| test-663 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputCreditCardDetails) | An Axiom |
| test-664 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputCreditCardCenter) | An Axiom |
| test-665 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputBoolean) | An Axiom |
| test-666 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputAirline) | An Axiom |
| test-667 | ⊦ ¬ isGetInputIFlowUtil(mkGetInputAgent) | An Axiom |
| test-668 | ⊦ ¬ isGetInputIFlowUtil(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-669 | ⊦ ¬ isGetInputIFlowUtil(mkGetDeclassifiedCCD) | An Axiom |
| test-670 | ⊦ ¬ isGetInputIFlowUtil(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-671 | ⊦ ¬ isGetInputIFlowUtil(mkConfirmRelease(d, a_String)) | An Axiom |
| test-672 | ⊦ ¬ isGetInputIFlowUtil(mkConfirmBooking(a_Integer)) | An Axiom |
| test-673 | ⊦ ¬ isGetInputIFlowUtil(mkConfirm) | An Axiom |
| test-674 | ⊦ ¬ isGetInputIFlowUtil(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-675 | ⊦ ¬ isGetInputIFlowUtil(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-676 | ⊦ ¬ isGetInputGPSPos(mkStart) | An Axiom |
| test-677 | ⊦ ¬ isGetInputGPSPos(mkShow(d)) | An Axiom |
| test-678 | ⊦ ¬ isGetInputGPSPos(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-679 | ⊦ ¬ isGetInputGPSPos(mkReleaseCCD(a_String)) | An Axiom |
| test-680 | ⊦ ¬ isGetInputGPSPos(mkPayCommission) | An Axiom |
| test-681 | ⊦ ¬ isGetInputGPSPos(mkOkPayCommission) | An Axiom |
| test-682 | ⊦ ¬ isGetInputGPSPos(mkOkConfirmBooking) | An Axiom |
| test-683 | ⊦ ¬ isGetInputGPSPos(mkGetSingleSelection(dl)) | An Axiom |
| test-684 | ⊦ ¬ isGetInputGPSPos(mkGetMultipleSelection(dl)) | An Axiom |
| test-685 | ⊦ ¬ isGetInputGPSPos(mkGetInputTravelPlanner) | An Axiom |
| test-686 | ⊦ ¬ isGetInputGPSPos(mkGetInputTravelAgency) | An Axiom |
| test-687 | ⊦ ¬ isGetInputGPSPos(mkGetInputString) | An Axiom |
| test-688 | ⊦ ¬ isGetInputGPSPos(mkGetInputRequestData) | An Axiom |
| test-689 | ⊦ ¬ isGetInputGPSPos(mkGetInputInteger) | An Axiom |
| test-690 | ⊦ ¬ isGetInputGPSPos(mkGetInputIFlowUtil) | An Axiom |
| test-691 | ⊦ isGetInputGPSPos(mkGetInputGPSPos) | An Axiom |
| test-692 | ⊦ ¬ isGetInputGPSPos(mkGetInputFlightOffer) | An Axiom |
| test-693 | ⊦ ¬ isGetInputGPSPos(mkGetInputData) | An Axiom |
| test-694 | ⊦ ¬ isGetInputGPSPos(mkGetInputCreditCardDetails) | An Axiom |
| test-695 | ⊦ ¬ isGetInputGPSPos(mkGetInputCreditCardCenter) | An Axiom |
| test-696 | ⊦ ¬ isGetInputGPSPos(mkGetInputBoolean) | An Axiom |
| test-697 | ⊦ ¬ isGetInputGPSPos(mkGetInputAirline) | An Axiom |
| test-698 | ⊦ ¬ isGetInputGPSPos(mkGetInputAgent) | An Axiom |
| test-699 | ⊦ ¬ isGetInputGPSPos(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-700 | ⊦ ¬ isGetInputGPSPos(mkGetDeclassifiedCCD) | An Axiom |
| test-701 | ⊦ ¬ isGetInputGPSPos(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-702 | ⊦ ¬ isGetInputGPSPos(mkConfirmRelease(d, a_String)) | An Axiom |
| test-703 | ⊦ ¬ isGetInputGPSPos(mkConfirmBooking(a_Integer)) | An Axiom |
| test-704 | ⊦ ¬ isGetInputGPSPos(mkConfirm) | An Axiom |
| test-705 | ⊦ ¬ isGetInputGPSPos(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-706 | ⊦ ¬ isGetInputGPSPos(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-707 | ⊦ ¬ isGetInputFlightOffer(mkStart) | An Axiom |
| test-708 | ⊦ ¬ isGetInputFlightOffer(mkShow(d)) | An Axiom |
| test-709 | ⊦ ¬ isGetInputFlightOffer(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-710 | ⊦ ¬ isGetInputFlightOffer(mkReleaseCCD(a_String)) | An Axiom |
| test-711 | ⊦ ¬ isGetInputFlightOffer(mkPayCommission) | An Axiom |
| test-712 | ⊦ ¬ isGetInputFlightOffer(mkOkPayCommission) | An Axiom |
| test-713 | ⊦ ¬ isGetInputFlightOffer(mkOkConfirmBooking) | An Axiom |
| test-714 | ⊦ ¬ isGetInputFlightOffer(mkGetSingleSelection(dl)) | An Axiom |
| test-715 | ⊦ ¬ isGetInputFlightOffer(mkGetMultipleSelection(dl)) | An Axiom |
| test-716 | ⊦ ¬ isGetInputFlightOffer(mkGetInputTravelPlanner) | An Axiom |
| test-717 | ⊦ ¬ isGetInputFlightOffer(mkGetInputTravelAgency) | An Axiom |
| test-718 | ⊦ ¬ isGetInputFlightOffer(mkGetInputString) | An Axiom |
| test-719 | ⊦ ¬ isGetInputFlightOffer(mkGetInputRequestData) | An Axiom |
| test-720 | ⊦ ¬ isGetInputFlightOffer(mkGetInputInteger) | An Axiom |
| test-721 | ⊦ ¬ isGetInputFlightOffer(mkGetInputIFlowUtil) | An Axiom |
| test-722 | ⊦ ¬ isGetInputFlightOffer(mkGetInputGPSPos) | An Axiom |
| test-723 | ⊦ isGetInputFlightOffer(mkGetInputFlightOffer) | An Axiom |
| test-724 | ⊦ ¬ isGetInputFlightOffer(mkGetInputData) | An Axiom |
| test-725 | ⊦ ¬ isGetInputFlightOffer(mkGetInputCreditCardDetails) | An Axiom |
| test-726 | ⊦ ¬ isGetInputFlightOffer(mkGetInputCreditCardCenter) | An Axiom |
| test-727 | ⊦ ¬ isGetInputFlightOffer(mkGetInputBoolean) | An Axiom |
| test-728 | ⊦ ¬ isGetInputFlightOffer(mkGetInputAirline) | An Axiom |
| test-729 | ⊦ ¬ isGetInputFlightOffer(mkGetInputAgent) | An Axiom |
| test-730 | ⊦ ¬ isGetInputFlightOffer(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-731 | ⊦ ¬ isGetInputFlightOffer(mkGetDeclassifiedCCD) | An Axiom |
| test-732 | ⊦ ¬ isGetInputFlightOffer(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-733 | ⊦ ¬ isGetInputFlightOffer(mkConfirmRelease(d, a_String)) | An Axiom |
| test-734 | ⊦ ¬ isGetInputFlightOffer(mkConfirmBooking(a_Integer)) | An Axiom |
| test-735 | ⊦ ¬ isGetInputFlightOffer(mkConfirm) | An Axiom |
| test-736 | ⊦ ¬ isGetInputFlightOffer(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-737 | ⊦ ¬ isGetInputFlightOffer(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-738 | ⊦ ¬ isGetInputData(mkStart) | An Axiom |
| test-739 | ⊦ ¬ isGetInputData(mkShow(d)) | An Axiom |
| test-740 | ⊦ ¬ isGetInputData(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-741 | ⊦ ¬ isGetInputData(mkReleaseCCD(a_String)) | An Axiom |
| test-742 | ⊦ ¬ isGetInputData(mkPayCommission) | An Axiom |
| test-743 | ⊦ ¬ isGetInputData(mkOkPayCommission) | An Axiom |
| test-744 | ⊦ ¬ isGetInputData(mkOkConfirmBooking) | An Axiom |
| test-745 | ⊦ ¬ isGetInputData(mkGetSingleSelection(dl)) | An Axiom |
| test-746 | ⊦ ¬ isGetInputData(mkGetMultipleSelection(dl)) | An Axiom |
| test-747 | ⊦ ¬ isGetInputData(mkGetInputTravelPlanner) | An Axiom |
| test-748 | ⊦ ¬ isGetInputData(mkGetInputTravelAgency) | An Axiom |
| test-749 | ⊦ ¬ isGetInputData(mkGetInputString) | An Axiom |
| test-750 | ⊦ ¬ isGetInputData(mkGetInputRequestData) | An Axiom |
| test-751 | ⊦ ¬ isGetInputData(mkGetInputInteger) | An Axiom |
| test-752 | ⊦ ¬ isGetInputData(mkGetInputIFlowUtil) | An Axiom |
| test-753 | ⊦ ¬ isGetInputData(mkGetInputGPSPos) | An Axiom |
| test-754 | ⊦ ¬ isGetInputData(mkGetInputFlightOffer) | An Axiom |
| test-755 | ⊦ isGetInputData(mkGetInputData) | An Axiom |
| test-756 | ⊦ ¬ isGetInputData(mkGetInputCreditCardDetails) | An Axiom |
| test-757 | ⊦ ¬ isGetInputData(mkGetInputCreditCardCenter) | An Axiom |
| test-758 | ⊦ ¬ isGetInputData(mkGetInputBoolean) | An Axiom |
| test-759 | ⊦ ¬ isGetInputData(mkGetInputAirline) | An Axiom |
| test-760 | ⊦ ¬ isGetInputData(mkGetInputAgent) | An Axiom |
| test-761 | ⊦ ¬ isGetInputData(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-762 | ⊦ ¬ isGetInputData(mkGetDeclassifiedCCD) | An Axiom |
| test-763 | ⊦ ¬ isGetInputData(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-764 | ⊦ ¬ isGetInputData(mkConfirmRelease(d, a_String)) | An Axiom |
| test-765 | ⊦ ¬ isGetInputData(mkConfirmBooking(a_Integer)) | An Axiom |
| test-766 | ⊦ ¬ isGetInputData(mkConfirm) | An Axiom |
| test-767 | ⊦ ¬ isGetInputData(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-768 | ⊦ ¬ isGetInputData(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-769 | ⊦ ¬ isGetInputCreditCardDetails(mkStart) | An Axiom |
| test-770 | ⊦ ¬ isGetInputCreditCardDetails(mkShow(d)) | An Axiom |
| test-771 | ⊦ ¬ isGetInputCreditCardDetails(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-772 | ⊦ ¬ isGetInputCreditCardDetails(mkReleaseCCD(a_String)) | An Axiom |
| test-773 | ⊦ ¬ isGetInputCreditCardDetails(mkPayCommission) | An Axiom |
| test-774 | ⊦ ¬ isGetInputCreditCardDetails(mkOkPayCommission) | An Axiom |
| test-775 | ⊦ ¬ isGetInputCreditCardDetails(mkOkConfirmBooking) | An Axiom |
| test-776 | ⊦ ¬ isGetInputCreditCardDetails(mkGetSingleSelection(dl)) | An Axiom |
| test-777 | ⊦ ¬ isGetInputCreditCardDetails(mkGetMultipleSelection(dl)) | An Axiom |
| test-778 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputTravelPlanner) | An Axiom |
| test-779 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputTravelAgency) | An Axiom |
| test-780 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputString) | An Axiom |
| test-781 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputRequestData) | An Axiom |
| test-782 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputInteger) | An Axiom |
| test-783 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputIFlowUtil) | An Axiom |
| test-784 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputGPSPos) | An Axiom |
| test-785 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputFlightOffer) | An Axiom |
| test-786 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputData) | An Axiom |
| test-787 | ⊦ isGetInputCreditCardDetails(mkGetInputCreditCardDetails) | An Axiom |
| test-788 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputCreditCardCenter) | An Axiom |
| test-789 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputBoolean) | An Axiom |
| test-790 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputAirline) | An Axiom |
| test-791 | ⊦ ¬ isGetInputCreditCardDetails(mkGetInputAgent) | An Axiom |
| test-792 | ⊦ ¬ isGetInputCreditCardDetails(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-793 | ⊦ ¬ isGetInputCreditCardDetails(mkGetDeclassifiedCCD) | An Axiom |
| test-794 | ⊦ ¬ isGetInputCreditCardDetails(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-795 | ⊦ ¬ isGetInputCreditCardDetails(mkConfirmRelease(d, a_String)) | An Axiom |
| test-796 | ⊦ ¬ isGetInputCreditCardDetails(mkConfirmBooking(a_Integer)) | An Axiom |
| test-797 | ⊦ ¬ isGetInputCreditCardDetails(mkConfirm) | An Axiom |
| test-798 | ⊦ ¬ isGetInputCreditCardDetails(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-799 | ⊦ ¬ isGetInputCreditCardDetails(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-800 | ⊦ ¬ isGetInputCreditCardCenter(mkStart) | An Axiom |
| test-801 | ⊦ ¬ isGetInputCreditCardCenter(mkShow(d)) | An Axiom |
| test-802 | ⊦ ¬ isGetInputCreditCardCenter(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-803 | ⊦ ¬ isGetInputCreditCardCenter(mkReleaseCCD(a_String)) | An Axiom |
| test-804 | ⊦ ¬ isGetInputCreditCardCenter(mkPayCommission) | An Axiom |
| test-805 | ⊦ ¬ isGetInputCreditCardCenter(mkOkPayCommission) | An Axiom |
| test-806 | ⊦ ¬ isGetInputCreditCardCenter(mkOkConfirmBooking) | An Axiom |
| test-807 | ⊦ ¬ isGetInputCreditCardCenter(mkGetSingleSelection(dl)) | An Axiom |
| test-808 | ⊦ ¬ isGetInputCreditCardCenter(mkGetMultipleSelection(dl)) | An Axiom |
| test-809 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputTravelPlanner) | An Axiom |
| test-810 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputTravelAgency) | An Axiom |
| test-811 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputString) | An Axiom |
| test-812 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputRequestData) | An Axiom |
| test-813 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputInteger) | An Axiom |
| test-814 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputIFlowUtil) | An Axiom |
| test-815 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputGPSPos) | An Axiom |
| test-816 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputFlightOffer) | An Axiom |
| test-817 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputData) | An Axiom |
| test-818 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputCreditCardDetails) | An Axiom |
| test-819 | ⊦ isGetInputCreditCardCenter(mkGetInputCreditCardCenter) | An Axiom |
| test-820 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputBoolean) | An Axiom |
| test-821 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputAirline) | An Axiom |
| test-822 | ⊦ ¬ isGetInputCreditCardCenter(mkGetInputAgent) | An Axiom |
| test-823 | ⊦ ¬ isGetInputCreditCardCenter(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-824 | ⊦ ¬ isGetInputCreditCardCenter(mkGetDeclassifiedCCD) | An Axiom |
| test-825 | ⊦ ¬ isGetInputCreditCardCenter(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-826 | ⊦ ¬ isGetInputCreditCardCenter(mkConfirmRelease(d, a_String)) | An Axiom |
| test-827 | ⊦ ¬ isGetInputCreditCardCenter(mkConfirmBooking(a_Integer)) | An Axiom |
| test-828 | ⊦ ¬ isGetInputCreditCardCenter(mkConfirm) | An Axiom |
| test-829 | ⊦ ¬ isGetInputCreditCardCenter(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-830 | ⊦ ¬ isGetInputCreditCardCenter(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-831 | ⊦ ¬ isGetInputBoolean(mkStart) | An Axiom |
| test-832 | ⊦ ¬ isGetInputBoolean(mkShow(d)) | An Axiom |
| test-833 | ⊦ ¬ isGetInputBoolean(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-834 | ⊦ ¬ isGetInputBoolean(mkReleaseCCD(a_String)) | An Axiom |
| test-835 | ⊦ ¬ isGetInputBoolean(mkPayCommission) | An Axiom |
| test-836 | ⊦ ¬ isGetInputBoolean(mkOkPayCommission) | An Axiom |
| test-837 | ⊦ ¬ isGetInputBoolean(mkOkConfirmBooking) | An Axiom |
| test-838 | ⊦ ¬ isGetInputBoolean(mkGetSingleSelection(dl)) | An Axiom |
| test-839 | ⊦ ¬ isGetInputBoolean(mkGetMultipleSelection(dl)) | An Axiom |
| test-840 | ⊦ ¬ isGetInputBoolean(mkGetInputTravelPlanner) | An Axiom |
| test-841 | ⊦ ¬ isGetInputBoolean(mkGetInputTravelAgency) | An Axiom |
| test-842 | ⊦ ¬ isGetInputBoolean(mkGetInputString) | An Axiom |
| test-843 | ⊦ ¬ isGetInputBoolean(mkGetInputRequestData) | An Axiom |
| test-844 | ⊦ ¬ isGetInputBoolean(mkGetInputInteger) | An Axiom |
| test-845 | ⊦ ¬ isGetInputBoolean(mkGetInputIFlowUtil) | An Axiom |
| test-846 | ⊦ ¬ isGetInputBoolean(mkGetInputGPSPos) | An Axiom |
| test-847 | ⊦ ¬ isGetInputBoolean(mkGetInputFlightOffer) | An Axiom |
| test-848 | ⊦ ¬ isGetInputBoolean(mkGetInputData) | An Axiom |
| test-849 | ⊦ ¬ isGetInputBoolean(mkGetInputCreditCardDetails) | An Axiom |
| test-850 | ⊦ ¬ isGetInputBoolean(mkGetInputCreditCardCenter) | An Axiom |
| test-851 | ⊦ isGetInputBoolean(mkGetInputBoolean) | An Axiom |
| test-852 | ⊦ ¬ isGetInputBoolean(mkGetInputAirline) | An Axiom |
| test-853 | ⊦ ¬ isGetInputBoolean(mkGetInputAgent) | An Axiom |
| test-854 | ⊦ ¬ isGetInputBoolean(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-855 | ⊦ ¬ isGetInputBoolean(mkGetDeclassifiedCCD) | An Axiom |
| test-856 | ⊦ ¬ isGetInputBoolean(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-857 | ⊦ ¬ isGetInputBoolean(mkConfirmRelease(d, a_String)) | An Axiom |
| test-858 | ⊦ ¬ isGetInputBoolean(mkConfirmBooking(a_Integer)) | An Axiom |
| test-859 | ⊦ ¬ isGetInputBoolean(mkConfirm) | An Axiom |
| test-860 | ⊦ ¬ isGetInputBoolean(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-861 | ⊦ ¬ isGetInputBoolean(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-862 | ⊦ ¬ isGetInputAirline(mkStart) | An Axiom |
| test-863 | ⊦ ¬ isGetInputAirline(mkShow(d)) | An Axiom |
| test-864 | ⊦ ¬ isGetInputAirline(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-865 | ⊦ ¬ isGetInputAirline(mkReleaseCCD(a_String)) | An Axiom |
| test-866 | ⊦ ¬ isGetInputAirline(mkPayCommission) | An Axiom |
| test-867 | ⊦ ¬ isGetInputAirline(mkOkPayCommission) | An Axiom |
| test-868 | ⊦ ¬ isGetInputAirline(mkOkConfirmBooking) | An Axiom |
| test-869 | ⊦ ¬ isGetInputAirline(mkGetSingleSelection(dl)) | An Axiom |
| test-870 | ⊦ ¬ isGetInputAirline(mkGetMultipleSelection(dl)) | An Axiom |
| test-871 | ⊦ ¬ isGetInputAirline(mkGetInputTravelPlanner) | An Axiom |
| test-872 | ⊦ ¬ isGetInputAirline(mkGetInputTravelAgency) | An Axiom |
| test-873 | ⊦ ¬ isGetInputAirline(mkGetInputString) | An Axiom |
| test-874 | ⊦ ¬ isGetInputAirline(mkGetInputRequestData) | An Axiom |
| test-875 | ⊦ ¬ isGetInputAirline(mkGetInputInteger) | An Axiom |
| test-876 | ⊦ ¬ isGetInputAirline(mkGetInputIFlowUtil) | An Axiom |
| test-877 | ⊦ ¬ isGetInputAirline(mkGetInputGPSPos) | An Axiom |
| test-878 | ⊦ ¬ isGetInputAirline(mkGetInputFlightOffer) | An Axiom |
| test-879 | ⊦ ¬ isGetInputAirline(mkGetInputData) | An Axiom |
| test-880 | ⊦ ¬ isGetInputAirline(mkGetInputCreditCardDetails) | An Axiom |
| test-881 | ⊦ ¬ isGetInputAirline(mkGetInputCreditCardCenter) | An Axiom |
| test-882 | ⊦ ¬ isGetInputAirline(mkGetInputBoolean) | An Axiom |
| test-883 | ⊦ isGetInputAirline(mkGetInputAirline) | An Axiom |
| test-884 | ⊦ ¬ isGetInputAirline(mkGetInputAgent) | An Axiom |
| test-885 | ⊦ ¬ isGetInputAirline(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-886 | ⊦ ¬ isGetInputAirline(mkGetDeclassifiedCCD) | An Axiom |
| test-887 | ⊦ ¬ isGetInputAirline(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-888 | ⊦ ¬ isGetInputAirline(mkConfirmRelease(d, a_String)) | An Axiom |
| test-889 | ⊦ ¬ isGetInputAirline(mkConfirmBooking(a_Integer)) | An Axiom |
| test-890 | ⊦ ¬ isGetInputAirline(mkConfirm) | An Axiom |
| test-891 | ⊦ ¬ isGetInputAirline(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-892 | ⊦ ¬ isGetInputAirline(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-893 | ⊦ ¬ isGetInputAgent(mkStart) | An Axiom |
| test-894 | ⊦ ¬ isGetInputAgent(mkShow(d)) | An Axiom |
| test-895 | ⊦ ¬ isGetInputAgent(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-896 | ⊦ ¬ isGetInputAgent(mkReleaseCCD(a_String)) | An Axiom |
| test-897 | ⊦ ¬ isGetInputAgent(mkPayCommission) | An Axiom |
| test-898 | ⊦ ¬ isGetInputAgent(mkOkPayCommission) | An Axiom |
| test-899 | ⊦ ¬ isGetInputAgent(mkOkConfirmBooking) | An Axiom |
| test-900 | ⊦ ¬ isGetInputAgent(mkGetSingleSelection(dl)) | An Axiom |
| test-901 | ⊦ ¬ isGetInputAgent(mkGetMultipleSelection(dl)) | An Axiom |
| test-902 | ⊦ ¬ isGetInputAgent(mkGetInputTravelPlanner) | An Axiom |
| test-903 | ⊦ ¬ isGetInputAgent(mkGetInputTravelAgency) | An Axiom |
| test-904 | ⊦ ¬ isGetInputAgent(mkGetInputString) | An Axiom |
| test-905 | ⊦ ¬ isGetInputAgent(mkGetInputRequestData) | An Axiom |
| test-906 | ⊦ ¬ isGetInputAgent(mkGetInputInteger) | An Axiom |
| test-907 | ⊦ ¬ isGetInputAgent(mkGetInputIFlowUtil) | An Axiom |
| test-908 | ⊦ ¬ isGetInputAgent(mkGetInputGPSPos) | An Axiom |
| test-909 | ⊦ ¬ isGetInputAgent(mkGetInputFlightOffer) | An Axiom |
| test-910 | ⊦ ¬ isGetInputAgent(mkGetInputData) | An Axiom |
| test-911 | ⊦ ¬ isGetInputAgent(mkGetInputCreditCardDetails) | An Axiom |
| test-912 | ⊦ ¬ isGetInputAgent(mkGetInputCreditCardCenter) | An Axiom |
| test-913 | ⊦ ¬ isGetInputAgent(mkGetInputBoolean) | An Axiom |
| test-914 | ⊦ ¬ isGetInputAgent(mkGetInputAirline) | An Axiom |
| test-915 | ⊦ isGetInputAgent(mkGetInputAgent) | An Axiom |
| test-916 | ⊦ ¬ isGetInputAgent(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-917 | ⊦ ¬ isGetInputAgent(mkGetDeclassifiedCCD) | An Axiom |
| test-918 | ⊦ ¬ isGetInputAgent(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-919 | ⊦ ¬ isGetInputAgent(mkConfirmRelease(d, a_String)) | An Axiom |
| test-920 | ⊦ ¬ isGetInputAgent(mkConfirmBooking(a_Integer)) | An Axiom |
| test-921 | ⊦ ¬ isGetInputAgent(mkConfirm) | An Axiom |
| test-922 | ⊦ ¬ isGetInputAgent(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-923 | ⊦ ¬ isGetInputAgent(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-924 | ⊦ ¬ isGetFlightOffers(mkStart) | An Axiom |
| test-925 | ⊦ ¬ isGetFlightOffers(mkShow(d)) | An Axiom |
| test-926 | ⊦ ¬ isGetFlightOffers(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-927 | ⊦ ¬ isGetFlightOffers(mkReleaseCCD(a_String)) | An Axiom |
| test-928 | ⊦ ¬ isGetFlightOffers(mkPayCommission) | An Axiom |
| test-929 | ⊦ ¬ isGetFlightOffers(mkOkPayCommission) | An Axiom |
| test-930 | ⊦ ¬ isGetFlightOffers(mkOkConfirmBooking) | An Axiom |
| test-931 | ⊦ ¬ isGetFlightOffers(mkGetSingleSelection(dl)) | An Axiom |
| test-932 | ⊦ ¬ isGetFlightOffers(mkGetMultipleSelection(dl)) | An Axiom |
| test-933 | ⊦ ¬ isGetFlightOffers(mkGetInputTravelPlanner) | An Axiom |
| test-934 | ⊦ ¬ isGetFlightOffers(mkGetInputTravelAgency) | An Axiom |
| test-935 | ⊦ ¬ isGetFlightOffers(mkGetInputString) | An Axiom |
| test-936 | ⊦ ¬ isGetFlightOffers(mkGetInputRequestData) | An Axiom |
| test-937 | ⊦ ¬ isGetFlightOffers(mkGetInputInteger) | An Axiom |
| test-938 | ⊦ ¬ isGetFlightOffers(mkGetInputIFlowUtil) | An Axiom |
| test-939 | ⊦ ¬ isGetFlightOffers(mkGetInputGPSPos) | An Axiom |
| test-940 | ⊦ ¬ isGetFlightOffers(mkGetInputFlightOffer) | An Axiom |
| test-941 | ⊦ ¬ isGetFlightOffers(mkGetInputData) | An Axiom |
| test-942 | ⊦ ¬ isGetFlightOffers(mkGetInputCreditCardDetails) | An Axiom |
| test-943 | ⊦ ¬ isGetFlightOffers(mkGetInputCreditCardCenter) | An Axiom |
| test-944 | ⊦ ¬ isGetFlightOffers(mkGetInputBoolean) | An Axiom |
| test-945 | ⊦ ¬ isGetFlightOffers(mkGetInputAirline) | An Axiom |
| test-946 | ⊦ ¬ isGetFlightOffers(mkGetInputAgent) | An Axiom |
| test-947 | ⊦ isGetFlightOffers(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-948 | ⊦ ¬ isGetFlightOffers(mkGetDeclassifiedCCD) | An Axiom |
| test-949 | ⊦ ¬ isGetFlightOffers(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-950 | ⊦ ¬ isGetFlightOffers(mkConfirmRelease(d, a_String)) | An Axiom |
| test-951 | ⊦ ¬ isGetFlightOffers(mkConfirmBooking(a_Integer)) | An Axiom |
| test-952 | ⊦ ¬ isGetFlightOffers(mkConfirm) | An Axiom |
| test-953 | ⊦ ¬ isGetFlightOffers(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-954 | ⊦ ¬ isGetFlightOffers(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-955 | ⊦ ¬ isGetDeclassifiedCCD(mkStart) | An Axiom |
| test-956 | ⊦ ¬ isGetDeclassifiedCCD(mkShow(d)) | An Axiom |
| test-957 | ⊦ ¬ isGetDeclassifiedCCD(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-958 | ⊦ ¬ isGetDeclassifiedCCD(mkReleaseCCD(a_String)) | An Axiom |
| test-959 | ⊦ ¬ isGetDeclassifiedCCD(mkPayCommission) | An Axiom |
| test-960 | ⊦ ¬ isGetDeclassifiedCCD(mkOkPayCommission) | An Axiom |
| test-961 | ⊦ ¬ isGetDeclassifiedCCD(mkOkConfirmBooking) | An Axiom |
| test-962 | ⊦ ¬ isGetDeclassifiedCCD(mkGetSingleSelection(dl)) | An Axiom |
| test-963 | ⊦ ¬ isGetDeclassifiedCCD(mkGetMultipleSelection(dl)) | An Axiom |
| test-964 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputTravelPlanner) | An Axiom |
| test-965 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputTravelAgency) | An Axiom |
| test-966 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputString) | An Axiom |
| test-967 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputRequestData) | An Axiom |
| test-968 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputInteger) | An Axiom |
| test-969 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputIFlowUtil) | An Axiom |
| test-970 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputGPSPos) | An Axiom |
| test-971 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputFlightOffer) | An Axiom |
| test-972 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputData) | An Axiom |
| test-973 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputCreditCardDetails) | An Axiom |
| test-974 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputCreditCardCenter) | An Axiom |
| test-975 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputBoolean) | An Axiom |
| test-976 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputAirline) | An Axiom |
| test-977 | ⊦ ¬ isGetDeclassifiedCCD(mkGetInputAgent) | An Axiom |
| test-978 | ⊦ ¬ isGetDeclassifiedCCD(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-979 | ⊦ isGetDeclassifiedCCD(mkGetDeclassifiedCCD) | An Axiom |
| test-980 | ⊦ ¬ isGetDeclassifiedCCD(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-981 | ⊦ ¬ isGetDeclassifiedCCD(mkConfirmRelease(d, a_String)) | An Axiom |
| test-982 | ⊦ ¬ isGetDeclassifiedCCD(mkConfirmBooking(a_Integer)) | An Axiom |
| test-983 | ⊦ ¬ isGetDeclassifiedCCD(mkConfirm) | An Axiom |
| test-984 | ⊦ ¬ isGetDeclassifiedCCD(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-985 | ⊦ ¬ isGetDeclassifiedCCD(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-986 | ⊦ ¬ isDeclassifiedCCD(mkStart) | An Axiom |
| test-987 | ⊦ ¬ isDeclassifiedCCD(mkShow(d)) | An Axiom |
| test-988 | ⊦ ¬ isDeclassifiedCCD(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-989 | ⊦ ¬ isDeclassifiedCCD(mkReleaseCCD(a_String)) | An Axiom |
| test-990 | ⊦ ¬ isDeclassifiedCCD(mkPayCommission) | An Axiom |
| test-991 | ⊦ ¬ isDeclassifiedCCD(mkOkPayCommission) | An Axiom |
| test-992 | ⊦ ¬ isDeclassifiedCCD(mkOkConfirmBooking) | An Axiom |
| test-993 | ⊦ ¬ isDeclassifiedCCD(mkGetSingleSelection(dl)) | An Axiom |
| test-994 | ⊦ ¬ isDeclassifiedCCD(mkGetMultipleSelection(dl)) | An Axiom |
| test-995 | ⊦ ¬ isDeclassifiedCCD(mkGetInputTravelPlanner) | An Axiom |
| test-996 | ⊦ ¬ isDeclassifiedCCD(mkGetInputTravelAgency) | An Axiom |
| test-997 | ⊦ ¬ isDeclassifiedCCD(mkGetInputString) | An Axiom |
| test-998 | ⊦ ¬ isDeclassifiedCCD(mkGetInputRequestData) | An Axiom |
| test-999 | ⊦ ¬ isDeclassifiedCCD(mkGetInputInteger) | An Axiom |
| test-1000 | ⊦ ¬ isDeclassifiedCCD(mkGetInputIFlowUtil) | An Axiom |
| test-1001 | ⊦ ¬ isDeclassifiedCCD(mkGetInputGPSPos) | An Axiom |
| test-1002 | ⊦ ¬ isDeclassifiedCCD(mkGetInputFlightOffer) | An Axiom |
| test-1003 | ⊦ ¬ isDeclassifiedCCD(mkGetInputData) | An Axiom |
| test-1004 | ⊦ ¬ isDeclassifiedCCD(mkGetInputCreditCardDetails) | An Axiom |
| test-1005 | ⊦ ¬ isDeclassifiedCCD(mkGetInputCreditCardCenter) | An Axiom |
| test-1006 | ⊦ ¬ isDeclassifiedCCD(mkGetInputBoolean) | An Axiom |
| test-1007 | ⊦ ¬ isDeclassifiedCCD(mkGetInputAirline) | An Axiom |
| test-1008 | ⊦ ¬ isDeclassifiedCCD(mkGetInputAgent) | An Axiom |
| test-1009 | ⊦ ¬ isDeclassifiedCCD(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-1010 | ⊦ ¬ isDeclassifiedCCD(mkGetDeclassifiedCCD) | An Axiom |
| test-1011 | ⊦ isDeclassifiedCCD(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-1012 | ⊦ ¬ isDeclassifiedCCD(mkConfirmRelease(d, a_String)) | An Axiom |
| test-1013 | ⊦ ¬ isDeclassifiedCCD(mkConfirmBooking(a_Integer)) | An Axiom |
| test-1014 | ⊦ ¬ isDeclassifiedCCD(mkConfirm) | An Axiom |
| test-1015 | ⊦ ¬ isDeclassifiedCCD(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-1016 | ⊦ ¬ isDeclassifiedCCD(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-1017 | ⊦ ¬ isConfirmRelease(mkStart) | An Axiom |
| test-1018 | ⊦ ¬ isConfirmRelease(mkShow(d)) | An Axiom |
| test-1019 | ⊦ ¬ isConfirmRelease(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-1020 | ⊦ ¬ isConfirmRelease(mkReleaseCCD(a_String)) | An Axiom |
| test-1021 | ⊦ ¬ isConfirmRelease(mkPayCommission) | An Axiom |
| test-1022 | ⊦ ¬ isConfirmRelease(mkOkPayCommission) | An Axiom |
| test-1023 | ⊦ ¬ isConfirmRelease(mkOkConfirmBooking) | An Axiom |
| test-1024 | ⊦ ¬ isConfirmRelease(mkGetSingleSelection(dl)) | An Axiom |
| test-1025 | ⊦ ¬ isConfirmRelease(mkGetMultipleSelection(dl)) | An Axiom |
| test-1026 | ⊦ ¬ isConfirmRelease(mkGetInputTravelPlanner) | An Axiom |
| test-1027 | ⊦ ¬ isConfirmRelease(mkGetInputTravelAgency) | An Axiom |
| test-1028 | ⊦ ¬ isConfirmRelease(mkGetInputString) | An Axiom |
| test-1029 | ⊦ ¬ isConfirmRelease(mkGetInputRequestData) | An Axiom |
| test-1030 | ⊦ ¬ isConfirmRelease(mkGetInputInteger) | An Axiom |
| test-1031 | ⊦ ¬ isConfirmRelease(mkGetInputIFlowUtil) | An Axiom |
| test-1032 | ⊦ ¬ isConfirmRelease(mkGetInputGPSPos) | An Axiom |
| test-1033 | ⊦ ¬ isConfirmRelease(mkGetInputFlightOffer) | An Axiom |
| test-1034 | ⊦ ¬ isConfirmRelease(mkGetInputData) | An Axiom |
| test-1035 | ⊦ ¬ isConfirmRelease(mkGetInputCreditCardDetails) | An Axiom |
| test-1036 | ⊦ ¬ isConfirmRelease(mkGetInputCreditCardCenter) | An Axiom |
| test-1037 | ⊦ ¬ isConfirmRelease(mkGetInputBoolean) | An Axiom |
| test-1038 | ⊦ ¬ isConfirmRelease(mkGetInputAirline) | An Axiom |
| test-1039 | ⊦ ¬ isConfirmRelease(mkGetInputAgent) | An Axiom |
| test-1040 | ⊦ ¬ isConfirmRelease(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-1041 | ⊦ ¬ isConfirmRelease(mkGetDeclassifiedCCD) | An Axiom |
| test-1042 | ⊦ ¬ isConfirmRelease(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-1043 | ⊦ isConfirmRelease(mkConfirmRelease(d, a_String)) | An Axiom |
| test-1044 | ⊦ ¬ isConfirmRelease(mkConfirmBooking(a_Integer)) | An Axiom |
| test-1045 | ⊦ ¬ isConfirmRelease(mkConfirm) | An Axiom |
| test-1046 | ⊦ ¬ isConfirmRelease(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-1047 | ⊦ ¬ isConfirmRelease(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-1048 | ⊦ ¬ isConfirmBooking(mkStart) | An Axiom |
| test-1049 | ⊦ ¬ isConfirmBooking(mkShow(d)) | An Axiom |
| test-1050 | ⊦ ¬ isConfirmBooking(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-1051 | ⊦ ¬ isConfirmBooking(mkReleaseCCD(a_String)) | An Axiom |
| test-1052 | ⊦ ¬ isConfirmBooking(mkPayCommission) | An Axiom |
| test-1053 | ⊦ ¬ isConfirmBooking(mkOkPayCommission) | An Axiom |
| test-1054 | ⊦ ¬ isConfirmBooking(mkOkConfirmBooking) | An Axiom |
| test-1055 | ⊦ ¬ isConfirmBooking(mkGetSingleSelection(dl)) | An Axiom |
| test-1056 | ⊦ ¬ isConfirmBooking(mkGetMultipleSelection(dl)) | An Axiom |
| test-1057 | ⊦ ¬ isConfirmBooking(mkGetInputTravelPlanner) | An Axiom |
| test-1058 | ⊦ ¬ isConfirmBooking(mkGetInputTravelAgency) | An Axiom |
| test-1059 | ⊦ ¬ isConfirmBooking(mkGetInputString) | An Axiom |
| test-1060 | ⊦ ¬ isConfirmBooking(mkGetInputRequestData) | An Axiom |
| test-1061 | ⊦ ¬ isConfirmBooking(mkGetInputInteger) | An Axiom |
| test-1062 | ⊦ ¬ isConfirmBooking(mkGetInputIFlowUtil) | An Axiom |
| test-1063 | ⊦ ¬ isConfirmBooking(mkGetInputGPSPos) | An Axiom |
| test-1064 | ⊦ ¬ isConfirmBooking(mkGetInputFlightOffer) | An Axiom |
| test-1065 | ⊦ ¬ isConfirmBooking(mkGetInputData) | An Axiom |
| test-1066 | ⊦ ¬ isConfirmBooking(mkGetInputCreditCardDetails) | An Axiom |
| test-1067 | ⊦ ¬ isConfirmBooking(mkGetInputCreditCardCenter) | An Axiom |
| test-1068 | ⊦ ¬ isConfirmBooking(mkGetInputBoolean) | An Axiom |
| test-1069 | ⊦ ¬ isConfirmBooking(mkGetInputAirline) | An Axiom |
| test-1070 | ⊦ ¬ isConfirmBooking(mkGetInputAgent) | An Axiom |
| test-1071 | ⊦ ¬ isConfirmBooking(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-1072 | ⊦ ¬ isConfirmBooking(mkGetDeclassifiedCCD) | An Axiom |
| test-1073 | ⊦ ¬ isConfirmBooking(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-1074 | ⊦ ¬ isConfirmBooking(mkConfirmRelease(d, a_String)) | An Axiom |
| test-1075 | ⊦ isConfirmBooking(mkConfirmBooking(a_Integer)) | An Axiom |
| test-1076 | ⊦ ¬ isConfirmBooking(mkConfirm) | An Axiom |
| test-1077 | ⊦ ¬ isConfirmBooking(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-1078 | ⊦ ¬ isConfirmBooking(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-1079 | ⊦ ¬ isConfirm(mkStart) | An Axiom |
| test-1080 | ⊦ ¬ isConfirm(mkShow(d)) | An Axiom |
| test-1081 | ⊦ ¬ isConfirm(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-1082 | ⊦ ¬ isConfirm(mkReleaseCCD(a_String)) | An Axiom |
| test-1083 | ⊦ ¬ isConfirm(mkPayCommission) | An Axiom |
| test-1084 | ⊦ ¬ isConfirm(mkOkPayCommission) | An Axiom |
| test-1085 | ⊦ ¬ isConfirm(mkOkConfirmBooking) | An Axiom |
| test-1086 | ⊦ ¬ isConfirm(mkGetSingleSelection(dl)) | An Axiom |
| test-1087 | ⊦ ¬ isConfirm(mkGetMultipleSelection(dl)) | An Axiom |
| test-1088 | ⊦ ¬ isConfirm(mkGetInputTravelPlanner) | An Axiom |
| test-1089 | ⊦ ¬ isConfirm(mkGetInputTravelAgency) | An Axiom |
| test-1090 | ⊦ ¬ isConfirm(mkGetInputString) | An Axiom |
| test-1091 | ⊦ ¬ isConfirm(mkGetInputRequestData) | An Axiom |
| test-1092 | ⊦ ¬ isConfirm(mkGetInputInteger) | An Axiom |
| test-1093 | ⊦ ¬ isConfirm(mkGetInputIFlowUtil) | An Axiom |
| test-1094 | ⊦ ¬ isConfirm(mkGetInputGPSPos) | An Axiom |
| test-1095 | ⊦ ¬ isConfirm(mkGetInputFlightOffer) | An Axiom |
| test-1096 | ⊦ ¬ isConfirm(mkGetInputData) | An Axiom |
| test-1097 | ⊦ ¬ isConfirm(mkGetInputCreditCardDetails) | An Axiom |
| test-1098 | ⊦ ¬ isConfirm(mkGetInputCreditCardCenter) | An Axiom |
| test-1099 | ⊦ ¬ isConfirm(mkGetInputBoolean) | An Axiom |
| test-1100 | ⊦ ¬ isConfirm(mkGetInputAirline) | An Axiom |
| test-1101 | ⊦ ¬ isConfirm(mkGetInputAgent) | An Axiom |
| test-1102 | ⊦ ¬ isConfirm(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-1103 | ⊦ ¬ isConfirm(mkGetDeclassifiedCCD) | An Axiom |
| test-1104 | ⊦ ¬ isConfirm(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-1105 | ⊦ ¬ isConfirm(mkConfirmRelease(d, a_String)) | An Axiom |
| test-1106 | ⊦ ¬ isConfirm(mkConfirmBooking(a_Integer)) | An Axiom |
| test-1107 | ⊦ isConfirm(mkConfirm) | An Axiom |
| test-1108 | ⊦ ¬ isConfirm(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-1109 | ⊦ ¬ isConfirm(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-1110 | ⊦ ¬ isBookSelected(mkStart) | An Axiom |
| test-1111 | ⊦ ¬ isBookSelected(mkShow(d)) | An Axiom |
| test-1112 | ⊦ ¬ isBookSelected(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-1113 | ⊦ ¬ isBookSelected(mkReleaseCCD(a_String)) | An Axiom |
| test-1114 | ⊦ ¬ isBookSelected(mkPayCommission) | An Axiom |
| test-1115 | ⊦ ¬ isBookSelected(mkOkPayCommission) | An Axiom |
| test-1116 | ⊦ ¬ isBookSelected(mkOkConfirmBooking) | An Axiom |
| test-1117 | ⊦ ¬ isBookSelected(mkGetSingleSelection(dl)) | An Axiom |
| test-1118 | ⊦ ¬ isBookSelected(mkGetMultipleSelection(dl)) | An Axiom |
| test-1119 | ⊦ ¬ isBookSelected(mkGetInputTravelPlanner) | An Axiom |
| test-1120 | ⊦ ¬ isBookSelected(mkGetInputTravelAgency) | An Axiom |
| test-1121 | ⊦ ¬ isBookSelected(mkGetInputString) | An Axiom |
| test-1122 | ⊦ ¬ isBookSelected(mkGetInputRequestData) | An Axiom |
| test-1123 | ⊦ ¬ isBookSelected(mkGetInputInteger) | An Axiom |
| test-1124 | ⊦ ¬ isBookSelected(mkGetInputIFlowUtil) | An Axiom |
| test-1125 | ⊦ ¬ isBookSelected(mkGetInputGPSPos) | An Axiom |
| test-1126 | ⊦ ¬ isBookSelected(mkGetInputFlightOffer) | An Axiom |
| test-1127 | ⊦ ¬ isBookSelected(mkGetInputData) | An Axiom |
| test-1128 | ⊦ ¬ isBookSelected(mkGetInputCreditCardDetails) | An Axiom |
| test-1129 | ⊦ ¬ isBookSelected(mkGetInputCreditCardCenter) | An Axiom |
| test-1130 | ⊦ ¬ isBookSelected(mkGetInputBoolean) | An Axiom |
| test-1131 | ⊦ ¬ isBookSelected(mkGetInputAirline) | An Axiom |
| test-1132 | ⊦ ¬ isBookSelected(mkGetInputAgent) | An Axiom |
| test-1133 | ⊦ ¬ isBookSelected(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-1134 | ⊦ ¬ isBookSelected(mkGetDeclassifiedCCD) | An Axiom |
| test-1135 | ⊦ ¬ isBookSelected(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-1136 | ⊦ ¬ isBookSelected(mkConfirmRelease(d, a_String)) | An Axiom |
| test-1137 | ⊦ ¬ isBookSelected(mkConfirmBooking(a_Integer)) | An Axiom |
| test-1138 | ⊦ ¬ isBookSelected(mkConfirm) | An Axiom |
| test-1139 | ⊦ isBookSelected(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-1140 | ⊦ ¬ isBookSelected(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| test-1141 | ⊦ ¬ isBookFlightOffer(mkStart) | An Axiom |
| test-1142 | ⊦ ¬ isBookFlightOffer(mkShow(d)) | An Axiom |
| test-1143 | ⊦ ¬ isBookFlightOffer(mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| test-1144 | ⊦ ¬ isBookFlightOffer(mkReleaseCCD(a_String)) | An Axiom |
| test-1145 | ⊦ ¬ isBookFlightOffer(mkPayCommission) | An Axiom |
| test-1146 | ⊦ ¬ isBookFlightOffer(mkOkPayCommission) | An Axiom |
| test-1147 | ⊦ ¬ isBookFlightOffer(mkOkConfirmBooking) | An Axiom |
| test-1148 | ⊦ ¬ isBookFlightOffer(mkGetSingleSelection(dl)) | An Axiom |
| test-1149 | ⊦ ¬ isBookFlightOffer(mkGetMultipleSelection(dl)) | An Axiom |
| test-1150 | ⊦ ¬ isBookFlightOffer(mkGetInputTravelPlanner) | An Axiom |
| test-1151 | ⊦ ¬ isBookFlightOffer(mkGetInputTravelAgency) | An Axiom |
| test-1152 | ⊦ ¬ isBookFlightOffer(mkGetInputString) | An Axiom |
| test-1153 | ⊦ ¬ isBookFlightOffer(mkGetInputRequestData) | An Axiom |
| test-1154 | ⊦ ¬ isBookFlightOffer(mkGetInputInteger) | An Axiom |
| test-1155 | ⊦ ¬ isBookFlightOffer(mkGetInputIFlowUtil) | An Axiom |
| test-1156 | ⊦ ¬ isBookFlightOffer(mkGetInputGPSPos) | An Axiom |
| test-1157 | ⊦ ¬ isBookFlightOffer(mkGetInputFlightOffer) | An Axiom |
| test-1158 | ⊦ ¬ isBookFlightOffer(mkGetInputData) | An Axiom |
| test-1159 | ⊦ ¬ isBookFlightOffer(mkGetInputCreditCardDetails) | An Axiom |
| test-1160 | ⊦ ¬ isBookFlightOffer(mkGetInputCreditCardCenter) | An Axiom |
| test-1161 | ⊦ ¬ isBookFlightOffer(mkGetInputBoolean) | An Axiom |
| test-1162 | ⊦ ¬ isBookFlightOffer(mkGetInputAirline) | An Axiom |
| test-1163 | ⊦ ¬ isBookFlightOffer(mkGetInputAgent) | An Axiom |
| test-1164 | ⊦ ¬ isBookFlightOffer(mkGetFlightOffers(a_RequestData)) | An Axiom |
| test-1165 | ⊦ ¬ isBookFlightOffer(mkGetDeclassifiedCCD) | An Axiom |
| test-1166 | ⊦ ¬ isBookFlightOffer(mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| test-1167 | ⊦ ¬ isBookFlightOffer(mkConfirmRelease(d, a_String)) | An Axiom |
| test-1168 | ⊦ ¬ isBookFlightOffer(mkConfirmBooking(a_Integer)) | An Axiom |
| test-1169 | ⊦ ¬ isBookFlightOffer(mkConfirm) | An Axiom |
| test-1170 | ⊦ ¬ isBookFlightOffer(mkBookSelected(a_FlightOffer)) | An Axiom |
| test-1171 | ⊦ isBookFlightOffer(mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| inj-01 | ⊦ d + dl = d0 + dl0 ↔ d = d0 ∧ dl = dl0 | An Axiom |
| inj-02 | ⊦ a_GPSPos + a_ListOfGPSPos = a_GPSPos0 + a_ListOfGPSPos0 ↔ a_GPSPos = a_GPSPos0 ∧ a_ListOfGPSPos = a_ListOfGPSPos0 | An Axiom |
| inj-03 | ⊦ a_FlightOffer + a_ListOfFlightOffer = a_FlightOffer0 + a_ListOfFlightOffer0 ↔ a_FlightOffer = a_FlightOffer0 ∧ a_ListOfFlightOffer = a_ListOfFlightOffer0 | An Axiom |
| inj-04 | ⊦ mkDataPair(d, d0) = mkDataPair(d1, d2) ↔ d = d1 ∧ d0 = d2 | An Axiom |
| inj-05 | ⊦ mkNat(m) = mkNat(m0) ↔ m = m0 | An Axiom |
| inj-06 | ⊦ wrapAgent2Data(ag) = wrapAgent2Data(ag0) ↔ ag = ag0 | An Axiom |
| inj-07 | ⊦ wrapListOfData2Data(dl) = wrapListOfData2Data(dl0) ↔ dl = dl0 | An Axiom |
| inj-08 | ⊦ wrapListOfGPSPos2Data(a_ListOfGPSPos) = wrapListOfGPSPos2Data(a_ListOfGPSPos0) ↔ a_ListOfGPSPos = a_ListOfGPSPos0 | An Axiom |
| inj-09 | ⊦ wrapListOfFlightOffer2Data(a_ListOfFlightOffer) = wrapListOfFlightOffer2Data(a_ListOfFlightOffer0) ↔ a_ListOfFlightOffer = a_ListOfFlightOffer0 | An Axiom |
| inj-10 | ⊦ wrapString2Data(a_String) = wrapString2Data(a_String0) ↔ a_String = a_String0 | An Axiom |
| inj-11 | ⊦ wrapRequestData2Data(a_RequestData) = wrapRequestData2Data(a_RequestData0) ↔ a_RequestData = a_RequestData0 | An Axiom |
| inj-12 | ⊦ wrapInteger2Data(a_Integer) = wrapInteger2Data(a_Integer0) ↔ a_Integer = a_Integer0 | An Axiom |
| inj-13 | ⊦ wrapGPSPos2Data(a_GPSPos) = wrapGPSPos2Data(a_GPSPos0) ↔ a_GPSPos = a_GPSPos0 | An Axiom |
| inj-14 | ⊦ wrapFlightOffer2Data(a_FlightOffer) = wrapFlightOffer2Data(a_FlightOffer0) ↔ a_FlightOffer = a_FlightOffer0 | An Axiom |
| inj-15 | ⊦ wrapCreditCardDetails2Data(a_CreditCardDetails) = wrapCreditCardDetails2Data(a_CreditCardDetails0) ↔ a_CreditCardDetails = a_CreditCardDetails0 | An Axiom |
| inj-16 | ⊦ wrapBoolean2Data(a_Boolean) = wrapBoolean2Data(a_Boolean0) ↔ a_Boolean = a_Boolean0 | An Axiom |
| inj-17 | ⊦ wrapMessage2Data(msg) = wrapMessage2Data(msg0) ↔ msg = msg0 | An Axiom |
| inj-18 | ⊦ mkString(stringvar) = mkString(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-19 | ⊦ mkRequestData(a_String) = mkRequestData(a_String0) ↔ a_String = a_String0 | An Axiom |
| inj-20 | ⊦ mkInteger(i) = mkInteger(i0) ↔ i = i0 | An Axiom |
| inj-21 | ⊦ mkGPSPos(a_String, a_String0) = mkGPSPos(a_String1, a_String2) ↔ a_String = a_String1 ∧ a_String0 = a_String2 | An Axiom |
| inj-22 | ⊦ mkFlightOffer(a_Integer, a_String) = mkFlightOffer(a_Integer0, a_String0) ↔ a_Integer = a_Integer0 ∧ a_String = a_String0 | An Axiom |
| inj-23 | ⊦ mkBoolean(boolvar) = mkBoolean(boolvar0) ↔ (boolvar ↔ boolvar0) | An Axiom |
| inj-24 | ⊦ mkShow(d) = mkShow(d0) ↔ d = d0 | An Axiom |
| inj-25 | ⊦ mkRetFlightOffers(a_ListOfFlightOffer) = mkRetFlightOffers(a_ListOfFlightOffer0) ↔ a_ListOfFlightOffer = a_ListOfFlightOffer0 | An Axiom |
| inj-26 | ⊦ mkReleaseCCD(a_String) = mkReleaseCCD(a_String0) ↔ a_String = a_String0 | An Axiom |
| inj-27 | ⊦ mkGetSingleSelection(dl) = mkGetSingleSelection(dl0) ↔ dl = dl0 | An Axiom |
| inj-28 | ⊦ mkGetMultipleSelection(dl) = mkGetMultipleSelection(dl0) ↔ dl = dl0 | An Axiom |
| inj-29 | ⊦ mkGetFlightOffers(a_RequestData) = mkGetFlightOffers(a_RequestData0) ↔ a_RequestData = a_RequestData0 | An Axiom |
| inj-30 | ⊦ mkDeclassifiedCCD(a_CreditCardDetails) = mkDeclassifiedCCD(a_CreditCardDetails0) ↔ a_CreditCardDetails = a_CreditCardDetails0 | An Axiom |
| inj-31 | ⊦ mkConfirmRelease(d, a_String) = mkConfirmRelease(d0, a_String0) ↔ d = d0 ∧ a_String = a_String0 | An Axiom |
| inj-32 | ⊦ mkConfirmBooking(a_Integer) = mkConfirmBooking(a_Integer0) ↔ a_Integer = a_Integer0 | An Axiom |
| inj-33 | ⊦ mkBookSelected(a_FlightOffer) = mkBookSelected(a_FlightOffer0) ↔ a_FlightOffer = a_FlightOffer0 | An Axiom |
| inj-34 | ⊦ mkBookFlightOffer(a_Integer, a_CreditCardDetails) = mkBookFlightOffer(a_Integer0, a_CreditCardDetails0) ↔ a_Integer = a_Integer0 ∧ a_CreditCardDetails = a_CreditCardDetails0 | An Axiom |
| inj-35 | ⊦ mkMessage(agl, cntnt) = mkMessage(agl0, cntnt0) ↔ agl = agl0 ∧ cntnt = cntnt0 | An Axiom |
| case-01 | ⊦ dl = [] ∨ dl = dl .first + dl .rest | An Axiom |
| case-02 | ⊦ a_ListOfGPSPos = [] ∨ a_ListOfGPSPos = a_ListOfGPSPos .first + a_ListOfGPSPos .rest | An Axiom |
| case-03 | ⊦ a_ListOfFlightOffer = [] ∨ a_ListOfFlightOffer = a_ListOfFlightOffer .first + a_ListOfFlightOffer .rest | An Axiom |
| case-04 | ⊦ d = wrapMessage2Data(d .msg) ∨ d = wrapBoolean2Data(d .Boolean) ∨ d = wrapCreditCardDetails2Data(d .CreditCardDetails) ∨ d = wrapFlightOffer2Data(d .FlightOffer) ∨ d = wrapGPSPos2Data(d .GPSPos) ∨ d = wrapInteger2Data(d .Integer) ∨ d = wrapRequestData2Data(d .RequestData) ∨ d = wrapString2Data(d .String) ∨ d = wrapListOfFlightOffer2Data(d .ListOfFlightOffer) ∨ d = wrapListOfGPSPos2Data(d .ListOfGPSPos) ∨ d = wrapListOfData2Data(d .ListOfData) ∨ d = wrapAgent2Data(d .Agent) ∨ d = mkNat(d .nat) ∨ d = mkDataPair(d .1, d .2) ∨ d = null | An Axiom |
| case-05 | ⊦ mkString(a_String .value) = a_String | An Axiom |
| case-06 | ⊦ mkRequestData(a_RequestData .date) = a_RequestData | An Axiom |
| case-07 | ⊦ mkInteger(a_Integer .value) = a_Integer | An Axiom |
| case-08 | ⊦ mkGPSPos(a_GPSPos .latitude, a_GPSPos .longitude) = a_GPSPos | An Axiom |
| case-09 | ⊦ mkFlightOffer(a_FlightOffer .id, a_FlightOffer .airline) = a_FlightOffer | An Axiom |
| case-10 | ⊦ mkCreditCardDetails = a_CreditCardDetails | An Axiom |
| case-11 | ⊦ mkBoolean(a_Boolean .value) = a_Boolean | An Axiom |
| case-12 | ⊦ cntnt = mkBookFlightOffer(cntnt .id, cntnt .ccd) ∨ cntnt = mkBookSelected(cntnt .flightOffer) ∨ cntnt = mkConfirm ∨ cntnt = mkConfirmBooking(cntnt .id) ∨ cntnt = mkConfirmRelease(cntnt .what, cntnt .receiver) ∨ cntnt = mkDeclassifiedCCD(cntnt .ccd) ∨ cntnt = mkGetDeclassifiedCCD ∨ cntnt = mkGetFlightOffers(cntnt .requestData) ∨ cntnt = mkGetInputAgent ∨ cntnt = mkGetInputAirline ∨ cntnt = mkGetInputBoolean ∨ cntnt = mkGetInputCreditCardCenter ∨ cntnt = mkGetInputCreditCardDetails ∨ cntnt = mkGetInputData ∨ cntnt = mkGetInputFlightOffer ∨ cntnt = mkGetInputGPSPos ∨ cntnt = mkGetInputIFlowUtil ∨ cntnt = mkGetInputInteger ∨ cntnt = mkGetInputRequestData ∨ cntnt = mkGetInputString ∨ cntnt = mkGetInputTravelAgency ∨ cntnt = mkGetInputTravelPlanner ∨ cntnt = mkGetMultipleSelection(cntnt .selection) ∨ cntnt = mkGetSingleSelection(cntnt .selection) ∨ cntnt = mkOkConfirmBooking ∨ cntnt = mkOkPayCommission ∨ cntnt = mkPayCommission ∨ cntnt = mkReleaseCCD(cntnt .receiver) ∨ cntnt = mkRetFlightOffers(cntnt .flightOffers) ∨ cntnt = mkShow(cntnt .data) ∨ cntnt = mkStart | An Axiom |
| case-13 | ⊦ mkMessage(msg .agentlist, msg .content) = msg | An Axiom |
| size-01 | ⊦ # (d + dl) = (# dl) +1 | An Axiom |
| size-02 | ⊦ # [] = 0 | An Axiom |
| ref | ⊦ ¬ dl < dl | An Axiom |
| trans | ⊦ dl < dl0 ∧ dl0 < dl1 → dl < dl1 | An Axiom |
| less-01 | ⊦ dl0 < d + dl ↔ dl0 = dl ∨ dl0 < dl | An Axiom |
| less-02 | ⊦ ¬ dl < [] | An Axiom |
| ex-01 | ⊦ isPair(d) ↔ (∃ d0, d1. d = mkDataPair(d0, d1)) | An Axiom |
| ex-02 | ⊦ isNat(d) ↔ (∃ m. d = mkNat(m)) | An Axiom |
| ex-03 | ⊦ isAgent(d) ↔ (∃ ag. d = wrapAgent2Data(ag)) | An Axiom |
| ex-04 | ⊦ isListOfData(d) ↔ (∃ dl. d = wrapListOfData2Data(dl)) | An Axiom |
| ex-05 | ⊦ isListOfGPSPos(d) ↔ (∃ a_ListOfGPSPos. d = wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| ex-06 | ⊦ isListOfFlightOffer(d) ↔ (∃ a_ListOfFlightOffer. d = wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| ex-07 | ⊦ isString(d) ↔ (∃ a_String. d = wrapString2Data(a_String)) | An Axiom |
| ex-08 | ⊦ isRequestData(d) ↔ (∃ a_RequestData. d = wrapRequestData2Data(a_RequestData)) | An Axiom |
| ex-09 | ⊦ isInteger(d) ↔ (∃ a_Integer. d = wrapInteger2Data(a_Integer)) | An Axiom |
| ex-10 | ⊦ isGPSPos(d) ↔ (∃ a_GPSPos. d = wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| ex-11 | ⊦ isFlightOffer(d) ↔ (∃ a_FlightOffer. d = wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| ex-12 | ⊦ isCreditCardDetails(d) ↔ (∃ a_CreditCardDetails. d = wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| ex-13 | ⊦ isBoolean(d) ↔ (∃ a_Boolean. d = wrapBoolean2Data(a_Boolean)) | An Axiom |
| ex-14 | ⊦ isMessage(d) ↔ (∃ msg. d = wrapMessage2Data(msg)) | An Axiom |
| ex-15 | ⊦ isStart(cntnt) ↔ cntnt = mkStart | An Axiom |
| ex-16 | ⊦ isShow(cntnt) ↔ (∃ d. cntnt = mkShow(d)) | An Axiom |
| ex-17 | ⊦ isRetFlightOffers(cntnt) ↔ (∃ a_ListOfFlightOffer. cntnt = mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| ex-18 | ⊦ isReleaseCCD(cntnt) ↔ (∃ a_String. cntnt = mkReleaseCCD(a_String)) | An Axiom |
| ex-19 | ⊦ isPayCommission(cntnt) ↔ cntnt = mkPayCommission | An Axiom |
| ex-20 | ⊦ isOkPayCommission(cntnt) ↔ cntnt = mkOkPayCommission | An Axiom |
| ex-21 | ⊦ isOkConfirmBooking(cntnt) ↔ cntnt = mkOkConfirmBooking | An Axiom |
| ex-22 | ⊦ isGetSingleSelection(cntnt) ↔ (∃ dl. cntnt = mkGetSingleSelection(dl)) | An Axiom |
| ex-23 | ⊦ isGetMultipleSelection(cntnt) ↔ (∃ dl. cntnt = mkGetMultipleSelection(dl)) | An Axiom |
| ex-24 | ⊦ isGetInputTravelPlanner(cntnt) ↔ cntnt = mkGetInputTravelPlanner | An Axiom |
| ex-25 | ⊦ isGetInputTravelAgency(cntnt) ↔ cntnt = mkGetInputTravelAgency | An Axiom |
| ex-26 | ⊦ isGetInputString(cntnt) ↔ cntnt = mkGetInputString | An Axiom |
| ex-27 | ⊦ isGetInputRequestData(cntnt) ↔ cntnt = mkGetInputRequestData | An Axiom |
| ex-28 | ⊦ isGetInputInteger(cntnt) ↔ cntnt = mkGetInputInteger | An Axiom |
| ex-29 | ⊦ isGetInputIFlowUtil(cntnt) ↔ cntnt = mkGetInputIFlowUtil | An Axiom |
| ex-30 | ⊦ isGetInputGPSPos(cntnt) ↔ cntnt = mkGetInputGPSPos | An Axiom |
| ex-31 | ⊦ isGetInputFlightOffer(cntnt) ↔ cntnt = mkGetInputFlightOffer | An Axiom |
| ex-32 | ⊦ isGetInputData(cntnt) ↔ cntnt = mkGetInputData | An Axiom |
| ex-33 | ⊦ isGetInputCreditCardDetails(cntnt) ↔ cntnt = mkGetInputCreditCardDetails | An Axiom |
| ex-34 | ⊦ isGetInputCreditCardCenter(cntnt) ↔ cntnt = mkGetInputCreditCardCenter | An Axiom |
| ex-35 | ⊦ isGetInputBoolean(cntnt) ↔ cntnt = mkGetInputBoolean | An Axiom |
| ex-36 | ⊦ isGetInputAirline(cntnt) ↔ cntnt = mkGetInputAirline | An Axiom |
| ex-37 | ⊦ isGetInputAgent(cntnt) ↔ cntnt = mkGetInputAgent | An Axiom |
| ex-38 | ⊦ isGetFlightOffers(cntnt) ↔ (∃ a_RequestData. cntnt = mkGetFlightOffers(a_RequestData)) | An Axiom |
| ex-39 | ⊦ isGetDeclassifiedCCD(cntnt) ↔ cntnt = mkGetDeclassifiedCCD | An Axiom |
| ex-40 | ⊦ isDeclassifiedCCD(cntnt) ↔ (∃ a_CreditCardDetails. cntnt = mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| ex-41 | ⊦ isConfirmRelease(cntnt) ↔ (∃ d, a_String. cntnt = mkConfirmRelease(d, a_String)) | An Axiom |
| ex-42 | ⊦ isConfirmBooking(cntnt) ↔ (∃ a_Integer. cntnt = mkConfirmBooking(a_Integer)) | An Axiom |
| ex-43 | ⊦ isConfirm(cntnt) ↔ cntnt = mkConfirm | An Axiom |
| ex-44 | ⊦ isBookSelected(cntnt) ↔ (∃ a_FlightOffer. cntnt = mkBookSelected(a_FlightOffer)) | An Axiom |
| ex-45 | ⊦ isBookFlightOffer(cntnt) ↔ (∃ a_Integer, a_CreditCardDetails. cntnt = mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| elim-01 | ⊦ dl ≠ [] → (d = dl .first ∧ dl0 = dl .rest ↔ dl = d + dl0) | An Axiom |
| elim-02 | ⊦ a_ListOfGPSPos ≠ [] → (a_GPSPos = a_ListOfGPSPos .first ∧ a_ListOfGPSPos0 = a_ListOfGPSPos .rest ↔ a_ListOfGPSPos = a_GPSPos + a_ListOfGPSPos0) | An Axiom |
| elim-03 | ⊦ a_ListOfFlightOffer ≠ [] → ( a_FlightOffer = a_ListOfFlightOffer .first ∧ a_ListOfFlightOffer0 = a_ListOfFlightOffer .rest ↔ a_ListOfFlightOffer = a_FlightOffer + a_ListOfFlightOffer0) | An Axiom |
| elim-04 | ⊦ isPair(d) → (d0 = d .1 ∧ d1 = d .2 ↔ d = mkDataPair(d0, d1)) | An Axiom |
| elim-05 | ⊦ isNat(d) → (m = d .nat ↔ d = mkNat(m)) | An Axiom |
| elim-06 | ⊦ isAgent(d) → (ag = d .Agent ↔ d = wrapAgent2Data(ag)) | An Axiom |
| elim-07 | ⊦ isListOfData(d) → (dl = d .ListOfData ↔ d = wrapListOfData2Data(dl)) | An Axiom |
| elim-08 | ⊦ isListOfGPSPos(d) → (a_ListOfGPSPos = d .ListOfGPSPos ↔ d = wrapListOfGPSPos2Data(a_ListOfGPSPos)) | An Axiom |
| elim-09 | ⊦ isListOfFlightOffer(d) → (a_ListOfFlightOffer = d .ListOfFlightOffer ↔ d = wrapListOfFlightOffer2Data(a_ListOfFlightOffer)) | An Axiom |
| elim-10 | ⊦ isString(d) → (a_String = d .String ↔ d = wrapString2Data(a_String)) | An Axiom |
| elim-11 | ⊦ isRequestData(d) → (a_RequestData = d .RequestData ↔ d = wrapRequestData2Data(a_RequestData)) | An Axiom |
| elim-12 | ⊦ isInteger(d) → (a_Integer = d .Integer ↔ d = wrapInteger2Data(a_Integer)) | An Axiom |
| elim-13 | ⊦ isGPSPos(d) → (a_GPSPos = d .GPSPos ↔ d = wrapGPSPos2Data(a_GPSPos)) | An Axiom |
| elim-14 | ⊦ isFlightOffer(d) → (a_FlightOffer = d .FlightOffer ↔ d = wrapFlightOffer2Data(a_FlightOffer)) | An Axiom |
| elim-15 | ⊦ isCreditCardDetails(d) → (a_CreditCardDetails = d .CreditCardDetails ↔ d = wrapCreditCardDetails2Data(a_CreditCardDetails)) | An Axiom |
| elim-16 | ⊦ isBoolean(d) → (a_Boolean = d .Boolean ↔ d = wrapBoolean2Data(a_Boolean)) | An Axiom |
| elim-17 | ⊦ isMessage(d) → (msg = d .msg ↔ d = wrapMessage2Data(msg)) | An Axiom |
| elim-18 | ⊦ stringvar = a_String .value ↔ a_String = mkString(stringvar) | An Axiom |
| elim-19 | ⊦ a_String = a_RequestData .date ↔ a_RequestData = mkRequestData(a_String) | An Axiom |
| elim-20 | ⊦ i = a_Integer .value ↔ a_Integer = mkInteger(i) | An Axiom |
| elim-21 | ⊦ a_String = a_GPSPos .latitude ∧ a_String0 = a_GPSPos .longitude ↔ a_GPSPos = mkGPSPos(a_String, a_String0) | An Axiom |
| elim-22 | ⊦ a_Integer = a_FlightOffer .id ∧ a_String = a_FlightOffer .airline ↔ a_FlightOffer = mkFlightOffer(a_Integer, a_String) | An Axiom |
| elim-23 | ⊦ (boolvar ↔ a_Boolean .value) ↔ a_Boolean = mkBoolean(boolvar) | An Axiom |
| elim-24 | ⊦ isShow(cntnt) → (d = cntnt .data ↔ cntnt = mkShow(d)) | An Axiom |
| elim-25 | ⊦ isRetFlightOffers(cntnt) → (a_ListOfFlightOffer = cntnt .flightOffers ↔ cntnt = mkRetFlightOffers(a_ListOfFlightOffer)) | An Axiom |
| elim-26 | ⊦ isReleaseCCD(cntnt) → (a_String = cntnt .receiver ↔ cntnt = mkReleaseCCD(a_String)) | An Axiom |
| elim-27 | ⊦ isGetSingleSelection(cntnt) → (dl = cntnt .selection ↔ cntnt = mkGetSingleSelection(dl)) | An Axiom |
| elim-28 | ⊦ isGetMultipleSelection(cntnt) → (dl = cntnt .selection ↔ cntnt = mkGetMultipleSelection(dl)) | An Axiom |
| elim-29 | ⊦ isGetFlightOffers(cntnt) → (a_RequestData = cntnt .requestData ↔ cntnt = mkGetFlightOffers(a_RequestData)) | An Axiom |
| elim-30 | ⊦ isDeclassifiedCCD(cntnt) → (a_CreditCardDetails = cntnt .ccd ↔ cntnt = mkDeclassifiedCCD(a_CreditCardDetails)) | An Axiom |
| elim-31 | ⊦ isConfirmRelease(cntnt) → (d = cntnt .what ∧ a_String = cntnt .receiver ↔ cntnt = mkConfirmRelease(d, a_String)) | An Axiom |
| elim-32 | ⊦ isConfirmBooking(cntnt) → (a_Integer = cntnt .id ↔ cntnt = mkConfirmBooking(a_Integer)) | An Axiom |
| elim-33 | ⊦ isBookSelected(cntnt) → (a_FlightOffer = cntnt .flightOffer ↔ cntnt = mkBookSelected(a_FlightOffer)) | An Axiom |
| elim-34 | ⊦ isBookFlightOffer(cntnt) → (a_Integer = cntnt .id ∧ a_CreditCardDetails = cntnt .ccd ↔ cntnt = mkBookFlightOffer(a_Integer, a_CreditCardDetails)) | An Axiom |
| elim-35 | ⊦ agl = msg .agentlist ∧ cntnt = msg .content ↔ msg = mkMessage(agl, cntnt) | An Axiom |
| gen | An Axiom | |
| noeth | An Axiom |