[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 is-valid-ref-stronger-def
⊦ is_valid_ref(str, r, st) ↔ is_obj(str, r, st) ∨ is_array(str, r, st)
Type: An axiom
Validity: The proof is valid.
Features: localsimp,
Comment:
Used by:
is_valid_ref-addobj
,
is_valid_ref-array
,
is_valid_ref-array-01
,
is_valid_ref-def
,
is_valid_ref-del-01
,
is_valid_ref-isarray
,
is_valid_ref-no-arraytype
,
is_valid_ref-obj
,
is_valid_ref-okbytearray
,
is_valid_ref-put
,
is_valid_ref-put-01
,
is_valid_ref-put-byte
,
is_valid_ref-put-equiv
,
is_valid_ref-put-index
,
is_valid_ref-put-samefield
,
is_valid_ref-put-samefield-01
,
is_valid_ref-putbytearray
,
is_valid_ref-reftype
,
is_valid_ref-type-01
,
is_valid_ref-update
,
isvalidref-put-array-badindex
,
Used by units in proved state:
Proof exists?: No