[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
⊦ is_valid_ref(r, st) ↔ is_obj(r, st) ∨ is_array(r, st)
Type: An axiom
Validity: The proof is valid.
Features:
Comment:
Used by:
is_array-validref
,
is_valid_ref-addobj
,
is_valid_ref-def
,
is_valid_ref-primarray
,
is_valid_ref-put
,
is_valid_ref-putbytearray
,
is_valid_ref-type-typeval
,
is_valid_ref-typeex
,
is_valid_ref-update
,
isvalidref-put-array-badindex
,
reffield-del
,
valid-type-typeval
,
validref-01
,
validref-02
,
validref-addobj
,
validref-del
,
validref-del-01
,
validref-isarray
,
validref-isobj
,
validref-new
,
validref-notin
,
validref-notin-01
,
validref-null
,
validref-primtype
,
validref-primtype-01
,
validref-primtype-02
,
validref-put
,
validref-put-01
,
validref-put-samefield
,
validref-put-samefield-01
,
validref-reftype
,
validref-typeval
,
Used by units in proved state:
Proof exists?: No