Theorem validrefs-null-02

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: cyclic-addarray-this, cyclic-addobj, cyclic-addrefarray, cyclic-not-null, cyclic-put-statfield, cyclic-put-statfield-01, cyclic-subset, cyclic-subset-01, junkrefs-put-nopathexplus-equiv, pathex-array, pathex-def-simple, pathex-null, pathex-put-nopathex, pathex-put-pathex-array-refval, pathex-validrefs-in, pathexplus-pathex, validref-refs-last-valid-subset, validrefs-addarray, validrefs-addarray-junkref, validrefs-addobj-01, validrefs-addobj-junkref, validrefs-all-same, validrefs-append, validrefs-contains-null, validrefs-delcycle, validrefs-delcycle-01, validrefs-delete-02, validrefs-delete-03, validrefs-has-null, validrefs-junkrefs-append, validrefs-lastelem, validrefs-levelsubset, validrefs-levelsubset-01, validrefs-nodups, validrefs-not, validrefs-postfix, validrefs-prefix, validrefs-primarray, validrefs-primtype, validrefs-put-array-badindex, validrefs-put-badarrayfield, validrefs-put-badarrayfield-01, validrefs-put-badclassfield, validrefs-put-badclassfield-01, validrefs-put-last, validrefs-put-notin, validrefs-put-notin-01, validrefs-put-notin-02, validrefs-put-notin-03, validrefs-put-statfield, validrefs-putbar, validrefs-putbar-01, validrefs-putbyte, validrefs-putbyte-01, validrefs-putbyte-field, validrefs-putshort-field, validrefs-subset, validrefs-subset-01, validrefs-subset-equiv, validrefs-subtype, validrefs-trans-01, validrefs-type,
• 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: validrefs-null, validrefs-null-01,
• Used spec theorems:
  • Used simplifier rules:
    • list/references/a
    • list/references/app