[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. 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
,
Theorem alter-observe-respects-policy
⊦ alter(domvar, nam, ag) ∧ observe(domvar0, nam, ag) → domvar ⇒ domvar0
Type: A proof obligation
Validity: The proof is valid.
Features: theorem,
Comment:
Used by:
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 28
Proof steps: 56
Used lemmas:
Used spec theorems:
Used simplifier rules:
dominterference
/
Abort9-interference-def
observeAlter
/
alter-Abort9
dominterference
/
Abort8-interference-def
observeAlter
/
alter-Abort8
domain
/
disj-19
dominterference
/
HighLow5-interference-def
observeAlter
/
alter-HighLow5
name
/
disj-144
name
/
disj-141
name
/
disj-06
name
/
disj-133
name
/
disj-131
name
/
disj-74
name
/
disj-94
name
/
disj-132
name
/
disj-130
name
/
disj-29
observeAlter
/
observe-User
domain
/
disj-18
dominterference
/
User-User_Airline-interference-def
observeAlter
/
alter-User-User_Airline
domain
/
disj-10
domain
/
disj-09
name
/
disj-145
name
/
disj-45
name
/
disj-143
name
/
disj-43
name
/
disj-142
name
/
disj-42
name
/
disj-140
name
/
disj-40
dominterference
/
User_TravelAgency_Airline-interference-def
observeAlter
/
alter-User_TravelAgency_Airline
name
/
disj-51
name
/
disj-25
name
/
disj-136
name
/
disj-36
name
/
disj-134
name
/
disj-34
name
/
disj-72
name
/
disj-26
name
/
disj-92
name
/
disj-27
name
/
disj-28
name
/
disj-111
observeAlter
/
observe-User-User_Airline
domain
/
disj-03
command
/
disj-301
command
/
disj-294
command
/
disj-267
command
/
disj-256
command
/
disj-231
command
/
disj-186
command
/
disj-169
command
/
disj-151
command
/
disj-132
command
/
disj-46
name
/
disj-66
name
/
disj-67
name
/
disj-65
name
/
disj-63
name
/
disj-64
name
/
disj-62
name
/
disj-02
command
/
disj-298
command
/
disj-291
command
/
disj-264
command
/
disj-253
command
/
disj-228
command
/
disj-183
command
/
disj-166
command
/
disj-148
command
/
disj-129
command
/
disj-43
name
/
disj-242
name
/
disj-243
name
/
disj-241
name
/
disj-239
name
/
disj-240
name
/
disj-238
name
/
disj-13
name
/
disj-219
name
/
disj-220
name
/
disj-218
name
/
disj-216
name
/
disj-217
name
/
disj-215
name
/
disj-11
exAgent
/
ex-not-37
command
/
disj-108
command
/
disj-107
command
/
disj-104
command
/
disj-103
command
/
disj-101
command
/
disj-98
command
/
disj-97
command
/
disj-96
command
/
disj-95
command
/
disj-28
command
/
disj-39
command
/
disj-125
command
/
disj-144
command
/
disj-162
command
/
disj-179
command
/
disj-224
command
/
disj-249
command
/
disj-260
command
/
disj-272
command
/
disj-273
domain
/
disj-14
domain
/
disj-13
domain
/
disj-07
domain
/
disj-06
observeAlter
/
observe-Abort9
dominterference
/
User_Airline-interference-def
observeAlter
/
alter-User_Airline
observeAlter
/
observe-HighLow5
domain
/
disj-20
domain
/
disj-16
domain
/
disj-04
command
/
disj-213
command
/
disj-282
command
/
disj-198
name
/
disj-206
name
/
disj-192
name
/
disj-161
name
/
disj-87
name
/
disj-126
name
/
disj-107
name
/
disj-207
name
/
disj-193
name
/
disj-162
name
/
disj-88
name
/
disj-127
name
/
disj-108
name
/
disj-205
name
/
disj-191
name
/
disj-160
name
/
disj-86
name
/
disj-125
name
/
disj-106
command
/
disj-212
command
/
disj-281
command
/
disj-197
name
/
disj-203
name
/
disj-189
name
/
disj-158
name
/
disj-84
name
/
disj-123
name
/
disj-104
name
/
disj-204
name
/
disj-190
name
/
disj-159
name
/
disj-85
name
/
disj-124
name
/
disj-105
name
/
disj-202
name
/
disj-188
name
/
disj-157
name
/
disj-83
name
/
disj-122
name
/
disj-103
command
/
disj-209
command
/
disj-261
command
/
disj-194
command
/
disj-208
command
/
disj-250
command
/
disj-193
name
/
disj-10
name
/
disj-09
name
/
disj-07
name
/
disj-03
name
/
disj-05
name
/
disj-04
command
/
disj-206
command
/
disj-225
command
/
disj-191
command
/
disj-174
command
/
disj-180
command
/
disj-173
command
/
disj-157
command
/
disj-163
command
/
disj-156
command
/
disj-139
command
/
disj-145
command
/
disj-138
command
/
disj-120
command
/
disj-126
command
/
disj-119
command
/
disj-33
command
/
disj-40
command
/
disj-34
exAgent
/
exTravelAgency-s
observeAlter
/
observe-User_TravelAgency_Airline
domain
/
disj-15
domain
/
disj-12
domain
/
disj-02
command
/
disj-217
command
/
disj-286
command
/
disj-202
command
/
disj-214
command
/
disj-283
command
/
disj-199
name
/
disj-197
name
/
disj-183
name
/
disj-152
name
/
disj-78
name
/
disj-117
name
/
disj-98
name
/
disj-198
name
/
disj-184
name
/
disj-153
name
/
disj-79
name
/
disj-118
name
/
disj-99
name
/
disj-196
name
/
disj-182
name
/
disj-151
name
/
disj-77
name
/
disj-116
name
/
disj-97
command
/
disj-210
command
/
disj-271
command
/
disj-195
name
/
disj-55
name
/
disj-54
name
/
disj-52
name
/
disj-48
name
/
disj-50
name
/
disj-49
name
/
disj-115
name
/
disj-114
name
/
disj-112
command
/
disj-100
command
/
disj-106
command
/
disj-99
name
/
inj-20
name
/
disj-71
name
/
inj-22
name
/
disj-73
name
/
disj-75
name
/
disj-76
exAgent
/
exAirline-s
observeAlter
/
observe-User_Airline
domain
/
disj-11
domain
/
disj-08
domain
/
disj-01
domain
/
disj-05
domain
/
disj-17
domain
/
disj-21
observeAlter
/
observe-Abort8
exAgent
/
ex-not-40
exAgent
/
ex-not-36
name
/
disj-91
name
/
disj-70
name
/
disj-93
name
/
disj-95
name
/
disj-96
name
/
inj-21
dominterference
/
User-interference-def
observeAlter
/
alter-User