[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification dominterference

dominterference/Abort8-interference-def is used by alter-observe-respects-policy,
dominterference/Abort9-interference-def is used by alter-observe-respects-policy,
dominterference/HighLow5-interference-def is used by alter-observe-respects-policy,
dominterference/User-User_Airline-interference-def is used by alter-observe-respects-policy,
dominterference/User-interference-def is used by ccd-no-read-up, alter-observe-respects-policy,
dominterference/User_Airline-interference-def is used by alter-observe-respects-policy,
dominterference/User_TravelAgency_Airline-interference-def is used by flightOffers-no-read-up, alter-observe-respects-policy,

Used from specification command

command/disj-100 is used by alter-observe-respects-policy,
command/disj-101 is used by alter-observe-respects-policy,
command/disj-103 is used by alter-observe-respects-policy,
command/disj-104 is used by alter-observe-respects-policy,
command/disj-106 is used by alter-observe-respects-policy,
command/disj-107 is used by alter-observe-respects-policy,
command/disj-108 is used by alter-observe-respects-policy,
command/disj-119 is used by alter-observe-respects-policy,
command/disj-120 is used by alter-observe-respects-policy,
command/disj-125 is used by alter-observe-respects-policy,
command/disj-126 is used by alter-observe-respects-policy,
command/disj-129 is used by alter-observe-respects-policy,
command/disj-132 is used by alter-observe-respects-policy,
command/disj-138 is used by alter-observe-respects-policy,
command/disj-139 is used by alter-observe-respects-policy,
command/disj-144 is used by alter-observe-respects-policy,
command/disj-145 is used by alter-observe-respects-policy,
command/disj-148 is used by alter-observe-respects-policy,
command/disj-151 is used by alter-observe-respects-policy,
command/disj-156 is used by alter-observe-respects-policy,
command/disj-157 is used by alter-observe-respects-policy,
command/disj-162 is used by alter-observe-respects-policy,
command/disj-163 is used by alter-observe-respects-policy,
command/disj-166 is used by alter-observe-respects-policy,
command/disj-169 is used by alter-observe-respects-policy,
command/disj-173 is used by alter-observe-respects-policy,
command/disj-174 is used by alter-observe-respects-policy,
command/disj-179 is used by alter-observe-respects-policy,
command/disj-180 is used by alter-observe-respects-policy,
command/disj-183 is used by alter-observe-respects-policy,
command/disj-186 is used by alter-observe-respects-policy,
command/disj-191 is used by alter-observe-respects-policy,
command/disj-193 is used by alter-observe-respects-policy,
command/disj-194 is used by alter-observe-respects-policy,
command/disj-195 is used by alter-observe-respects-policy,
command/disj-197 is used by alter-observe-respects-policy,
command/disj-198 is used by alter-observe-respects-policy,
command/disj-199 is used by alter-observe-respects-policy,
command/disj-202 is used by alter-observe-respects-policy,
command/disj-206 is used by alter-observe-respects-policy,
command/disj-208 is used by alter-observe-respects-policy,
command/disj-209 is used by alter-observe-respects-policy,
command/disj-210 is used by alter-observe-respects-policy,
command/disj-212 is used by alter-observe-respects-policy,
command/disj-213 is used by alter-observe-respects-policy,
command/disj-214 is used by alter-observe-respects-policy,
command/disj-217 is used by alter-observe-respects-policy,
command/disj-224 is used by alter-observe-respects-policy,
command/disj-225 is used by alter-observe-respects-policy,
command/disj-228 is used by alter-observe-respects-policy,
command/disj-231 is used by alter-observe-respects-policy,
command/disj-249 is used by alter-observe-respects-policy,
command/disj-250 is used by alter-observe-respects-policy,
command/disj-253 is used by alter-observe-respects-policy,
command/disj-256 is used by alter-observe-respects-policy,
command/disj-260 is used by alter-observe-respects-policy,
command/disj-261 is used by alter-observe-respects-policy,
command/disj-264 is used by alter-observe-respects-policy,
command/disj-267 is used by alter-observe-respects-policy,
command/disj-271 is used by alter-observe-respects-policy,
command/disj-272 is used by alter-observe-respects-policy,
command/disj-273 is used by alter-observe-respects-policy,
command/disj-28 is used by alter-observe-respects-policy,
command/disj-281 is used by alter-observe-respects-policy,
command/disj-282 is used by alter-observe-respects-policy,
command/disj-283 is used by alter-observe-respects-policy,
command/disj-286 is used by alter-observe-respects-policy,
command/disj-291 is used by alter-observe-respects-policy,
command/disj-294 is used by alter-observe-respects-policy,
command/disj-298 is used by alter-observe-respects-policy,
command/disj-301 is used by alter-observe-respects-policy,
command/disj-33 is used by alter-observe-respects-policy,
command/disj-34 is used by alter-observe-respects-policy,
command/disj-39 is used by alter-observe-respects-policy,
command/disj-40 is used by alter-observe-respects-policy,
command/disj-43 is used by alter-observe-respects-policy,
command/disj-46 is used by alter-observe-respects-policy,
command/disj-95 is used by alter-observe-respects-policy,
command/disj-96 is used by alter-observe-respects-policy,
command/disj-97 is used by alter-observe-respects-policy,
command/disj-98 is used by alter-observe-respects-policy,
command/disj-99 is used by alter-observe-respects-policy,

Used from specification domain

domain/disj-01 is used by IFProperty1, ccd-no-read-up, alter-observe-respects-policy,
domain/disj-02 is used by IFProperty2, IFProperty1, ccd-no-read-up, alter-observe-respects-policy,
domain/disj-03 is used by flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-04 is used by ccd-no-read-up, flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-05 is used by ccd-no-read-up, flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-06 is used by flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-07 is used by IFProperty2, alter-observe-respects-policy,
domain/disj-08 is used by IFProperty1, ccd-no-read-up, flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-09 is used by flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-10 is used by flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-11 is used by IFProperty1, ccd-no-read-up, flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-12 is used by IFProperty2, IFProperty1, ccd-no-read-up, flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-13 is used by flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-14 is used by flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-15 is used by IFProperty2, IFProperty1, ccd-no-read-up, flightOffers-no-read-up, alter-observe-respects-policy,
domain/disj-16 is used by ccd-no-read-up, alter-observe-respects-policy,
domain/disj-17 is used by ccd-no-read-up, alter-observe-respects-policy,
domain/disj-18 is used by alter-observe-respects-policy,
domain/disj-19 is used by alter-observe-respects-policy,
domain/disj-20 is used by ccd-no-read-up, alter-observe-respects-policy,
domain/disj-21 is used by ccd-no-read-up, alter-observe-respects-policy,

Used from specification domdefinitions

domdefinitions/dom-Mailbox-BookFlightOffer is used by IFProperty1,
domdefinitions/dom-Mailbox-GetFlightOffers-02 is used by IFProperty2,
domdefinitions/dom-Mailbox-GetFlightOffers-03 is used by IFProperty1,
domdefinitions/dom-Mailbox-OkPayCommission is used by IFProperty1,
domdefinitions/dom-Mailbox-PayCommission is used by IFProperty2,
domdefinitions/dom-Mailbox-RetFlightOffers-01 is used by IFProperty2,
domdefinitions/dom-ccd is used by IFProperty2, IFProperty1, ccd-no-write-down, ccd-no-read-up,
domdefinitions/dom-flightOffers is used by flightOffers-no-write-down, flightOffers-no-read-up,

Used from specification set-basic

set-basic/domains/add-01 is used by IFProperty2,
set-basic/domains/addtwo is used by IFProperty1,
set-basic/domains/in-04 is used by IFProperty2, IFProperty1,
set-basic/domains/rax is used by IFProperty1,

Used from specification exAgent

exAgent/ex-not-36 is used by alter-observe-respects-policy,
exAgent/ex-not-37 is used by alter-observe-respects-policy,
exAgent/ex-not-40 is used by alter-observe-respects-policy,
exAgent/exAirline-s is used by alter-observe-respects-policy,
exAgent/exTravelAgency-s is used by alter-observe-respects-policy,

Used from specification observeAlter

observeAlter/alter-Abort8 is used by ccd-no-write-down, flightOffers-no-write-down, alter-observe-respects-policy,
observeAlter/alter-Abort9 is used by ccd-no-write-down, flightOffers-no-write-down, alter-observe-respects-policy,
observeAlter/alter-HighLow5 is used by ccd-no-write-down, flightOffers-no-write-down, alter-observe-respects-policy,
observeAlter/alter-User is used by ccd-no-write-down, flightOffers-no-write-down, alter-observe-respects-policy,
observeAlter/alter-User-User_Airline is used by ccd-no-write-down, flightOffers-no-write-down, alter-observe-respects-policy,
observeAlter/alter-User_Airline is used by ccd-no-write-down, flightOffers-no-write-down, alter-observe-respects-policy,
observeAlter/alter-User_TravelAgency_Airline is used by ccd-no-write-down, flightOffers-no-write-down, alter-observe-respects-policy,
observeAlter/observe-Abort8 is used by ccd-no-read-up, flightOffers-no-read-up, alter-observe-respects-policy,
observeAlter/observe-Abort9 is used by flightOffers-no-read-up, alter-observe-respects-policy,
observeAlter/observe-HighLow5 is used by ccd-no-read-up, flightOffers-no-read-up, alter-observe-respects-policy,
observeAlter/observe-User is used by alter-observe-respects-policy,
observeAlter/observe-User-User_Airline is used by flightOffers-no-read-up, alter-observe-respects-policy,
observeAlter/observe-User_Airline is used by ccd-no-read-up, alter-observe-respects-policy,
observeAlter/observe-User_TravelAgency_Airline is used by ccd-no-read-up, alter-observe-respects-policy,

Used from specification name

name/disj-01 is used by ccd-no-read-up, flightOffers-no-read-up,
name/disj-02 is used by flightOffers-no-write-down, alter-observe-respects-policy,
name/disj-03 is used by flightOffers-no-write-down, alter-observe-respects-policy,
name/disj-04 is used by flightOffers-no-write-down, flightOffers-no-read-up, alter-observe-respects-policy,
name/disj-05 is used by flightOffers-no-write-down, alter-observe-respects-policy,
name/disj-06 is used by flightOffers-no-write-down, flightOffers-no-read-up, alter-observe-respects-policy,
name/disj-07 is used by flightOffers-no-write-down, alter-observe-respects-policy,
name/disj-09 is used by flightOffers-no-write-down, alter-observe-respects-policy,
name/disj-10 is used by flightOffers-no-write-down, alter-observe-respects-policy,
name/disj-103 is used by alter-observe-respects-policy,
name/disj-104 is used by alter-observe-respects-policy,
name/disj-105 is used by alter-observe-respects-policy,
name/disj-106 is used by alter-observe-respects-policy,
name/disj-107 is used by alter-observe-respects-policy,
name/disj-108 is used by alter-observe-respects-policy,
name/disj-11 is used by flightOffers-no-write-down, alter-observe-respects-policy,
name/disj-111 is used by alter-observe-respects-policy,
name/disj-112 is used by alter-observe-respects-policy,
name/disj-114 is used by alter-observe-respects-policy,
name/disj-115 is used by alter-observe-respects-policy,
name/disj-116 is used by alter-observe-respects-policy,
name/disj-117 is used by alter-observe-respects-policy,
name/disj-118 is used by alter-observe-respects-policy,
name/disj-122 is used by alter-observe-respects-policy,
name/disj-123 is used by alter-observe-respects-policy,
name/disj-124 is used by alter-observe-respects-policy,
name/disj-125 is used by alter-observe-respects-policy,
name/disj-126 is used by alter-observe-respects-policy,
name/disj-127 is used by alter-observe-respects-policy,
name/disj-13 is used by flightOffers-no-write-down, alter-observe-respects-policy,
name/disj-130 is used by alter-observe-respects-policy,
name/disj-131 is used by alter-observe-respects-policy,
name/disj-132 is used by alter-observe-respects-policy,
name/disj-133 is used by alter-observe-respects-policy,
name/disj-134 is used by alter-observe-respects-policy,
name/disj-136 is used by alter-observe-respects-policy,
name/disj-140 is used by alter-observe-respects-policy,
name/disj-141 is used by alter-observe-respects-policy,
name/disj-142 is used by alter-observe-respects-policy,
name/disj-143 is used by alter-observe-respects-policy,
name/disj-144 is used by alter-observe-respects-policy,
name/disj-145 is used by alter-observe-respects-policy,
name/disj-151 is used by alter-observe-respects-policy,
name/disj-152 is used by alter-observe-respects-policy,
name/disj-153 is used by alter-observe-respects-policy,
name/disj-157 is used by alter-observe-respects-policy,
name/disj-158 is used by alter-observe-respects-policy,
name/disj-159 is used by alter-observe-respects-policy,
name/disj-160 is used by alter-observe-respects-policy,
name/disj-161 is used by alter-observe-respects-policy,
name/disj-162 is used by alter-observe-respects-policy,
name/disj-17 is used by flightOffers-no-write-down,
name/disj-182 is used by alter-observe-respects-policy,
name/disj-183 is used by alter-observe-respects-policy,
name/disj-184 is used by alter-observe-respects-policy,
name/disj-188 is used by alter-observe-respects-policy,
name/disj-189 is used by alter-observe-respects-policy,
name/disj-19 is used by flightOffers-no-write-down,
name/disj-190 is used by alter-observe-respects-policy,
name/disj-191 is used by alter-observe-respects-policy,
name/disj-192 is used by alter-observe-respects-policy,
name/disj-193 is used by alter-observe-respects-policy,
name/disj-196 is used by alter-observe-respects-policy,
name/disj-197 is used by alter-observe-respects-policy,
name/disj-198 is used by alter-observe-respects-policy,
name/disj-20 is used by flightOffers-no-write-down,
name/disj-202 is used by alter-observe-respects-policy,
name/disj-203 is used by alter-observe-respects-policy,
name/disj-204 is used by alter-observe-respects-policy,
name/disj-205 is used by alter-observe-respects-policy,
name/disj-206 is used by alter-observe-respects-policy,
name/disj-207 is used by alter-observe-respects-policy,
name/disj-215 is used by alter-observe-respects-policy,
name/disj-216 is used by alter-observe-respects-policy,
name/disj-217 is used by alter-observe-respects-policy,
name/disj-218 is used by alter-observe-respects-policy,
name/disj-219 is used by alter-observe-respects-policy,
name/disj-22 is used by flightOffers-no-write-down,
name/disj-220 is used by alter-observe-respects-policy,
name/disj-238 is used by alter-observe-respects-policy,
name/disj-239 is used by alter-observe-respects-policy,
name/disj-240 is used by alter-observe-respects-policy,
name/disj-241 is used by alter-observe-respects-policy,
name/disj-242 is used by alter-observe-respects-policy,
name/disj-243 is used by alter-observe-respects-policy,
name/disj-25 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-26 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-27 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-28 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-29 is used by ccd-no-write-down, alter-observe-respects-policy,
name/disj-30 is used by ccd-no-write-down,
name/disj-32 is used by ccd-no-write-down,
name/disj-33 is used by ccd-no-write-down,
name/disj-34 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-35 is used by ccd-no-read-up,
name/disj-36 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-40 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-41 is used by ccd-no-read-up,
name/disj-42 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-43 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-44 is used by ccd-no-read-up,
name/disj-45 is used by ccd-no-write-down, ccd-no-read-up, alter-observe-respects-policy,
name/disj-48 is used by alter-observe-respects-policy,
name/disj-49 is used by alter-observe-respects-policy,
name/disj-50 is used by alter-observe-respects-policy,
name/disj-51 is used by alter-observe-respects-policy,
name/disj-52 is used by alter-observe-respects-policy,
name/disj-54 is used by alter-observe-respects-policy,
name/disj-55 is used by alter-observe-respects-policy,
name/disj-62 is used by alter-observe-respects-policy,
name/disj-63 is used by alter-observe-respects-policy,
name/disj-64 is used by alter-observe-respects-policy,
name/disj-65 is used by alter-observe-respects-policy,
name/disj-66 is used by alter-observe-respects-policy,
name/disj-67 is used by alter-observe-respects-policy,
name/disj-70 is used by alter-observe-respects-policy,
name/disj-71 is used by alter-observe-respects-policy,
name/disj-72 is used by alter-observe-respects-policy,
name/disj-73 is used by alter-observe-respects-policy,
name/disj-74 is used by alter-observe-respects-policy,
name/disj-75 is used by alter-observe-respects-policy,
name/disj-76 is used by alter-observe-respects-policy,
name/disj-77 is used by alter-observe-respects-policy,
name/disj-78 is used by alter-observe-respects-policy,
name/disj-79 is used by alter-observe-respects-policy,
name/disj-83 is used by alter-observe-respects-policy,
name/disj-84 is used by alter-observe-respects-policy,
name/disj-85 is used by alter-observe-respects-policy,
name/disj-86 is used by alter-observe-respects-policy,
name/disj-87 is used by alter-observe-respects-policy,
name/disj-88 is used by alter-observe-respects-policy,
name/disj-91 is used by alter-observe-respects-policy,
name/disj-92 is used by alter-observe-respects-policy,
name/disj-93 is used by alter-observe-respects-policy,
name/disj-94 is used by alter-observe-respects-policy,
name/disj-95 is used by alter-observe-respects-policy,
name/disj-96 is used by alter-observe-respects-policy,
name/disj-97 is used by alter-observe-respects-policy,
name/disj-98 is used by alter-observe-respects-policy,
name/disj-99 is used by alter-observe-respects-policy,
name/inj-20 is used by alter-observe-respects-policy,
name/inj-21 is used by alter-observe-respects-policy,
name/inj-22 is used by alter-observe-respects-policy,