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 | ⊦ Airline-flightOffers ≠ CreditCardCenter-ccd | An Axiom |
| disj-02 | ⊦ Airline-flightOffers ≠ TravelPlanner-flightOffer | An Axiom |
| disj-03 | ⊦ Airline-flightOffers ≠ locVar(stringvar) | An Axiom |
| disj-04 | ⊦ Airline-flightOffers ≠ state(stringvar) | An Axiom |
| disj-05 | ⊦ Airline-flightOffers ≠ Mailbox(cmd) | An Axiom |
| disj-06 | ⊦ Airline-flightOffers ≠ declassify-count(stringvar) | An Axiom |
| disj-07 | ⊦ Airline-flightOffers ≠ User-ConfirmRelease(stringvar) | An Axiom |
| disj-08 | ⊦ Airline-flightOffers ≠ User-ConfirmReleases(stringvar) | An Axiom |
| disj-09 | ⊦ Airline-flightOffers ≠ User-ConfirmRelease-count(stringvar) | An Axiom |
| disj-10 | ⊦ Airline-flightOffers ≠ User-ConfirmedRelease-count(stringvar) | An Axiom |
| disj-11 | ⊦ Airline-flightOffers ≠ User-GetSingleSelection(stringvar) | An Axiom |
| disj-12 | ⊦ Airline-flightOffers ≠ User-GetSingleSelections(stringvar) | An Axiom |
| disj-13 | ⊦ Airline-flightOffers ≠ User-GetSingleSelection-count(stringvar) | An Axiom |
| disj-14 | ⊦ Airline-flightOffers ≠ User-GetMultipleSelection(stringvar) | An Axiom |
| disj-15 | ⊦ Airline-flightOffers ≠ User-GetMultipleSelections(stringvar) | An Axiom |
| disj-16 | ⊦ Airline-flightOffers ≠ User-GetMultipleSelection-count(stringvar) | An Axiom |
| disj-17 | ⊦ Airline-flightOffers ≠ User-GetInput(stringvar) | An Axiom |
| disj-18 | ⊦ Airline-flightOffers ≠ User-GetInputs(stringvar) | An Axiom |
| disj-19 | ⊦ Airline-flightOffers ≠ User-GetInput-count(stringvar) | An Axiom |
| disj-20 | ⊦ Airline-flightOffers ≠ User-Confirm(stringvar) | An Axiom |
| disj-21 | ⊦ Airline-flightOffers ≠ User-Confirms(stringvar) | An Axiom |
| disj-22 | ⊦ Airline-flightOffers ≠ User-Confirm-count(stringvar) | An Axiom |
| disj-23 | ⊦ Airline-flightOffers ≠ ReadSourceInputs(stringvar, stringvar0) | An Axiom |
| disj-24 | ⊦ Airline-flightOffers ≠ ReadSourceCount(stringvar, stringvar0) | An Axiom |
| disj-25 | ⊦ CreditCardCenter-ccd ≠ TravelPlanner-flightOffer | An Axiom |
| disj-26 | ⊦ CreditCardCenter-ccd ≠ locVar(stringvar) | An Axiom |
| disj-27 | ⊦ CreditCardCenter-ccd ≠ state(stringvar) | An Axiom |
| disj-28 | ⊦ CreditCardCenter-ccd ≠ Mailbox(cmd) | An Axiom |
| disj-29 | ⊦ CreditCardCenter-ccd ≠ declassify-count(stringvar) | An Axiom |
| disj-30 | ⊦ CreditCardCenter-ccd ≠ User-ConfirmRelease(stringvar) | An Axiom |
| disj-31 | ⊦ CreditCardCenter-ccd ≠ User-ConfirmReleases(stringvar) | An Axiom |
| disj-32 | ⊦ CreditCardCenter-ccd ≠ User-ConfirmRelease-count(stringvar) | An Axiom |
| disj-33 | ⊦ CreditCardCenter-ccd ≠ User-ConfirmedRelease-count(stringvar) | An Axiom |
| disj-34 | ⊦ CreditCardCenter-ccd ≠ User-GetSingleSelection(stringvar) | An Axiom |
| disj-35 | ⊦ CreditCardCenter-ccd ≠ User-GetSingleSelections(stringvar) | An Axiom |
| disj-36 | ⊦ CreditCardCenter-ccd ≠ User-GetSingleSelection-count(stringvar) | An Axiom |
| disj-37 | ⊦ CreditCardCenter-ccd ≠ User-GetMultipleSelection(stringvar) | An Axiom |
| disj-38 | ⊦ CreditCardCenter-ccd ≠ User-GetMultipleSelections(stringvar) | An Axiom |
| disj-39 | ⊦ CreditCardCenter-ccd ≠ User-GetMultipleSelection-count(stringvar) | An Axiom |
| disj-40 | ⊦ CreditCardCenter-ccd ≠ User-GetInput(stringvar) | An Axiom |
| disj-41 | ⊦ CreditCardCenter-ccd ≠ User-GetInputs(stringvar) | An Axiom |
| disj-42 | ⊦ CreditCardCenter-ccd ≠ User-GetInput-count(stringvar) | An Axiom |
| disj-43 | ⊦ CreditCardCenter-ccd ≠ User-Confirm(stringvar) | An Axiom |
| disj-44 | ⊦ CreditCardCenter-ccd ≠ User-Confirms(stringvar) | An Axiom |
| disj-45 | ⊦ CreditCardCenter-ccd ≠ User-Confirm-count(stringvar) | An Axiom |
| disj-46 | ⊦ CreditCardCenter-ccd ≠ ReadSourceInputs(stringvar, stringvar0) | An Axiom |
| disj-47 | ⊦ CreditCardCenter-ccd ≠ ReadSourceCount(stringvar, stringvar0) | An Axiom |
| disj-48 | ⊦ TravelPlanner-flightOffer ≠ locVar(stringvar) | An Axiom |
| disj-49 | ⊦ TravelPlanner-flightOffer ≠ state(stringvar) | An Axiom |
| disj-50 | ⊦ TravelPlanner-flightOffer ≠ Mailbox(cmd) | An Axiom |
| disj-51 | ⊦ TravelPlanner-flightOffer ≠ declassify-count(stringvar) | An Axiom |
| disj-52 | ⊦ TravelPlanner-flightOffer ≠ User-ConfirmRelease(stringvar) | An Axiom |
| disj-53 | ⊦ TravelPlanner-flightOffer ≠ User-ConfirmReleases(stringvar) | An Axiom |
| disj-54 | ⊦ TravelPlanner-flightOffer ≠ User-ConfirmRelease-count(stringvar) | An Axiom |
| disj-55 | ⊦ TravelPlanner-flightOffer ≠ User-ConfirmedRelease-count(stringvar) | An Axiom |
| disj-56 | ⊦ TravelPlanner-flightOffer ≠ User-GetSingleSelection(stringvar) | An Axiom |
| disj-57 | ⊦ TravelPlanner-flightOffer ≠ User-GetSingleSelections(stringvar) | An Axiom |
| disj-58 | ⊦ TravelPlanner-flightOffer ≠ User-GetSingleSelection-count(stringvar) | An Axiom |
| disj-59 | ⊦ TravelPlanner-flightOffer ≠ User-GetMultipleSelection(stringvar) | An Axiom |
| disj-60 | ⊦ TravelPlanner-flightOffer ≠ User-GetMultipleSelections(stringvar) | An Axiom |
| disj-61 | ⊦ TravelPlanner-flightOffer ≠ User-GetMultipleSelection-count(stringvar) | An Axiom |
| disj-62 | ⊦ TravelPlanner-flightOffer ≠ User-GetInput(stringvar) | An Axiom |
| disj-63 | ⊦ TravelPlanner-flightOffer ≠ User-GetInputs(stringvar) | An Axiom |
| disj-64 | ⊦ TravelPlanner-flightOffer ≠ User-GetInput-count(stringvar) | An Axiom |
| disj-65 | ⊦ TravelPlanner-flightOffer ≠ User-Confirm(stringvar) | An Axiom |
| disj-66 | ⊦ TravelPlanner-flightOffer ≠ User-Confirms(stringvar) | An Axiom |
| disj-67 | ⊦ TravelPlanner-flightOffer ≠ User-Confirm-count(stringvar) | An Axiom |
| disj-68 | ⊦ TravelPlanner-flightOffer ≠ ReadSourceInputs(stringvar, stringvar0) | An Axiom |
| disj-69 | ⊦ TravelPlanner-flightOffer ≠ ReadSourceCount(stringvar, stringvar0) | An Axiom |
| disj-70 | ⊦ locVar(stringvar) ≠ state(stringvar0) | An Axiom |
| disj-71 | ⊦ locVar(stringvar) ≠ Mailbox(cmd) | An Axiom |
| disj-72 | ⊦ locVar(stringvar) ≠ declassify-count(stringvar0) | An Axiom |
| disj-73 | ⊦ locVar(stringvar) ≠ User-ConfirmRelease(stringvar0) | An Axiom |
| disj-74 | ⊦ locVar(stringvar) ≠ User-ConfirmReleases(stringvar0) | An Axiom |
| disj-75 | ⊦ locVar(stringvar) ≠ User-ConfirmRelease-count(stringvar0) | An Axiom |
| disj-76 | ⊦ locVar(stringvar) ≠ User-ConfirmedRelease-count(stringvar0) | An Axiom |
| disj-77 | ⊦ locVar(stringvar) ≠ User-GetSingleSelection(stringvar0) | An Axiom |
| disj-78 | ⊦ locVar(stringvar) ≠ User-GetSingleSelections(stringvar0) | An Axiom |
| disj-79 | ⊦ locVar(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-80 | ⊦ locVar(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-81 | ⊦ locVar(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-82 | ⊦ locVar(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-83 | ⊦ locVar(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-84 | ⊦ locVar(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-85 | ⊦ locVar(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-86 | ⊦ locVar(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-87 | ⊦ locVar(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-88 | ⊦ locVar(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-89 | ⊦ locVar(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-90 | ⊦ locVar(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-91 | ⊦ state(stringvar) ≠ Mailbox(cmd) | An Axiom |
| disj-92 | ⊦ state(stringvar) ≠ declassify-count(stringvar0) | An Axiom |
| disj-93 | ⊦ state(stringvar) ≠ User-ConfirmRelease(stringvar0) | An Axiom |
| disj-94 | ⊦ state(stringvar) ≠ User-ConfirmReleases(stringvar0) | An Axiom |
| disj-95 | ⊦ state(stringvar) ≠ User-ConfirmRelease-count(stringvar0) | An Axiom |
| disj-96 | ⊦ state(stringvar) ≠ User-ConfirmedRelease-count(stringvar0) | An Axiom |
| disj-97 | ⊦ state(stringvar) ≠ User-GetSingleSelection(stringvar0) | An Axiom |
| disj-98 | ⊦ state(stringvar) ≠ User-GetSingleSelections(stringvar0) | An Axiom |
| disj-99 | ⊦ state(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-100 | ⊦ state(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-101 | ⊦ state(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-102 | ⊦ state(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-103 | ⊦ state(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-104 | ⊦ state(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-105 | ⊦ state(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-106 | ⊦ state(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-107 | ⊦ state(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-108 | ⊦ state(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-109 | ⊦ state(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-110 | ⊦ state(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-111 | ⊦ Mailbox(cmd) ≠ declassify-count(stringvar) | An Axiom |
| disj-112 | ⊦ Mailbox(cmd) ≠ User-ConfirmRelease(stringvar) | An Axiom |
| disj-113 | ⊦ Mailbox(cmd) ≠ User-ConfirmReleases(stringvar) | An Axiom |
| disj-114 | ⊦ Mailbox(cmd) ≠ User-ConfirmRelease-count(stringvar) | An Axiom |
| disj-115 | ⊦ Mailbox(cmd) ≠ User-ConfirmedRelease-count(stringvar) | An Axiom |
| disj-116 | ⊦ Mailbox(cmd) ≠ User-GetSingleSelection(stringvar) | An Axiom |
| disj-117 | ⊦ Mailbox(cmd) ≠ User-GetSingleSelections(stringvar) | An Axiom |
| disj-118 | ⊦ Mailbox(cmd) ≠ User-GetSingleSelection-count(stringvar) | An Axiom |
| disj-119 | ⊦ Mailbox(cmd) ≠ User-GetMultipleSelection(stringvar) | An Axiom |
| disj-120 | ⊦ Mailbox(cmd) ≠ User-GetMultipleSelections(stringvar) | An Axiom |
| disj-121 | ⊦ Mailbox(cmd) ≠ User-GetMultipleSelection-count(stringvar) | An Axiom |
| disj-122 | ⊦ Mailbox(cmd) ≠ User-GetInput(stringvar) | An Axiom |
| disj-123 | ⊦ Mailbox(cmd) ≠ User-GetInputs(stringvar) | An Axiom |
| disj-124 | ⊦ Mailbox(cmd) ≠ User-GetInput-count(stringvar) | An Axiom |
| disj-125 | ⊦ Mailbox(cmd) ≠ User-Confirm(stringvar) | An Axiom |
| disj-126 | ⊦ Mailbox(cmd) ≠ User-Confirms(stringvar) | An Axiom |
| disj-127 | ⊦ Mailbox(cmd) ≠ User-Confirm-count(stringvar) | An Axiom |
| disj-128 | ⊦ Mailbox(cmd) ≠ ReadSourceInputs(stringvar, stringvar0) | An Axiom |
| disj-129 | ⊦ Mailbox(cmd) ≠ ReadSourceCount(stringvar, stringvar0) | An Axiom |
| disj-130 | ⊦ declassify-count(stringvar) ≠ User-ConfirmRelease(stringvar0) | An Axiom |
| disj-131 | ⊦ declassify-count(stringvar) ≠ User-ConfirmReleases(stringvar0) | An Axiom |
| disj-132 | ⊦ declassify-count(stringvar) ≠ User-ConfirmRelease-count(stringvar0) | An Axiom |
| disj-133 | ⊦ declassify-count(stringvar) ≠ User-ConfirmedRelease-count(stringvar0) | An Axiom |
| disj-134 | ⊦ declassify-count(stringvar) ≠ User-GetSingleSelection(stringvar0) | An Axiom |
| disj-135 | ⊦ declassify-count(stringvar) ≠ User-GetSingleSelections(stringvar0) | An Axiom |
| disj-136 | ⊦ declassify-count(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-137 | ⊦ declassify-count(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-138 | ⊦ declassify-count(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-139 | ⊦ declassify-count(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-140 | ⊦ declassify-count(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-141 | ⊦ declassify-count(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-142 | ⊦ declassify-count(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-143 | ⊦ declassify-count(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-144 | ⊦ declassify-count(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-145 | ⊦ declassify-count(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-146 | ⊦ declassify-count(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-147 | ⊦ declassify-count(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-148 | ⊦ User-ConfirmRelease(stringvar) ≠ User-ConfirmReleases(stringvar0) | An Axiom |
| disj-149 | ⊦ User-ConfirmRelease(stringvar) ≠ User-ConfirmRelease-count(stringvar0) | An Axiom |
| disj-150 | ⊦ User-ConfirmRelease(stringvar) ≠ User-ConfirmedRelease-count(stringvar0) | An Axiom |
| disj-151 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetSingleSelection(stringvar0) | An Axiom |
| disj-152 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetSingleSelections(stringvar0) | An Axiom |
| disj-153 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-154 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-155 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-156 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-157 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-158 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-159 | ⊦ User-ConfirmRelease(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-160 | ⊦ User-ConfirmRelease(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-161 | ⊦ User-ConfirmRelease(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-162 | ⊦ User-ConfirmRelease(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-163 | ⊦ User-ConfirmRelease(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-164 | ⊦ User-ConfirmRelease(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-165 | ⊦ User-ConfirmReleases(stringvar) ≠ User-ConfirmRelease-count(stringvar0) | An Axiom |
| disj-166 | ⊦ User-ConfirmReleases(stringvar) ≠ User-ConfirmedRelease-count(stringvar0) | An Axiom |
| disj-167 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetSingleSelection(stringvar0) | An Axiom |
| disj-168 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetSingleSelections(stringvar0) | An Axiom |
| disj-169 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-170 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-171 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-172 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-173 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-174 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-175 | ⊦ User-ConfirmReleases(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-176 | ⊦ User-ConfirmReleases(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-177 | ⊦ User-ConfirmReleases(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-178 | ⊦ User-ConfirmReleases(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-179 | ⊦ User-ConfirmReleases(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-180 | ⊦ User-ConfirmReleases(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-181 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-ConfirmedRelease-count(stringvar0) | An Axiom |
| disj-182 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetSingleSelection(stringvar0) | An Axiom |
| disj-183 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetSingleSelections(stringvar0) | An Axiom |
| disj-184 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-185 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-186 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-187 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-188 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-189 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-190 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-191 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-192 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-193 | ⊦ User-ConfirmRelease-count(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-194 | ⊦ User-ConfirmRelease-count(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-195 | ⊦ User-ConfirmRelease-count(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-196 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetSingleSelection(stringvar0) | An Axiom |
| disj-197 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetSingleSelections(stringvar0) | An Axiom |
| disj-198 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-199 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-200 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-201 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-202 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-203 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-204 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-205 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-206 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-207 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-208 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-209 | ⊦ User-ConfirmedRelease-count(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-210 | ⊦ User-GetSingleSelection(stringvar) ≠ User-GetSingleSelections(stringvar0) | An Axiom |
| disj-211 | ⊦ User-GetSingleSelection(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-212 | ⊦ User-GetSingleSelection(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-213 | ⊦ User-GetSingleSelection(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-214 | ⊦ User-GetSingleSelection(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-215 | ⊦ User-GetSingleSelection(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-216 | ⊦ User-GetSingleSelection(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-217 | ⊦ User-GetSingleSelection(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-218 | ⊦ User-GetSingleSelection(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-219 | ⊦ User-GetSingleSelection(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-220 | ⊦ User-GetSingleSelection(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-221 | ⊦ User-GetSingleSelection(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-222 | ⊦ User-GetSingleSelection(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-223 | ⊦ User-GetSingleSelections(stringvar) ≠ User-GetSingleSelection-count(stringvar0) | An Axiom |
| disj-224 | ⊦ User-GetSingleSelections(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-225 | ⊦ User-GetSingleSelections(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-226 | ⊦ User-GetSingleSelections(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-227 | ⊦ User-GetSingleSelections(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-228 | ⊦ User-GetSingleSelections(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-229 | ⊦ User-GetSingleSelections(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-230 | ⊦ User-GetSingleSelections(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-231 | ⊦ User-GetSingleSelections(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-232 | ⊦ User-GetSingleSelections(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-233 | ⊦ User-GetSingleSelections(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-234 | ⊦ User-GetSingleSelections(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-235 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-GetMultipleSelection(stringvar0) | An Axiom |
| disj-236 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-237 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-238 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-239 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-240 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-241 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-242 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-243 | ⊦ User-GetSingleSelection-count(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-244 | ⊦ User-GetSingleSelection-count(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-245 | ⊦ User-GetSingleSelection-count(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-246 | ⊦ User-GetMultipleSelection(stringvar) ≠ User-GetMultipleSelections(stringvar0) | An Axiom |
| disj-247 | ⊦ User-GetMultipleSelection(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-248 | ⊦ User-GetMultipleSelection(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-249 | ⊦ User-GetMultipleSelection(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-250 | ⊦ User-GetMultipleSelection(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-251 | ⊦ User-GetMultipleSelection(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-252 | ⊦ User-GetMultipleSelection(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-253 | ⊦ User-GetMultipleSelection(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-254 | ⊦ User-GetMultipleSelection(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-255 | ⊦ User-GetMultipleSelection(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-256 | ⊦ User-GetMultipleSelections(stringvar) ≠ User-GetMultipleSelection-count(stringvar0) | An Axiom |
| disj-257 | ⊦ User-GetMultipleSelections(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-258 | ⊦ User-GetMultipleSelections(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-259 | ⊦ User-GetMultipleSelections(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-260 | ⊦ User-GetMultipleSelections(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-261 | ⊦ User-GetMultipleSelections(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-262 | ⊦ User-GetMultipleSelections(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-263 | ⊦ User-GetMultipleSelections(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-264 | ⊦ User-GetMultipleSelections(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-265 | ⊦ User-GetMultipleSelection-count(stringvar) ≠ User-GetInput(stringvar0) | An Axiom |
| disj-266 | ⊦ User-GetMultipleSelection-count(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-267 | ⊦ User-GetMultipleSelection-count(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-268 | ⊦ User-GetMultipleSelection-count(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-269 | ⊦ User-GetMultipleSelection-count(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-270 | ⊦ User-GetMultipleSelection-count(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-271 | ⊦ User-GetMultipleSelection-count(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-272 | ⊦ User-GetMultipleSelection-count(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-273 | ⊦ User-GetInput(stringvar) ≠ User-GetInputs(stringvar0) | An Axiom |
| disj-274 | ⊦ User-GetInput(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-275 | ⊦ User-GetInput(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-276 | ⊦ User-GetInput(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-277 | ⊦ User-GetInput(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-278 | ⊦ User-GetInput(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-279 | ⊦ User-GetInput(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-280 | ⊦ User-GetInputs(stringvar) ≠ User-GetInput-count(stringvar0) | An Axiom |
| disj-281 | ⊦ User-GetInputs(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-282 | ⊦ User-GetInputs(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-283 | ⊦ User-GetInputs(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-284 | ⊦ User-GetInputs(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-285 | ⊦ User-GetInputs(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-286 | ⊦ User-GetInput-count(stringvar) ≠ User-Confirm(stringvar0) | An Axiom |
| disj-287 | ⊦ User-GetInput-count(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-288 | ⊦ User-GetInput-count(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-289 | ⊦ User-GetInput-count(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-290 | ⊦ User-GetInput-count(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-291 | ⊦ User-Confirm(stringvar) ≠ User-Confirms(stringvar0) | An Axiom |
| disj-292 | ⊦ User-Confirm(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-293 | ⊦ User-Confirm(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-294 | ⊦ User-Confirm(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-295 | ⊦ User-Confirms(stringvar) ≠ User-Confirm-count(stringvar0) | An Axiom |
| disj-296 | ⊦ User-Confirms(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-297 | ⊦ User-Confirms(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-298 | ⊦ User-Confirm-count(stringvar) ≠ ReadSourceInputs(stringvar0, stringvar1) | An Axiom |
| disj-299 | ⊦ User-Confirm-count(stringvar) ≠ ReadSourceCount(stringvar0, stringvar1) | An Axiom |
| disj-300 | ⊦ ReadSourceInputs(stringvar, stringvar0) ≠ ReadSourceCount(stringvar1, stringvar2) | An Axiom |
| sel-01 | ⊦ ReadSourceCount(stringvar, stringvar0) .call = stringvar0 | An Axiom |
| sel-02 | ⊦ ReadSourceCount(stringvar, stringvar0) .methodname = stringvar | An Axiom |
| sel-03 | ⊦ ReadSourceInputs(stringvar, stringvar0) .call = stringvar0 | An Axiom |
| sel-04 | ⊦ ReadSourceInputs(stringvar, stringvar0) .methodname = stringvar | An Axiom |
| sel-05 | ⊦ User-Confirm-count(stringvar) .name = stringvar | An Axiom |
| sel-06 | ⊦ User-Confirms(stringvar) .name = stringvar | An Axiom |
| sel-07 | ⊦ User-Confirm(stringvar) .name = stringvar | An Axiom |
| sel-08 | ⊦ User-GetInput-count(stringvar) .name = stringvar | An Axiom |
| sel-09 | ⊦ User-GetInputs(stringvar) .name = stringvar | An Axiom |
| sel-10 | ⊦ User-GetInput(stringvar) .name = stringvar | An Axiom |
| sel-11 | ⊦ User-GetMultipleSelection-count(stringvar) .name = stringvar | An Axiom |
| sel-12 | ⊦ User-GetMultipleSelections(stringvar) .name = stringvar | An Axiom |
| sel-13 | ⊦ User-GetMultipleSelection(stringvar) .name = stringvar | An Axiom |
| sel-14 | ⊦ User-GetSingleSelection-count(stringvar) .name = stringvar | An Axiom |
| sel-15 | ⊦ User-GetSingleSelections(stringvar) .name = stringvar | An Axiom |
| sel-16 | ⊦ User-GetSingleSelection(stringvar) .name = stringvar | An Axiom |
| sel-17 | ⊦ User-ConfirmedRelease-count(stringvar) .name = stringvar | An Axiom |
| sel-18 | ⊦ User-ConfirmRelease-count(stringvar) .name = stringvar | An Axiom |
| sel-19 | ⊦ User-ConfirmReleases(stringvar) .name = stringvar | An Axiom |
| sel-20 | ⊦ User-ConfirmRelease(stringvar) .name = stringvar | An Axiom |
| sel-21 | ⊦ declassify-count(stringvar) .name = stringvar | An Axiom |
| sel-22 | ⊦ Mailbox(cmd) .cmd = cmd | An Axiom |
| sel-23 | ⊦ state(stringvar) .name = stringvar | An Axiom |
| sel-24 | ⊦ locVar(stringvar) .name = stringvar | An Axiom |
| test-01 | ⊦ isReadSourceCount(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-02 | ⊦ ¬ isReadSourceCount(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-03 | ⊦ ¬ isReadSourceCount(User-Confirm-count(stringvar)) | An Axiom |
| test-04 | ⊦ ¬ isReadSourceCount(User-Confirms(stringvar)) | An Axiom |
| test-05 | ⊦ ¬ isReadSourceCount(User-Confirm(stringvar)) | An Axiom |
| test-06 | ⊦ ¬ isReadSourceCount(User-GetInput-count(stringvar)) | An Axiom |
| test-07 | ⊦ ¬ isReadSourceCount(User-GetInputs(stringvar)) | An Axiom |
| test-08 | ⊦ ¬ isReadSourceCount(User-GetInput(stringvar)) | An Axiom |
| test-09 | ⊦ ¬ isReadSourceCount(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-10 | ⊦ ¬ isReadSourceCount(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-11 | ⊦ ¬ isReadSourceCount(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-12 | ⊦ ¬ isReadSourceCount(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-13 | ⊦ ¬ isReadSourceCount(User-GetSingleSelections(stringvar)) | An Axiom |
| test-14 | ⊦ ¬ isReadSourceCount(User-GetSingleSelection(stringvar)) | An Axiom |
| test-15 | ⊦ ¬ isReadSourceCount(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-16 | ⊦ ¬ isReadSourceCount(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-17 | ⊦ ¬ isReadSourceCount(User-ConfirmReleases(stringvar)) | An Axiom |
| test-18 | ⊦ ¬ isReadSourceCount(User-ConfirmRelease(stringvar)) | An Axiom |
| test-19 | ⊦ ¬ isReadSourceCount(declassify-count(stringvar)) | An Axiom |
| test-20 | ⊦ ¬ isReadSourceCount(Mailbox(cmd)) | An Axiom |
| test-21 | ⊦ ¬ isReadSourceCount(state(stringvar)) | An Axiom |
| test-22 | ⊦ ¬ isReadSourceCount(locVar(stringvar)) | An Axiom |
| test-23 | ⊦ ¬ isReadSourceCount(TravelPlanner-flightOffer) | An Axiom |
| test-24 | ⊦ ¬ isReadSourceCount(CreditCardCenter-ccd) | An Axiom |
| test-25 | ⊦ ¬ isReadSourceCount(Airline-flightOffers) | An Axiom |
| test-26 | ⊦ ¬ isReadSourceInputs(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-27 | ⊦ isReadSourceInputs(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-28 | ⊦ ¬ isReadSourceInputs(User-Confirm-count(stringvar)) | An Axiom |
| test-29 | ⊦ ¬ isReadSourceInputs(User-Confirms(stringvar)) | An Axiom |
| test-30 | ⊦ ¬ isReadSourceInputs(User-Confirm(stringvar)) | An Axiom |
| test-31 | ⊦ ¬ isReadSourceInputs(User-GetInput-count(stringvar)) | An Axiom |
| test-32 | ⊦ ¬ isReadSourceInputs(User-GetInputs(stringvar)) | An Axiom |
| test-33 | ⊦ ¬ isReadSourceInputs(User-GetInput(stringvar)) | An Axiom |
| test-34 | ⊦ ¬ isReadSourceInputs(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-35 | ⊦ ¬ isReadSourceInputs(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-36 | ⊦ ¬ isReadSourceInputs(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-37 | ⊦ ¬ isReadSourceInputs(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-38 | ⊦ ¬ isReadSourceInputs(User-GetSingleSelections(stringvar)) | An Axiom |
| test-39 | ⊦ ¬ isReadSourceInputs(User-GetSingleSelection(stringvar)) | An Axiom |
| test-40 | ⊦ ¬ isReadSourceInputs(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-41 | ⊦ ¬ isReadSourceInputs(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-42 | ⊦ ¬ isReadSourceInputs(User-ConfirmReleases(stringvar)) | An Axiom |
| test-43 | ⊦ ¬ isReadSourceInputs(User-ConfirmRelease(stringvar)) | An Axiom |
| test-44 | ⊦ ¬ isReadSourceInputs(declassify-count(stringvar)) | An Axiom |
| test-45 | ⊦ ¬ isReadSourceInputs(Mailbox(cmd)) | An Axiom |
| test-46 | ⊦ ¬ isReadSourceInputs(state(stringvar)) | An Axiom |
| test-47 | ⊦ ¬ isReadSourceInputs(locVar(stringvar)) | An Axiom |
| test-48 | ⊦ ¬ isReadSourceInputs(TravelPlanner-flightOffer) | An Axiom |
| test-49 | ⊦ ¬ isReadSourceInputs(CreditCardCenter-ccd) | An Axiom |
| test-50 | ⊦ ¬ isReadSourceInputs(Airline-flightOffers) | An Axiom |
| test-51 | ⊦ ¬ isUser-Confirm-count(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-52 | ⊦ ¬ isUser-Confirm-count(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-53 | ⊦ isUser-Confirm-count(User-Confirm-count(stringvar)) | An Axiom |
| test-54 | ⊦ ¬ isUser-Confirm-count(User-Confirms(stringvar)) | An Axiom |
| test-55 | ⊦ ¬ isUser-Confirm-count(User-Confirm(stringvar)) | An Axiom |
| test-56 | ⊦ ¬ isUser-Confirm-count(User-GetInput-count(stringvar)) | An Axiom |
| test-57 | ⊦ ¬ isUser-Confirm-count(User-GetInputs(stringvar)) | An Axiom |
| test-58 | ⊦ ¬ isUser-Confirm-count(User-GetInput(stringvar)) | An Axiom |
| test-59 | ⊦ ¬ isUser-Confirm-count(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-60 | ⊦ ¬ isUser-Confirm-count(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-61 | ⊦ ¬ isUser-Confirm-count(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-62 | ⊦ ¬ isUser-Confirm-count(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-63 | ⊦ ¬ isUser-Confirm-count(User-GetSingleSelections(stringvar)) | An Axiom |
| test-64 | ⊦ ¬ isUser-Confirm-count(User-GetSingleSelection(stringvar)) | An Axiom |
| test-65 | ⊦ ¬ isUser-Confirm-count(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-66 | ⊦ ¬ isUser-Confirm-count(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-67 | ⊦ ¬ isUser-Confirm-count(User-ConfirmReleases(stringvar)) | An Axiom |
| test-68 | ⊦ ¬ isUser-Confirm-count(User-ConfirmRelease(stringvar)) | An Axiom |
| test-69 | ⊦ ¬ isUser-Confirm-count(declassify-count(stringvar)) | An Axiom |
| test-70 | ⊦ ¬ isUser-Confirm-count(Mailbox(cmd)) | An Axiom |
| test-71 | ⊦ ¬ isUser-Confirm-count(state(stringvar)) | An Axiom |
| test-72 | ⊦ ¬ isUser-Confirm-count(locVar(stringvar)) | An Axiom |
| test-73 | ⊦ ¬ isUser-Confirm-count(TravelPlanner-flightOffer) | An Axiom |
| test-74 | ⊦ ¬ isUser-Confirm-count(CreditCardCenter-ccd) | An Axiom |
| test-75 | ⊦ ¬ isUser-Confirm-count(Airline-flightOffers) | An Axiom |
| test-76 | ⊦ ¬ isUser-Confirms(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-77 | ⊦ ¬ isUser-Confirms(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-78 | ⊦ ¬ isUser-Confirms(User-Confirm-count(stringvar)) | An Axiom |
| test-79 | ⊦ isUser-Confirms(User-Confirms(stringvar)) | An Axiom |
| test-80 | ⊦ ¬ isUser-Confirms(User-Confirm(stringvar)) | An Axiom |
| test-81 | ⊦ ¬ isUser-Confirms(User-GetInput-count(stringvar)) | An Axiom |
| test-82 | ⊦ ¬ isUser-Confirms(User-GetInputs(stringvar)) | An Axiom |
| test-83 | ⊦ ¬ isUser-Confirms(User-GetInput(stringvar)) | An Axiom |
| test-84 | ⊦ ¬ isUser-Confirms(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-85 | ⊦ ¬ isUser-Confirms(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-86 | ⊦ ¬ isUser-Confirms(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-87 | ⊦ ¬ isUser-Confirms(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-88 | ⊦ ¬ isUser-Confirms(User-GetSingleSelections(stringvar)) | An Axiom |
| test-89 | ⊦ ¬ isUser-Confirms(User-GetSingleSelection(stringvar)) | An Axiom |
| test-90 | ⊦ ¬ isUser-Confirms(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-91 | ⊦ ¬ isUser-Confirms(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-92 | ⊦ ¬ isUser-Confirms(User-ConfirmReleases(stringvar)) | An Axiom |
| test-93 | ⊦ ¬ isUser-Confirms(User-ConfirmRelease(stringvar)) | An Axiom |
| test-94 | ⊦ ¬ isUser-Confirms(declassify-count(stringvar)) | An Axiom |
| test-95 | ⊦ ¬ isUser-Confirms(Mailbox(cmd)) | An Axiom |
| test-96 | ⊦ ¬ isUser-Confirms(state(stringvar)) | An Axiom |
| test-97 | ⊦ ¬ isUser-Confirms(locVar(stringvar)) | An Axiom |
| test-98 | ⊦ ¬ isUser-Confirms(TravelPlanner-flightOffer) | An Axiom |
| test-99 | ⊦ ¬ isUser-Confirms(CreditCardCenter-ccd) | An Axiom |
| test-100 | ⊦ ¬ isUser-Confirms(Airline-flightOffers) | An Axiom |
| test-101 | ⊦ ¬ isUser-Confirm(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-102 | ⊦ ¬ isUser-Confirm(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-103 | ⊦ ¬ isUser-Confirm(User-Confirm-count(stringvar)) | An Axiom |
| test-104 | ⊦ ¬ isUser-Confirm(User-Confirms(stringvar)) | An Axiom |
| test-105 | ⊦ isUser-Confirm(User-Confirm(stringvar)) | An Axiom |
| test-106 | ⊦ ¬ isUser-Confirm(User-GetInput-count(stringvar)) | An Axiom |
| test-107 | ⊦ ¬ isUser-Confirm(User-GetInputs(stringvar)) | An Axiom |
| test-108 | ⊦ ¬ isUser-Confirm(User-GetInput(stringvar)) | An Axiom |
| test-109 | ⊦ ¬ isUser-Confirm(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-110 | ⊦ ¬ isUser-Confirm(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-111 | ⊦ ¬ isUser-Confirm(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-112 | ⊦ ¬ isUser-Confirm(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-113 | ⊦ ¬ isUser-Confirm(User-GetSingleSelections(stringvar)) | An Axiom |
| test-114 | ⊦ ¬ isUser-Confirm(User-GetSingleSelection(stringvar)) | An Axiom |
| test-115 | ⊦ ¬ isUser-Confirm(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-116 | ⊦ ¬ isUser-Confirm(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-117 | ⊦ ¬ isUser-Confirm(User-ConfirmReleases(stringvar)) | An Axiom |
| test-118 | ⊦ ¬ isUser-Confirm(User-ConfirmRelease(stringvar)) | An Axiom |
| test-119 | ⊦ ¬ isUser-Confirm(declassify-count(stringvar)) | An Axiom |
| test-120 | ⊦ ¬ isUser-Confirm(Mailbox(cmd)) | An Axiom |
| test-121 | ⊦ ¬ isUser-Confirm(state(stringvar)) | An Axiom |
| test-122 | ⊦ ¬ isUser-Confirm(locVar(stringvar)) | An Axiom |
| test-123 | ⊦ ¬ isUser-Confirm(TravelPlanner-flightOffer) | An Axiom |
| test-124 | ⊦ ¬ isUser-Confirm(CreditCardCenter-ccd) | An Axiom |
| test-125 | ⊦ ¬ isUser-Confirm(Airline-flightOffers) | An Axiom |
| test-126 | ⊦ ¬ isUser-GetInput-count(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-127 | ⊦ ¬ isUser-GetInput-count(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-128 | ⊦ ¬ isUser-GetInput-count(User-Confirm-count(stringvar)) | An Axiom |
| test-129 | ⊦ ¬ isUser-GetInput-count(User-Confirms(stringvar)) | An Axiom |
| test-130 | ⊦ ¬ isUser-GetInput-count(User-Confirm(stringvar)) | An Axiom |
| test-131 | ⊦ isUser-GetInput-count(User-GetInput-count(stringvar)) | An Axiom |
| test-132 | ⊦ ¬ isUser-GetInput-count(User-GetInputs(stringvar)) | An Axiom |
| test-133 | ⊦ ¬ isUser-GetInput-count(User-GetInput(stringvar)) | An Axiom |
| test-134 | ⊦ ¬ isUser-GetInput-count(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-135 | ⊦ ¬ isUser-GetInput-count(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-136 | ⊦ ¬ isUser-GetInput-count(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-137 | ⊦ ¬ isUser-GetInput-count(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-138 | ⊦ ¬ isUser-GetInput-count(User-GetSingleSelections(stringvar)) | An Axiom |
| test-139 | ⊦ ¬ isUser-GetInput-count(User-GetSingleSelection(stringvar)) | An Axiom |
| test-140 | ⊦ ¬ isUser-GetInput-count(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-141 | ⊦ ¬ isUser-GetInput-count(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-142 | ⊦ ¬ isUser-GetInput-count(User-ConfirmReleases(stringvar)) | An Axiom |
| test-143 | ⊦ ¬ isUser-GetInput-count(User-ConfirmRelease(stringvar)) | An Axiom |
| test-144 | ⊦ ¬ isUser-GetInput-count(declassify-count(stringvar)) | An Axiom |
| test-145 | ⊦ ¬ isUser-GetInput-count(Mailbox(cmd)) | An Axiom |
| test-146 | ⊦ ¬ isUser-GetInput-count(state(stringvar)) | An Axiom |
| test-147 | ⊦ ¬ isUser-GetInput-count(locVar(stringvar)) | An Axiom |
| test-148 | ⊦ ¬ isUser-GetInput-count(TravelPlanner-flightOffer) | An Axiom |
| test-149 | ⊦ ¬ isUser-GetInput-count(CreditCardCenter-ccd) | An Axiom |
| test-150 | ⊦ ¬ isUser-GetInput-count(Airline-flightOffers) | An Axiom |
| test-151 | ⊦ ¬ isUser-GetInputs(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-152 | ⊦ ¬ isUser-GetInputs(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-153 | ⊦ ¬ isUser-GetInputs(User-Confirm-count(stringvar)) | An Axiom |
| test-154 | ⊦ ¬ isUser-GetInputs(User-Confirms(stringvar)) | An Axiom |
| test-155 | ⊦ ¬ isUser-GetInputs(User-Confirm(stringvar)) | An Axiom |
| test-156 | ⊦ ¬ isUser-GetInputs(User-GetInput-count(stringvar)) | An Axiom |
| test-157 | ⊦ isUser-GetInputs(User-GetInputs(stringvar)) | An Axiom |
| test-158 | ⊦ ¬ isUser-GetInputs(User-GetInput(stringvar)) | An Axiom |
| test-159 | ⊦ ¬ isUser-GetInputs(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-160 | ⊦ ¬ isUser-GetInputs(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-161 | ⊦ ¬ isUser-GetInputs(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-162 | ⊦ ¬ isUser-GetInputs(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-163 | ⊦ ¬ isUser-GetInputs(User-GetSingleSelections(stringvar)) | An Axiom |
| test-164 | ⊦ ¬ isUser-GetInputs(User-GetSingleSelection(stringvar)) | An Axiom |
| test-165 | ⊦ ¬ isUser-GetInputs(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-166 | ⊦ ¬ isUser-GetInputs(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-167 | ⊦ ¬ isUser-GetInputs(User-ConfirmReleases(stringvar)) | An Axiom |
| test-168 | ⊦ ¬ isUser-GetInputs(User-ConfirmRelease(stringvar)) | An Axiom |
| test-169 | ⊦ ¬ isUser-GetInputs(declassify-count(stringvar)) | An Axiom |
| test-170 | ⊦ ¬ isUser-GetInputs(Mailbox(cmd)) | An Axiom |
| test-171 | ⊦ ¬ isUser-GetInputs(state(stringvar)) | An Axiom |
| test-172 | ⊦ ¬ isUser-GetInputs(locVar(stringvar)) | An Axiom |
| test-173 | ⊦ ¬ isUser-GetInputs(TravelPlanner-flightOffer) | An Axiom |
| test-174 | ⊦ ¬ isUser-GetInputs(CreditCardCenter-ccd) | An Axiom |
| test-175 | ⊦ ¬ isUser-GetInputs(Airline-flightOffers) | An Axiom |
| test-176 | ⊦ ¬ isUser-GetInput(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-177 | ⊦ ¬ isUser-GetInput(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-178 | ⊦ ¬ isUser-GetInput(User-Confirm-count(stringvar)) | An Axiom |
| test-179 | ⊦ ¬ isUser-GetInput(User-Confirms(stringvar)) | An Axiom |
| test-180 | ⊦ ¬ isUser-GetInput(User-Confirm(stringvar)) | An Axiom |
| test-181 | ⊦ ¬ isUser-GetInput(User-GetInput-count(stringvar)) | An Axiom |
| test-182 | ⊦ ¬ isUser-GetInput(User-GetInputs(stringvar)) | An Axiom |
| test-183 | ⊦ isUser-GetInput(User-GetInput(stringvar)) | An Axiom |
| test-184 | ⊦ ¬ isUser-GetInput(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-185 | ⊦ ¬ isUser-GetInput(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-186 | ⊦ ¬ isUser-GetInput(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-187 | ⊦ ¬ isUser-GetInput(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-188 | ⊦ ¬ isUser-GetInput(User-GetSingleSelections(stringvar)) | An Axiom |
| test-189 | ⊦ ¬ isUser-GetInput(User-GetSingleSelection(stringvar)) | An Axiom |
| test-190 | ⊦ ¬ isUser-GetInput(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-191 | ⊦ ¬ isUser-GetInput(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-192 | ⊦ ¬ isUser-GetInput(User-ConfirmReleases(stringvar)) | An Axiom |
| test-193 | ⊦ ¬ isUser-GetInput(User-ConfirmRelease(stringvar)) | An Axiom |
| test-194 | ⊦ ¬ isUser-GetInput(declassify-count(stringvar)) | An Axiom |
| test-195 | ⊦ ¬ isUser-GetInput(Mailbox(cmd)) | An Axiom |
| test-196 | ⊦ ¬ isUser-GetInput(state(stringvar)) | An Axiom |
| test-197 | ⊦ ¬ isUser-GetInput(locVar(stringvar)) | An Axiom |
| test-198 | ⊦ ¬ isUser-GetInput(TravelPlanner-flightOffer) | An Axiom |
| test-199 | ⊦ ¬ isUser-GetInput(CreditCardCenter-ccd) | An Axiom |
| test-200 | ⊦ ¬ isUser-GetInput(Airline-flightOffers) | An Axiom |
| test-201 | ⊦ ¬ isUser-GetMultipleSelection-count(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-202 | ⊦ ¬ isUser-GetMultipleSelection-count(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-203 | ⊦ ¬ isUser-GetMultipleSelection-count(User-Confirm-count(stringvar)) | An Axiom |
| test-204 | ⊦ ¬ isUser-GetMultipleSelection-count(User-Confirms(stringvar)) | An Axiom |
| test-205 | ⊦ ¬ isUser-GetMultipleSelection-count(User-Confirm(stringvar)) | An Axiom |
| test-206 | ⊦ ¬ isUser-GetMultipleSelection-count(User-GetInput-count(stringvar)) | An Axiom |
| test-207 | ⊦ ¬ isUser-GetMultipleSelection-count(User-GetInputs(stringvar)) | An Axiom |
| test-208 | ⊦ ¬ isUser-GetMultipleSelection-count(User-GetInput(stringvar)) | An Axiom |
| test-209 | ⊦ isUser-GetMultipleSelection-count(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-210 | ⊦ ¬ isUser-GetMultipleSelection-count(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-211 | ⊦ ¬ isUser-GetMultipleSelection-count(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-212 | ⊦ ¬ isUser-GetMultipleSelection-count(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-213 | ⊦ ¬ isUser-GetMultipleSelection-count(User-GetSingleSelections(stringvar)) | An Axiom |
| test-214 | ⊦ ¬ isUser-GetMultipleSelection-count(User-GetSingleSelection(stringvar)) | An Axiom |
| test-215 | ⊦ ¬ isUser-GetMultipleSelection-count(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-216 | ⊦ ¬ isUser-GetMultipleSelection-count(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-217 | ⊦ ¬ isUser-GetMultipleSelection-count(User-ConfirmReleases(stringvar)) | An Axiom |
| test-218 | ⊦ ¬ isUser-GetMultipleSelection-count(User-ConfirmRelease(stringvar)) | An Axiom |
| test-219 | ⊦ ¬ isUser-GetMultipleSelection-count(declassify-count(stringvar)) | An Axiom |
| test-220 | ⊦ ¬ isUser-GetMultipleSelection-count(Mailbox(cmd)) | An Axiom |
| test-221 | ⊦ ¬ isUser-GetMultipleSelection-count(state(stringvar)) | An Axiom |
| test-222 | ⊦ ¬ isUser-GetMultipleSelection-count(locVar(stringvar)) | An Axiom |
| test-223 | ⊦ ¬ isUser-GetMultipleSelection-count(TravelPlanner-flightOffer) | An Axiom |
| test-224 | ⊦ ¬ isUser-GetMultipleSelection-count(CreditCardCenter-ccd) | An Axiom |
| test-225 | ⊦ ¬ isUser-GetMultipleSelection-count(Airline-flightOffers) | An Axiom |
| test-226 | ⊦ ¬ isUser-GetMultipleSelections(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-227 | ⊦ ¬ isUser-GetMultipleSelections(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-228 | ⊦ ¬ isUser-GetMultipleSelections(User-Confirm-count(stringvar)) | An Axiom |
| test-229 | ⊦ ¬ isUser-GetMultipleSelections(User-Confirms(stringvar)) | An Axiom |
| test-230 | ⊦ ¬ isUser-GetMultipleSelections(User-Confirm(stringvar)) | An Axiom |
| test-231 | ⊦ ¬ isUser-GetMultipleSelections(User-GetInput-count(stringvar)) | An Axiom |
| test-232 | ⊦ ¬ isUser-GetMultipleSelections(User-GetInputs(stringvar)) | An Axiom |
| test-233 | ⊦ ¬ isUser-GetMultipleSelections(User-GetInput(stringvar)) | An Axiom |
| test-234 | ⊦ ¬ isUser-GetMultipleSelections(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-235 | ⊦ isUser-GetMultipleSelections(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-236 | ⊦ ¬ isUser-GetMultipleSelections(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-237 | ⊦ ¬ isUser-GetMultipleSelections(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-238 | ⊦ ¬ isUser-GetMultipleSelections(User-GetSingleSelections(stringvar)) | An Axiom |
| test-239 | ⊦ ¬ isUser-GetMultipleSelections(User-GetSingleSelection(stringvar)) | An Axiom |
| test-240 | ⊦ ¬ isUser-GetMultipleSelections(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-241 | ⊦ ¬ isUser-GetMultipleSelections(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-242 | ⊦ ¬ isUser-GetMultipleSelections(User-ConfirmReleases(stringvar)) | An Axiom |
| test-243 | ⊦ ¬ isUser-GetMultipleSelections(User-ConfirmRelease(stringvar)) | An Axiom |
| test-244 | ⊦ ¬ isUser-GetMultipleSelections(declassify-count(stringvar)) | An Axiom |
| test-245 | ⊦ ¬ isUser-GetMultipleSelections(Mailbox(cmd)) | An Axiom |
| test-246 | ⊦ ¬ isUser-GetMultipleSelections(state(stringvar)) | An Axiom |
| test-247 | ⊦ ¬ isUser-GetMultipleSelections(locVar(stringvar)) | An Axiom |
| test-248 | ⊦ ¬ isUser-GetMultipleSelections(TravelPlanner-flightOffer) | An Axiom |
| test-249 | ⊦ ¬ isUser-GetMultipleSelections(CreditCardCenter-ccd) | An Axiom |
| test-250 | ⊦ ¬ isUser-GetMultipleSelections(Airline-flightOffers) | An Axiom |
| test-251 | ⊦ ¬ isUser-GetMultipleSelection(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-252 | ⊦ ¬ isUser-GetMultipleSelection(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-253 | ⊦ ¬ isUser-GetMultipleSelection(User-Confirm-count(stringvar)) | An Axiom |
| test-254 | ⊦ ¬ isUser-GetMultipleSelection(User-Confirms(stringvar)) | An Axiom |
| test-255 | ⊦ ¬ isUser-GetMultipleSelection(User-Confirm(stringvar)) | An Axiom |
| test-256 | ⊦ ¬ isUser-GetMultipleSelection(User-GetInput-count(stringvar)) | An Axiom |
| test-257 | ⊦ ¬ isUser-GetMultipleSelection(User-GetInputs(stringvar)) | An Axiom |
| test-258 | ⊦ ¬ isUser-GetMultipleSelection(User-GetInput(stringvar)) | An Axiom |
| test-259 | ⊦ ¬ isUser-GetMultipleSelection(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-260 | ⊦ ¬ isUser-GetMultipleSelection(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-261 | ⊦ isUser-GetMultipleSelection(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-262 | ⊦ ¬ isUser-GetMultipleSelection(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-263 | ⊦ ¬ isUser-GetMultipleSelection(User-GetSingleSelections(stringvar)) | An Axiom |
| test-264 | ⊦ ¬ isUser-GetMultipleSelection(User-GetSingleSelection(stringvar)) | An Axiom |
| test-265 | ⊦ ¬ isUser-GetMultipleSelection(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-266 | ⊦ ¬ isUser-GetMultipleSelection(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-267 | ⊦ ¬ isUser-GetMultipleSelection(User-ConfirmReleases(stringvar)) | An Axiom |
| test-268 | ⊦ ¬ isUser-GetMultipleSelection(User-ConfirmRelease(stringvar)) | An Axiom |
| test-269 | ⊦ ¬ isUser-GetMultipleSelection(declassify-count(stringvar)) | An Axiom |
| test-270 | ⊦ ¬ isUser-GetMultipleSelection(Mailbox(cmd)) | An Axiom |
| test-271 | ⊦ ¬ isUser-GetMultipleSelection(state(stringvar)) | An Axiom |
| test-272 | ⊦ ¬ isUser-GetMultipleSelection(locVar(stringvar)) | An Axiom |
| test-273 | ⊦ ¬ isUser-GetMultipleSelection(TravelPlanner-flightOffer) | An Axiom |
| test-274 | ⊦ ¬ isUser-GetMultipleSelection(CreditCardCenter-ccd) | An Axiom |
| test-275 | ⊦ ¬ isUser-GetMultipleSelection(Airline-flightOffers) | An Axiom |
| test-276 | ⊦ ¬ isUser-GetSingleSelection-count(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-277 | ⊦ ¬ isUser-GetSingleSelection-count(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-278 | ⊦ ¬ isUser-GetSingleSelection-count(User-Confirm-count(stringvar)) | An Axiom |
| test-279 | ⊦ ¬ isUser-GetSingleSelection-count(User-Confirms(stringvar)) | An Axiom |
| test-280 | ⊦ ¬ isUser-GetSingleSelection-count(User-Confirm(stringvar)) | An Axiom |
| test-281 | ⊦ ¬ isUser-GetSingleSelection-count(User-GetInput-count(stringvar)) | An Axiom |
| test-282 | ⊦ ¬ isUser-GetSingleSelection-count(User-GetInputs(stringvar)) | An Axiom |
| test-283 | ⊦ ¬ isUser-GetSingleSelection-count(User-GetInput(stringvar)) | An Axiom |
| test-284 | ⊦ ¬ isUser-GetSingleSelection-count(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-285 | ⊦ ¬ isUser-GetSingleSelection-count(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-286 | ⊦ ¬ isUser-GetSingleSelection-count(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-287 | ⊦ isUser-GetSingleSelection-count(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-288 | ⊦ ¬ isUser-GetSingleSelection-count(User-GetSingleSelections(stringvar)) | An Axiom |
| test-289 | ⊦ ¬ isUser-GetSingleSelection-count(User-GetSingleSelection(stringvar)) | An Axiom |
| test-290 | ⊦ ¬ isUser-GetSingleSelection-count(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-291 | ⊦ ¬ isUser-GetSingleSelection-count(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-292 | ⊦ ¬ isUser-GetSingleSelection-count(User-ConfirmReleases(stringvar)) | An Axiom |
| test-293 | ⊦ ¬ isUser-GetSingleSelection-count(User-ConfirmRelease(stringvar)) | An Axiom |
| test-294 | ⊦ ¬ isUser-GetSingleSelection-count(declassify-count(stringvar)) | An Axiom |
| test-295 | ⊦ ¬ isUser-GetSingleSelection-count(Mailbox(cmd)) | An Axiom |
| test-296 | ⊦ ¬ isUser-GetSingleSelection-count(state(stringvar)) | An Axiom |
| test-297 | ⊦ ¬ isUser-GetSingleSelection-count(locVar(stringvar)) | An Axiom |
| test-298 | ⊦ ¬ isUser-GetSingleSelection-count(TravelPlanner-flightOffer) | An Axiom |
| test-299 | ⊦ ¬ isUser-GetSingleSelection-count(CreditCardCenter-ccd) | An Axiom |
| test-300 | ⊦ ¬ isUser-GetSingleSelection-count(Airline-flightOffers) | An Axiom |
| test-301 | ⊦ ¬ isUser-GetSingleSelections(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-302 | ⊦ ¬ isUser-GetSingleSelections(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-303 | ⊦ ¬ isUser-GetSingleSelections(User-Confirm-count(stringvar)) | An Axiom |
| test-304 | ⊦ ¬ isUser-GetSingleSelections(User-Confirms(stringvar)) | An Axiom |
| test-305 | ⊦ ¬ isUser-GetSingleSelections(User-Confirm(stringvar)) | An Axiom |
| test-306 | ⊦ ¬ isUser-GetSingleSelections(User-GetInput-count(stringvar)) | An Axiom |
| test-307 | ⊦ ¬ isUser-GetSingleSelections(User-GetInputs(stringvar)) | An Axiom |
| test-308 | ⊦ ¬ isUser-GetSingleSelections(User-GetInput(stringvar)) | An Axiom |
| test-309 | ⊦ ¬ isUser-GetSingleSelections(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-310 | ⊦ ¬ isUser-GetSingleSelections(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-311 | ⊦ ¬ isUser-GetSingleSelections(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-312 | ⊦ ¬ isUser-GetSingleSelections(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-313 | ⊦ isUser-GetSingleSelections(User-GetSingleSelections(stringvar)) | An Axiom |
| test-314 | ⊦ ¬ isUser-GetSingleSelections(User-GetSingleSelection(stringvar)) | An Axiom |
| test-315 | ⊦ ¬ isUser-GetSingleSelections(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-316 | ⊦ ¬ isUser-GetSingleSelections(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-317 | ⊦ ¬ isUser-GetSingleSelections(User-ConfirmReleases(stringvar)) | An Axiom |
| test-318 | ⊦ ¬ isUser-GetSingleSelections(User-ConfirmRelease(stringvar)) | An Axiom |
| test-319 | ⊦ ¬ isUser-GetSingleSelections(declassify-count(stringvar)) | An Axiom |
| test-320 | ⊦ ¬ isUser-GetSingleSelections(Mailbox(cmd)) | An Axiom |
| test-321 | ⊦ ¬ isUser-GetSingleSelections(state(stringvar)) | An Axiom |
| test-322 | ⊦ ¬ isUser-GetSingleSelections(locVar(stringvar)) | An Axiom |
| test-323 | ⊦ ¬ isUser-GetSingleSelections(TravelPlanner-flightOffer) | An Axiom |
| test-324 | ⊦ ¬ isUser-GetSingleSelections(CreditCardCenter-ccd) | An Axiom |
| test-325 | ⊦ ¬ isUser-GetSingleSelections(Airline-flightOffers) | An Axiom |
| test-326 | ⊦ ¬ isUser-GetSingleSelection(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-327 | ⊦ ¬ isUser-GetSingleSelection(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-328 | ⊦ ¬ isUser-GetSingleSelection(User-Confirm-count(stringvar)) | An Axiom |
| test-329 | ⊦ ¬ isUser-GetSingleSelection(User-Confirms(stringvar)) | An Axiom |
| test-330 | ⊦ ¬ isUser-GetSingleSelection(User-Confirm(stringvar)) | An Axiom |
| test-331 | ⊦ ¬ isUser-GetSingleSelection(User-GetInput-count(stringvar)) | An Axiom |
| test-332 | ⊦ ¬ isUser-GetSingleSelection(User-GetInputs(stringvar)) | An Axiom |
| test-333 | ⊦ ¬ isUser-GetSingleSelection(User-GetInput(stringvar)) | An Axiom |
| test-334 | ⊦ ¬ isUser-GetSingleSelection(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-335 | ⊦ ¬ isUser-GetSingleSelection(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-336 | ⊦ ¬ isUser-GetSingleSelection(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-337 | ⊦ ¬ isUser-GetSingleSelection(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-338 | ⊦ ¬ isUser-GetSingleSelection(User-GetSingleSelections(stringvar)) | An Axiom |
| test-339 | ⊦ isUser-GetSingleSelection(User-GetSingleSelection(stringvar)) | An Axiom |
| test-340 | ⊦ ¬ isUser-GetSingleSelection(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-341 | ⊦ ¬ isUser-GetSingleSelection(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-342 | ⊦ ¬ isUser-GetSingleSelection(User-ConfirmReleases(stringvar)) | An Axiom |
| test-343 | ⊦ ¬ isUser-GetSingleSelection(User-ConfirmRelease(stringvar)) | An Axiom |
| test-344 | ⊦ ¬ isUser-GetSingleSelection(declassify-count(stringvar)) | An Axiom |
| test-345 | ⊦ ¬ isUser-GetSingleSelection(Mailbox(cmd)) | An Axiom |
| test-346 | ⊦ ¬ isUser-GetSingleSelection(state(stringvar)) | An Axiom |
| test-347 | ⊦ ¬ isUser-GetSingleSelection(locVar(stringvar)) | An Axiom |
| test-348 | ⊦ ¬ isUser-GetSingleSelection(TravelPlanner-flightOffer) | An Axiom |
| test-349 | ⊦ ¬ isUser-GetSingleSelection(CreditCardCenter-ccd) | An Axiom |
| test-350 | ⊦ ¬ isUser-GetSingleSelection(Airline-flightOffers) | An Axiom |
| test-351 | ⊦ ¬ isUser-ConfirmedRelease-count(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-352 | ⊦ ¬ isUser-ConfirmedRelease-count(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-353 | ⊦ ¬ isUser-ConfirmedRelease-count(User-Confirm-count(stringvar)) | An Axiom |
| test-354 | ⊦ ¬ isUser-ConfirmedRelease-count(User-Confirms(stringvar)) | An Axiom |
| test-355 | ⊦ ¬ isUser-ConfirmedRelease-count(User-Confirm(stringvar)) | An Axiom |
| test-356 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetInput-count(stringvar)) | An Axiom |
| test-357 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetInputs(stringvar)) | An Axiom |
| test-358 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetInput(stringvar)) | An Axiom |
| test-359 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-360 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-361 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-362 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-363 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetSingleSelections(stringvar)) | An Axiom |
| test-364 | ⊦ ¬ isUser-ConfirmedRelease-count(User-GetSingleSelection(stringvar)) | An Axiom |
| test-365 | ⊦ isUser-ConfirmedRelease-count(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-366 | ⊦ ¬ isUser-ConfirmedRelease-count(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-367 | ⊦ ¬ isUser-ConfirmedRelease-count(User-ConfirmReleases(stringvar)) | An Axiom |
| test-368 | ⊦ ¬ isUser-ConfirmedRelease-count(User-ConfirmRelease(stringvar)) | An Axiom |
| test-369 | ⊦ ¬ isUser-ConfirmedRelease-count(declassify-count(stringvar)) | An Axiom |
| test-370 | ⊦ ¬ isUser-ConfirmedRelease-count(Mailbox(cmd)) | An Axiom |
| test-371 | ⊦ ¬ isUser-ConfirmedRelease-count(state(stringvar)) | An Axiom |
| test-372 | ⊦ ¬ isUser-ConfirmedRelease-count(locVar(stringvar)) | An Axiom |
| test-373 | ⊦ ¬ isUser-ConfirmedRelease-count(TravelPlanner-flightOffer) | An Axiom |
| test-374 | ⊦ ¬ isUser-ConfirmedRelease-count(CreditCardCenter-ccd) | An Axiom |
| test-375 | ⊦ ¬ isUser-ConfirmedRelease-count(Airline-flightOffers) | An Axiom |
| test-376 | ⊦ ¬ isUser-ConfirmRelease-count(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-377 | ⊦ ¬ isUser-ConfirmRelease-count(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-378 | ⊦ ¬ isUser-ConfirmRelease-count(User-Confirm-count(stringvar)) | An Axiom |
| test-379 | ⊦ ¬ isUser-ConfirmRelease-count(User-Confirms(stringvar)) | An Axiom |
| test-380 | ⊦ ¬ isUser-ConfirmRelease-count(User-Confirm(stringvar)) | An Axiom |
| test-381 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetInput-count(stringvar)) | An Axiom |
| test-382 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetInputs(stringvar)) | An Axiom |
| test-383 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetInput(stringvar)) | An Axiom |
| test-384 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-385 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-386 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-387 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-388 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetSingleSelections(stringvar)) | An Axiom |
| test-389 | ⊦ ¬ isUser-ConfirmRelease-count(User-GetSingleSelection(stringvar)) | An Axiom |
| test-390 | ⊦ ¬ isUser-ConfirmRelease-count(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-391 | ⊦ isUser-ConfirmRelease-count(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-392 | ⊦ ¬ isUser-ConfirmRelease-count(User-ConfirmReleases(stringvar)) | An Axiom |
| test-393 | ⊦ ¬ isUser-ConfirmRelease-count(User-ConfirmRelease(stringvar)) | An Axiom |
| test-394 | ⊦ ¬ isUser-ConfirmRelease-count(declassify-count(stringvar)) | An Axiom |
| test-395 | ⊦ ¬ isUser-ConfirmRelease-count(Mailbox(cmd)) | An Axiom |
| test-396 | ⊦ ¬ isUser-ConfirmRelease-count(state(stringvar)) | An Axiom |
| test-397 | ⊦ ¬ isUser-ConfirmRelease-count(locVar(stringvar)) | An Axiom |
| test-398 | ⊦ ¬ isUser-ConfirmRelease-count(TravelPlanner-flightOffer) | An Axiom |
| test-399 | ⊦ ¬ isUser-ConfirmRelease-count(CreditCardCenter-ccd) | An Axiom |
| test-400 | ⊦ ¬ isUser-ConfirmRelease-count(Airline-flightOffers) | An Axiom |
| test-401 | ⊦ ¬ isUser-ConfirmReleases(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-402 | ⊦ ¬ isUser-ConfirmReleases(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-403 | ⊦ ¬ isUser-ConfirmReleases(User-Confirm-count(stringvar)) | An Axiom |
| test-404 | ⊦ ¬ isUser-ConfirmReleases(User-Confirms(stringvar)) | An Axiom |
| test-405 | ⊦ ¬ isUser-ConfirmReleases(User-Confirm(stringvar)) | An Axiom |
| test-406 | ⊦ ¬ isUser-ConfirmReleases(User-GetInput-count(stringvar)) | An Axiom |
| test-407 | ⊦ ¬ isUser-ConfirmReleases(User-GetInputs(stringvar)) | An Axiom |
| test-408 | ⊦ ¬ isUser-ConfirmReleases(User-GetInput(stringvar)) | An Axiom |
| test-409 | ⊦ ¬ isUser-ConfirmReleases(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-410 | ⊦ ¬ isUser-ConfirmReleases(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-411 | ⊦ ¬ isUser-ConfirmReleases(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-412 | ⊦ ¬ isUser-ConfirmReleases(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-413 | ⊦ ¬ isUser-ConfirmReleases(User-GetSingleSelections(stringvar)) | An Axiom |
| test-414 | ⊦ ¬ isUser-ConfirmReleases(User-GetSingleSelection(stringvar)) | An Axiom |
| test-415 | ⊦ ¬ isUser-ConfirmReleases(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-416 | ⊦ ¬ isUser-ConfirmReleases(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-417 | ⊦ isUser-ConfirmReleases(User-ConfirmReleases(stringvar)) | An Axiom |
| test-418 | ⊦ ¬ isUser-ConfirmReleases(User-ConfirmRelease(stringvar)) | An Axiom |
| test-419 | ⊦ ¬ isUser-ConfirmReleases(declassify-count(stringvar)) | An Axiom |
| test-420 | ⊦ ¬ isUser-ConfirmReleases(Mailbox(cmd)) | An Axiom |
| test-421 | ⊦ ¬ isUser-ConfirmReleases(state(stringvar)) | An Axiom |
| test-422 | ⊦ ¬ isUser-ConfirmReleases(locVar(stringvar)) | An Axiom |
| test-423 | ⊦ ¬ isUser-ConfirmReleases(TravelPlanner-flightOffer) | An Axiom |
| test-424 | ⊦ ¬ isUser-ConfirmReleases(CreditCardCenter-ccd) | An Axiom |
| test-425 | ⊦ ¬ isUser-ConfirmReleases(Airline-flightOffers) | An Axiom |
| test-426 | ⊦ ¬ isUser-ConfirmRelease(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-427 | ⊦ ¬ isUser-ConfirmRelease(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-428 | ⊦ ¬ isUser-ConfirmRelease(User-Confirm-count(stringvar)) | An Axiom |
| test-429 | ⊦ ¬ isUser-ConfirmRelease(User-Confirms(stringvar)) | An Axiom |
| test-430 | ⊦ ¬ isUser-ConfirmRelease(User-Confirm(stringvar)) | An Axiom |
| test-431 | ⊦ ¬ isUser-ConfirmRelease(User-GetInput-count(stringvar)) | An Axiom |
| test-432 | ⊦ ¬ isUser-ConfirmRelease(User-GetInputs(stringvar)) | An Axiom |
| test-433 | ⊦ ¬ isUser-ConfirmRelease(User-GetInput(stringvar)) | An Axiom |
| test-434 | ⊦ ¬ isUser-ConfirmRelease(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-435 | ⊦ ¬ isUser-ConfirmRelease(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-436 | ⊦ ¬ isUser-ConfirmRelease(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-437 | ⊦ ¬ isUser-ConfirmRelease(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-438 | ⊦ ¬ isUser-ConfirmRelease(User-GetSingleSelections(stringvar)) | An Axiom |
| test-439 | ⊦ ¬ isUser-ConfirmRelease(User-GetSingleSelection(stringvar)) | An Axiom |
| test-440 | ⊦ ¬ isUser-ConfirmRelease(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-441 | ⊦ ¬ isUser-ConfirmRelease(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-442 | ⊦ ¬ isUser-ConfirmRelease(User-ConfirmReleases(stringvar)) | An Axiom |
| test-443 | ⊦ isUser-ConfirmRelease(User-ConfirmRelease(stringvar)) | An Axiom |
| test-444 | ⊦ ¬ isUser-ConfirmRelease(declassify-count(stringvar)) | An Axiom |
| test-445 | ⊦ ¬ isUser-ConfirmRelease(Mailbox(cmd)) | An Axiom |
| test-446 | ⊦ ¬ isUser-ConfirmRelease(state(stringvar)) | An Axiom |
| test-447 | ⊦ ¬ isUser-ConfirmRelease(locVar(stringvar)) | An Axiom |
| test-448 | ⊦ ¬ isUser-ConfirmRelease(TravelPlanner-flightOffer) | An Axiom |
| test-449 | ⊦ ¬ isUser-ConfirmRelease(CreditCardCenter-ccd) | An Axiom |
| test-450 | ⊦ ¬ isUser-ConfirmRelease(Airline-flightOffers) | An Axiom |
| test-451 | ⊦ ¬ isDeclassify-count(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-452 | ⊦ ¬ isDeclassify-count(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-453 | ⊦ ¬ isDeclassify-count(User-Confirm-count(stringvar)) | An Axiom |
| test-454 | ⊦ ¬ isDeclassify-count(User-Confirms(stringvar)) | An Axiom |
| test-455 | ⊦ ¬ isDeclassify-count(User-Confirm(stringvar)) | An Axiom |
| test-456 | ⊦ ¬ isDeclassify-count(User-GetInput-count(stringvar)) | An Axiom |
| test-457 | ⊦ ¬ isDeclassify-count(User-GetInputs(stringvar)) | An Axiom |
| test-458 | ⊦ ¬ isDeclassify-count(User-GetInput(stringvar)) | An Axiom |
| test-459 | ⊦ ¬ isDeclassify-count(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-460 | ⊦ ¬ isDeclassify-count(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-461 | ⊦ ¬ isDeclassify-count(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-462 | ⊦ ¬ isDeclassify-count(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-463 | ⊦ ¬ isDeclassify-count(User-GetSingleSelections(stringvar)) | An Axiom |
| test-464 | ⊦ ¬ isDeclassify-count(User-GetSingleSelection(stringvar)) | An Axiom |
| test-465 | ⊦ ¬ isDeclassify-count(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-466 | ⊦ ¬ isDeclassify-count(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-467 | ⊦ ¬ isDeclassify-count(User-ConfirmReleases(stringvar)) | An Axiom |
| test-468 | ⊦ ¬ isDeclassify-count(User-ConfirmRelease(stringvar)) | An Axiom |
| test-469 | ⊦ isDeclassify-count(declassify-count(stringvar)) | An Axiom |
| test-470 | ⊦ ¬ isDeclassify-count(Mailbox(cmd)) | An Axiom |
| test-471 | ⊦ ¬ isDeclassify-count(state(stringvar)) | An Axiom |
| test-472 | ⊦ ¬ isDeclassify-count(locVar(stringvar)) | An Axiom |
| test-473 | ⊦ ¬ isDeclassify-count(TravelPlanner-flightOffer) | An Axiom |
| test-474 | ⊦ ¬ isDeclassify-count(CreditCardCenter-ccd) | An Axiom |
| test-475 | ⊦ ¬ isDeclassify-count(Airline-flightOffers) | An Axiom |
| test-476 | ⊦ ¬ isMailbox(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-477 | ⊦ ¬ isMailbox(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-478 | ⊦ ¬ isMailbox(User-Confirm-count(stringvar)) | An Axiom |
| test-479 | ⊦ ¬ isMailbox(User-Confirms(stringvar)) | An Axiom |
| test-480 | ⊦ ¬ isMailbox(User-Confirm(stringvar)) | An Axiom |
| test-481 | ⊦ ¬ isMailbox(User-GetInput-count(stringvar)) | An Axiom |
| test-482 | ⊦ ¬ isMailbox(User-GetInputs(stringvar)) | An Axiom |
| test-483 | ⊦ ¬ isMailbox(User-GetInput(stringvar)) | An Axiom |
| test-484 | ⊦ ¬ isMailbox(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-485 | ⊦ ¬ isMailbox(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-486 | ⊦ ¬ isMailbox(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-487 | ⊦ ¬ isMailbox(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-488 | ⊦ ¬ isMailbox(User-GetSingleSelections(stringvar)) | An Axiom |
| test-489 | ⊦ ¬ isMailbox(User-GetSingleSelection(stringvar)) | An Axiom |
| test-490 | ⊦ ¬ isMailbox(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-491 | ⊦ ¬ isMailbox(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-492 | ⊦ ¬ isMailbox(User-ConfirmReleases(stringvar)) | An Axiom |
| test-493 | ⊦ ¬ isMailbox(User-ConfirmRelease(stringvar)) | An Axiom |
| test-494 | ⊦ ¬ isMailbox(declassify-count(stringvar)) | An Axiom |
| test-495 | ⊦ isMailbox(Mailbox(cmd)) | An Axiom |
| test-496 | ⊦ ¬ isMailbox(state(stringvar)) | An Axiom |
| test-497 | ⊦ ¬ isMailbox(locVar(stringvar)) | An Axiom |
| test-498 | ⊦ ¬ isMailbox(TravelPlanner-flightOffer) | An Axiom |
| test-499 | ⊦ ¬ isMailbox(CreditCardCenter-ccd) | An Axiom |
| test-500 | ⊦ ¬ isMailbox(Airline-flightOffers) | An Axiom |
| test-501 | ⊦ ¬ isState(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-502 | ⊦ ¬ isState(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-503 | ⊦ ¬ isState(User-Confirm-count(stringvar)) | An Axiom |
| test-504 | ⊦ ¬ isState(User-Confirms(stringvar)) | An Axiom |
| test-505 | ⊦ ¬ isState(User-Confirm(stringvar)) | An Axiom |
| test-506 | ⊦ ¬ isState(User-GetInput-count(stringvar)) | An Axiom |
| test-507 | ⊦ ¬ isState(User-GetInputs(stringvar)) | An Axiom |
| test-508 | ⊦ ¬ isState(User-GetInput(stringvar)) | An Axiom |
| test-509 | ⊦ ¬ isState(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-510 | ⊦ ¬ isState(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-511 | ⊦ ¬ isState(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-512 | ⊦ ¬ isState(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-513 | ⊦ ¬ isState(User-GetSingleSelections(stringvar)) | An Axiom |
| test-514 | ⊦ ¬ isState(User-GetSingleSelection(stringvar)) | An Axiom |
| test-515 | ⊦ ¬ isState(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-516 | ⊦ ¬ isState(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-517 | ⊦ ¬ isState(User-ConfirmReleases(stringvar)) | An Axiom |
| test-518 | ⊦ ¬ isState(User-ConfirmRelease(stringvar)) | An Axiom |
| test-519 | ⊦ ¬ isState(declassify-count(stringvar)) | An Axiom |
| test-520 | ⊦ ¬ isState(Mailbox(cmd)) | An Axiom |
| test-521 | ⊦ isState(state(stringvar)) | An Axiom |
| test-522 | ⊦ ¬ isState(locVar(stringvar)) | An Axiom |
| test-523 | ⊦ ¬ isState(TravelPlanner-flightOffer) | An Axiom |
| test-524 | ⊦ ¬ isState(CreditCardCenter-ccd) | An Axiom |
| test-525 | ⊦ ¬ isState(Airline-flightOffers) | An Axiom |
| test-526 | ⊦ ¬ isLocVar(ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| test-527 | ⊦ ¬ isLocVar(ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| test-528 | ⊦ ¬ isLocVar(User-Confirm-count(stringvar)) | An Axiom |
| test-529 | ⊦ ¬ isLocVar(User-Confirms(stringvar)) | An Axiom |
| test-530 | ⊦ ¬ isLocVar(User-Confirm(stringvar)) | An Axiom |
| test-531 | ⊦ ¬ isLocVar(User-GetInput-count(stringvar)) | An Axiom |
| test-532 | ⊦ ¬ isLocVar(User-GetInputs(stringvar)) | An Axiom |
| test-533 | ⊦ ¬ isLocVar(User-GetInput(stringvar)) | An Axiom |
| test-534 | ⊦ ¬ isLocVar(User-GetMultipleSelection-count(stringvar)) | An Axiom |
| test-535 | ⊦ ¬ isLocVar(User-GetMultipleSelections(stringvar)) | An Axiom |
| test-536 | ⊦ ¬ isLocVar(User-GetMultipleSelection(stringvar)) | An Axiom |
| test-537 | ⊦ ¬ isLocVar(User-GetSingleSelection-count(stringvar)) | An Axiom |
| test-538 | ⊦ ¬ isLocVar(User-GetSingleSelections(stringvar)) | An Axiom |
| test-539 | ⊦ ¬ isLocVar(User-GetSingleSelection(stringvar)) | An Axiom |
| test-540 | ⊦ ¬ isLocVar(User-ConfirmedRelease-count(stringvar)) | An Axiom |
| test-541 | ⊦ ¬ isLocVar(User-ConfirmRelease-count(stringvar)) | An Axiom |
| test-542 | ⊦ ¬ isLocVar(User-ConfirmReleases(stringvar)) | An Axiom |
| test-543 | ⊦ ¬ isLocVar(User-ConfirmRelease(stringvar)) | An Axiom |
| test-544 | ⊦ ¬ isLocVar(declassify-count(stringvar)) | An Axiom |
| test-545 | ⊦ ¬ isLocVar(Mailbox(cmd)) | An Axiom |
| test-546 | ⊦ ¬ isLocVar(state(stringvar)) | An Axiom |
| test-547 | ⊦ isLocVar(locVar(stringvar)) | An Axiom |
| test-548 | ⊦ ¬ isLocVar(TravelPlanner-flightOffer) | An Axiom |
| test-549 | ⊦ ¬ isLocVar(CreditCardCenter-ccd) | An Axiom |
| test-550 | ⊦ ¬ isLocVar(Airline-flightOffers) | An Axiom |
| inj-01 | ⊦ ReadSourceCount(stringvar, stringvar0) = ReadSourceCount(stringvar1, stringvar2) ↔ stringvar = stringvar1 ∧ stringvar0 = stringvar2 | An Axiom |
| inj-02 | ⊦ ReadSourceInputs(stringvar, stringvar0) = ReadSourceInputs(stringvar1, stringvar2) ↔ stringvar = stringvar1 ∧ stringvar0 = stringvar2 | An Axiom |
| inj-03 | ⊦ User-Confirm-count(stringvar) = User-Confirm-count(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-04 | ⊦ User-Confirms(stringvar) = User-Confirms(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-05 | ⊦ User-Confirm(stringvar) = User-Confirm(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-06 | ⊦ User-GetInput-count(stringvar) = User-GetInput-count(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-07 | ⊦ User-GetInputs(stringvar) = User-GetInputs(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-08 | ⊦ User-GetInput(stringvar) = User-GetInput(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-09 | ⊦ User-GetMultipleSelection-count(stringvar) = User-GetMultipleSelection-count(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-10 | ⊦ User-GetMultipleSelections(stringvar) = User-GetMultipleSelections(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-11 | ⊦ User-GetMultipleSelection(stringvar) = User-GetMultipleSelection(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-12 | ⊦ User-GetSingleSelection-count(stringvar) = User-GetSingleSelection-count(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-13 | ⊦ User-GetSingleSelections(stringvar) = User-GetSingleSelections(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-14 | ⊦ User-GetSingleSelection(stringvar) = User-GetSingleSelection(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-15 | ⊦ User-ConfirmedRelease-count(stringvar) = User-ConfirmedRelease-count(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-16 | ⊦ User-ConfirmRelease-count(stringvar) = User-ConfirmRelease-count(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-17 | ⊦ User-ConfirmReleases(stringvar) = User-ConfirmReleases(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-18 | ⊦ User-ConfirmRelease(stringvar) = User-ConfirmRelease(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-19 | ⊦ declassify-count(stringvar) = declassify-count(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-20 | ⊦ Mailbox(cmd) = Mailbox(cmd0) ↔ cmd = cmd0 | An Axiom |
| inj-21 | ⊦ state(stringvar) = state(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| inj-22 | ⊦ locVar(stringvar) = locVar(stringvar0) ↔ stringvar = stringvar0 | An Axiom |
| case | ⊦ nam = Airline-flightOffers ∨ nam = CreditCardCenter-ccd ∨ nam = TravelPlanner-flightOffer ∨ nam = locVar(nam .name) ∨ nam = state(nam .name) ∨ nam = Mailbox(nam .cmd) ∨ nam = declassify-count(nam .name) ∨ nam = User-ConfirmRelease(nam .name) ∨ nam = User-ConfirmReleases(nam .name) ∨ nam = User-ConfirmRelease-count(nam .name) ∨ nam = User-ConfirmedRelease-count(nam .name) ∨ nam = User-GetSingleSelection(nam .name) ∨ nam = User-GetSingleSelections(nam .name) ∨ nam = User-GetSingleSelection-count(nam .name) ∨ nam = User-GetMultipleSelection(nam .name) ∨ nam = User-GetMultipleSelections(nam .name) ∨ nam = User-GetMultipleSelection-count(nam .name) ∨ nam = User-GetInput(nam .name) ∨ nam = User-GetInputs(nam .name) ∨ nam = User-GetInput-count(nam .name) ∨ nam = User-Confirm(nam .name) ∨ nam = User-Confirms(nam .name) ∨ nam = User-Confirm-count(nam .name) ∨ nam = ReadSourceInputs(nam .methodname, nam .call) ∨ nam = ReadSourceCount(nam .methodname, nam .call) | An Axiom |
| ex-01 | ⊦ isReadSourceCount(nam) ↔ (∃ stringvar, stringvar0. nam = ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| ex-02 | ⊦ isReadSourceInputs(nam) ↔ (∃ stringvar, stringvar0. nam = ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| ex-03 | ⊦ isUser-Confirm-count(nam) ↔ (∃ stringvar. nam = User-Confirm-count(stringvar)) | An Axiom |
| ex-04 | ⊦ isUser-Confirms(nam) ↔ (∃ stringvar. nam = User-Confirms(stringvar)) | An Axiom |
| ex-05 | ⊦ isUser-Confirm(nam) ↔ (∃ stringvar. nam = User-Confirm(stringvar)) | An Axiom |
| ex-06 | ⊦ isUser-GetInput-count(nam) ↔ (∃ stringvar. nam = User-GetInput-count(stringvar)) | An Axiom |
| ex-07 | ⊦ isUser-GetInputs(nam) ↔ (∃ stringvar. nam = User-GetInputs(stringvar)) | An Axiom |
| ex-08 | ⊦ isUser-GetInput(nam) ↔ (∃ stringvar. nam = User-GetInput(stringvar)) | An Axiom |
| ex-09 | ⊦ isUser-GetMultipleSelection-count(nam) ↔ (∃ stringvar. nam = User-GetMultipleSelection-count(stringvar)) | An Axiom |
| ex-10 | ⊦ isUser-GetMultipleSelections(nam) ↔ (∃ stringvar. nam = User-GetMultipleSelections(stringvar)) | An Axiom |
| ex-11 | ⊦ isUser-GetMultipleSelection(nam) ↔ (∃ stringvar. nam = User-GetMultipleSelection(stringvar)) | An Axiom |
| ex-12 | ⊦ isUser-GetSingleSelection-count(nam) ↔ (∃ stringvar. nam = User-GetSingleSelection-count(stringvar)) | An Axiom |
| ex-13 | ⊦ isUser-GetSingleSelections(nam) ↔ (∃ stringvar. nam = User-GetSingleSelections(stringvar)) | An Axiom |
| ex-14 | ⊦ isUser-GetSingleSelection(nam) ↔ (∃ stringvar. nam = User-GetSingleSelection(stringvar)) | An Axiom |
| ex-15 | ⊦ isUser-ConfirmedRelease-count(nam) ↔ (∃ stringvar. nam = User-ConfirmedRelease-count(stringvar)) | An Axiom |
| ex-16 | ⊦ isUser-ConfirmRelease-count(nam) ↔ (∃ stringvar. nam = User-ConfirmRelease-count(stringvar)) | An Axiom |
| ex-17 | ⊦ isUser-ConfirmReleases(nam) ↔ (∃ stringvar. nam = User-ConfirmReleases(stringvar)) | An Axiom |
| ex-18 | ⊦ isUser-ConfirmRelease(nam) ↔ (∃ stringvar. nam = User-ConfirmRelease(stringvar)) | An Axiom |
| ex-19 | ⊦ isDeclassify-count(nam) ↔ (∃ stringvar. nam = declassify-count(stringvar)) | An Axiom |
| ex-20 | ⊦ isMailbox(nam) ↔ (∃ cmd. nam = Mailbox(cmd)) | An Axiom |
| ex-21 | ⊦ isState(nam) ↔ (∃ stringvar. nam = state(stringvar)) | An Axiom |
| ex-22 | ⊦ isLocVar(nam) ↔ (∃ stringvar. nam = locVar(stringvar)) | An Axiom |
| elim-01 | ⊦ isReadSourceCount(nam) → (stringvar = nam .methodname ∧ stringvar0 = nam .call ↔ nam = ReadSourceCount(stringvar, stringvar0)) | An Axiom |
| elim-02 | ⊦ isReadSourceInputs(nam) → (stringvar = nam .methodname ∧ stringvar0 = nam .call ↔ nam = ReadSourceInputs(stringvar, stringvar0)) | An Axiom |
| elim-03 | ⊦ isUser-Confirm-count(nam) → (stringvar = nam .name ↔ nam = User-Confirm-count(stringvar)) | An Axiom |
| elim-04 | ⊦ isUser-Confirms(nam) → (stringvar = nam .name ↔ nam = User-Confirms(stringvar)) | An Axiom |
| elim-05 | ⊦ isUser-Confirm(nam) → (stringvar = nam .name ↔ nam = User-Confirm(stringvar)) | An Axiom |
| elim-06 | ⊦ isUser-GetInput-count(nam) → (stringvar = nam .name ↔ nam = User-GetInput-count(stringvar)) | An Axiom |
| elim-07 | ⊦ isUser-GetInputs(nam) → (stringvar = nam .name ↔ nam = User-GetInputs(stringvar)) | An Axiom |
| elim-08 | ⊦ isUser-GetInput(nam) → (stringvar = nam .name ↔ nam = User-GetInput(stringvar)) | An Axiom |
| elim-09 | ⊦ isUser-GetMultipleSelection-count(nam) → (stringvar = nam .name ↔ nam = User-GetMultipleSelection-count(stringvar)) | An Axiom |
| elim-10 | ⊦ isUser-GetMultipleSelections(nam) → (stringvar = nam .name ↔ nam = User-GetMultipleSelections(stringvar)) | An Axiom |
| elim-11 | ⊦ isUser-GetMultipleSelection(nam) → (stringvar = nam .name ↔ nam = User-GetMultipleSelection(stringvar)) | An Axiom |
| elim-12 | ⊦ isUser-GetSingleSelection-count(nam) → (stringvar = nam .name ↔ nam = User-GetSingleSelection-count(stringvar)) | An Axiom |
| elim-13 | ⊦ isUser-GetSingleSelections(nam) → (stringvar = nam .name ↔ nam = User-GetSingleSelections(stringvar)) | An Axiom |
| elim-14 | ⊦ isUser-GetSingleSelection(nam) → (stringvar = nam .name ↔ nam = User-GetSingleSelection(stringvar)) | An Axiom |
| elim-15 | ⊦ isUser-ConfirmedRelease-count(nam) → (stringvar = nam .name ↔ nam = User-ConfirmedRelease-count(stringvar)) | An Axiom |
| elim-16 | ⊦ isUser-ConfirmRelease-count(nam) → (stringvar = nam .name ↔ nam = User-ConfirmRelease-count(stringvar)) | An Axiom |
| elim-17 | ⊦ isUser-ConfirmReleases(nam) → (stringvar = nam .name ↔ nam = User-ConfirmReleases(stringvar)) | An Axiom |
| elim-18 | ⊦ isUser-ConfirmRelease(nam) → (stringvar = nam .name ↔ nam = User-ConfirmRelease(stringvar)) | An Axiom |
| elim-19 | ⊦ isDeclassify-count(nam) → (stringvar = nam .name ↔ nam = declassify-count(stringvar)) | An Axiom |
| elim-20 | ⊦ isMailbox(nam) → (cmd = nam .cmd ↔ nam = Mailbox(cmd)) | An Axiom |
| elim-21 | ⊦ isState(nam) → (stringvar = nam .name ↔ nam = state(stringvar)) | An Axiom |
| elim-22 | ⊦ isLocVar(nam) → (stringvar = nam .name ↔ nam = locVar(stringvar)) | An Axiom |
| gen | An Axiom |