[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 flightOffers-no-write-down
⊦ alter(domvar, Airline-flightOffers, mkAirline(0)) → domvar ⇒ dom(Airline-flightOffers, mkAirline(0))
Type: A proof obligation
Validity: The proof is valid.
Features: theorem,
Comment: attribute flightOffers in class Airline has explicit domain User_TravelAgency_Airline.
Used by:
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 1
Proof steps: 2
Used lemmas:
Used spec theorems:
Used simplifier rules:
observeAlter
/
alter-Abort9
observeAlter
/
alter-Abort8
observeAlter
/
alter-HighLow5
name
/
disj-06
observeAlter
/
alter-User-User_Airline
name
/
disj-22
name
/
disj-20
name
/
disj-19
name
/
disj-17
observeAlter
/
alter-User_TravelAgency_Airline
name
/
disj-10
name
/
disj-09
name
/
disj-07
observeAlter
/
alter-User
observeAlter
/
alter-User_Airline
name
/
disj-04
name
/
disj-05
name
/
disj-03
name
/
disj-11
name
/
disj-13
name
/
disj-02
domdefinitions
/
dom-flightOffers