[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 range-del-in
⊦ key ∈ ri ∧ ri[key] = adr ∧ ri-inj(ri) → range(ri -- key) = range ri -- adr
Type: A user defined theorem
Validity: The proof is valid.
Features: s, ls,
Comment:
Used by:
Used by units in proved state:
gjournal-asm
,
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 6
Proof steps: 15
Used lemmas:
Used spec theorems:
set-basic
/node-store/
Extension
store+set
/node-index/
Data-in
aubifs-inv
/
ri-inj
Used simplifier rules:
set-union
/node-store/
Delete
aubifs-base
/
range
store
/node-index/
Del-at
store
/node-index/
Del-in