A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas
above its position. This means the list is a topological order of the dependency graph.
An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|
| junkref-update-equiv | proved | all subs proved
| pathex-array,
pathex-class,
pathex-one,
pathex-not-is-validref-01,
junkref-update,
|
| pathex-putbar-02 | proved | all subs proved
| pathex-putbar-01,
|
| junkref-update | proved | all subs proved
| nopathex-update,
junkref-put-nopathex,
|
| pathex-putbar-01 | proved | all subs proved
| pathex-putbar-03,
|
| validref-nopathex-put | proved | all subs proved
| junkref-put-nopathex-equiv-01,
|
| junkref-put-nopathex-equiv-01 | proved | all subs proved
| junkrefs-put-nopathex-equiv,
junkrefs-put-nopathex,
|
| pathex-putbar-03 | proved | all subs proved
| pathex-putbyteval,
|
| nopathex-update | proved | all subs proved
| junkref-put-nopathex,
pathex-put-last,
|
| cyclic-put-nopathex | proved | all subs proved
| validrefs-nopathex-01,
validrefs-not,
pathex-put-last,
validrefs-nopathex,
pathex-one,
validrefs-put-notin,
cyclic-def-shortest,
|
| cyclic-putbar | proved | all subs proved
| cyclic-putbyte-01,
|
| cyclic-putbar-02 | proved | all subs proved
| cyclic-putbar-01,
|
| cyclic-putbar-03 | proved | all subs proved
| cyclic-putbar-01,
|
| junkref-put-nopathexplus-equiv | proved | all subs proved
| junkrefs-put-nopathexplus-equiv,
|
| pathex-levelsubset-equiv | proved | all subs proved
| pathex-levelsubset,
pathex-levelsubset-01,
|
| cyclic-putbyte-01 | proved | all subs proved
| validrefs-putbyte,
cyclic-def-shortest,
cyclic-def-simple,
cyclic-putbyte,
|
| cyclic-putbar-01 | proved | all subs proved
| cyclic-putbar-04,
|
| junkrefs-put-nopathex-equiv | proved | all subs proved
| pathex-array,
pathex-class,
pathex-one,
junkrefs-put-nopathex,
|
| junkrefs-put-nopathexplus-equiv | proved | all subs proved
| validrefs-array,
validrefs-null-02,
validrefs-sametype,
validrefs-superclass,
validrefs-class,
step-exists-def,
validrefs-one,
pathex-plus-def,
pathexplus-pathex,
junkrefs-put-nopathex,
|
| junkref-put-nopathex | proved | all subs proved
| junkrefs-put-nopathex,
|
| pathex-put-last | proved | all subs proved
| validrefs-put-last,
pathex-one,
pathex-def-nodups,
|
| pathex-levelsubset-01 | proved | all subs proved
| validrefs-levelsubset-01,
pathex-def-simple,
pathex-one,
pathex-def-nodups,
|
| pathex-putbyteval | proved | all subs proved
| pathex-putbyteval-01,
|
| pathex-putshortfield-01 | proved | all subs proved
| pathex-putshortfield,
|
| pathex-putbyte-field-01 | proved | all subs proved
| pathex-putbyte-field,
|
| pathex-putbar | proved | all subs proved
| pathex-putbyte,
|
| pathex-put-pathex-array-refval | proved | all subs proved
| validrefs-null-02,
pathex-array,
pathex-trans,
validrefs-postfix,
pathex-def-simple,
validrefs-one,
pathex-not-is-validref-01,
pathex-validrefs-in,
validrefs-is-junk,
validrefs-array,
validrefs-put-notin,
pathex-not-is-validref-02,
pathex-one,
pathex-def-nodups,
|
| pathex-put-cyclic | proved | all subs proved
| validrefs-primtype,
validrefs-superclass,
validrefs-put-notin-02,
validrefs-is-junk,
validrefs-postfix,
validrefs-one,
validrefs-class,
pathex-one,
pathex-def-nodups,
cyclic-def-simple,
|
| pathex-junkref-02 | proved | all subs proved
| pathex-junkref-01,
|
| cyclic-put-statfield-01 | proved | all subs proved
| validrefs-sametype,
validrefs-null-02,
validrefs-put-statfield,
cyclic-def-simple,
cyclic-put-statfield,
|
| pathex-putshortfield | proved | all subs proved
| validrefs-putshort-field,
pathex-one,
pathex-def,
|
| pathex-putbyteval-01 | proved | all subs proved
| validrefs-putbyte-01,
pathex-one,
pathex-def,
|
| pathex-putbyte-field | proved | all subs proved
| validrefs-putbyte-field,
pathex-one,
pathex-def,
|
| pathex-putbyte | proved | all subs proved
| validrefs-putbyte,
validrefs-putbyte-01,
pathex-def-simple,
|
| pathex-def-nodups | proved | all subs proved
| validrefs-delcycle-01,
validrefs-nodups-01,
pathex-def-simple,
|
| pathex-junkref-01 | proved | all subs proved
| pathex-junkref,
|
| junkrefs-put-nopathex | proved | all subs proved
| pathex-array,
pathex-class,
pathex-one,
|
| cyclic-putbyte | proved | all subs proved
| validrefs-putbyte-01,
cyclic-def-simple,
|
| cyclic-putbar-04 | proved | all subs proved
| validrefs-putbar,
cyclic-def,
|
| cyclic-put-statfield | proved | all subs proved
| cyclic-not-null,
validrefs-null-02,
validrefs-put-statfield,
cyclic-def-simple,
|
| validrefs-nopathex-01 | proved | all subs proved
| validrefs-nopathex,
|
| cyclic-addobj | proved | all subs proved
| validrefs-one,
validrefs-type,
validrefs-sametype,
validrefs-addobj,
validrefs-addobj-junkref,
cyclic-not-null,
validrefs-null-02,
validrefs-class,
validrefs-is-junk,
validrefs-null,
cyclic-def-simple,
|
| cyclic-addobj-other-01 | proved | all subs proved
| validrefs-newref,
validrefs-addobj-notin,
cyclic-def-simple,
cyclic-addobj-other,
|
| cyclic-addrefarray | proved | all subs proved
| cyclic-not-null,
validrefs-null-02,
validrefs-sametype,
validrefs-addarray,
validrefs-addarray-junkref,
validrefs-array,
validrefs-is-junk,
cyclic-def-simple,
|
| cyclic-put-badarrayfield | proved | all subs proved
| validrefs-put-badarrayfield-01,
validrefs-put-badarrayfield,
cyclic-def-shortest,
|
| cyclic-put-badclassfield | proved | all subs proved
| validrefs-put-badclassfield-01,
validrefs-put-badclassfield,
cyclic-def-shortest,
|
| cyclic-putbar-05 | proved | all subs proved
| validrefs-putbar,
cyclic-def,
|
| exvalidrefs | proved | all subs proved
| validrefs-delete-01,
validrefs-delete,
validrefs-del-junkrefs,
validrefs-one,
cyclic-def-simple,
validrefs-null-01,
validrefs-class,
|
| exvalidrefs-03 | proved | all subs proved
| validrefs-null-01,
validrefs-delete-01,
validrefs-del-junkrefs,
validrefs-one,
validrefs-class,
cyclic-def-simple,
|
| exvalidrefs-maxlength | proved | all subs proved
| validrefs-del,
validrefs-delete-02,
validrefs-array,
validrefs-delete,
validrefs-newref,
validrefs-del-junkrefs,
validrefs-delete-01,
validrefs-class,
cyclic-def-simple,
validrefs-one,
validrefs-null-01,
cyclic-not-null,
|
| exvalidrefs-nodups | proved | all subs proved
| validrefs-null-01,
validrefs-delete-01,
validrefs-del-junkrefs,
validrefs-one,
validrefs-class,
cyclic-def-simple,
|
| okarray-put-nopath-01 | proved | all subs proved
| okarray-put-nopath,
pathex-lookup-put-other,
|
| pathex-no-newref | proved | all subs proved
| pathex-not-is-validref,
|
| pathex-put-nopathex | proved | all subs proved
| validrefs-sametype,
pathex-array,
validrefs-array,
pathex-null,
pathex-class,
validrefs-null-02,
validrefs-sametype-03,
pathex-one,
validrefs-class,
validrefs-null,
validrefs-is-junk,
pathex-def-simple,
|
| pathex-putstatfield-01 | proved | all subs proved
| pathex-putstatfield,
|
| pathex-subset-equiv | proved | all subs proved
| pathex-subset-02,
validrefs-subset-equiv,
pathex-one,
pathex-def,
|
| validrefs-bytearray-01 | proved | all subs proved
| validrefs-bytearray,
validrefs-empty,
|
| cyclic-addobj-other | proved | all subs proved
| validrefs-addobj-junkref,
validrefs-addobj,
cyclic-def-simple,
|
| validrefs-putbar | proved | all subs proved
| validrefs-null-01,
validrefs-primtype-01,
validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| cyclic-def-shortest | proved | all subs proved
| validrefs-prefix,
cyclic-def-simple,
|
| cyclic-not-null | proved | all subs proved
| validrefs-null-02,
validrefs-empty,
cyclic-def-simple,
|
| validrefs-delete-01 | proved | all subs proved
| validrefs-superclass,
validrefs-delete,
|
| okarray-put-nopath | proved | all subs proved
| pathex-one,
|
| pathex-lookup-put-other | proved | all subs proved
| pathex-one,
|
| validrefs-nodups-01 | proved | all subs proved
| validrefs-delcycle-01,
|
| pathex-junkref | proved | all subs proved
| validrefs-junkrefs-append,
pathex-def-simple,
|
| pathex-not-is-validref | proved | all subs proved
| validrefs-not-in,
validrefs-one,
pathex-def-simple,
|
| pathex-class | proved | all subs proved
| validrefs-superclass,
validrefs-null-01,
validrefs-sametype,
validrefs-null,
validrefs-is-junk,
validrefs-class,
pathex-def-simple,
|
| pathex-array | proved | all subs proved
| validrefs-superclass,
validrefs-null-01,
validrefs-null-02,
validrefs-sametype,
validrefs-is-junk,
validrefs-array,
pathex-def-simple,
|
| pathex-trans | proved | all subs proved
| validrefs-trans,
pathex-def,
|
| pathex-not-is-validref-01 | proved | all subs proved
| validrefs-not-in-01,
pathex-def-simple,
|
| validrefs-putbyte-field | proved | all subs proved
| validrefs-primtype-01,
validrefs-one,
validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| validrefs-putbyte-01 | proved | all subs proved
| validrefs-primtype-01,
validrefs-one,
validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-putshort-field | proved | all subs proved
| validrefs-primtype-02,
validrefs-one,
validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| pathex-putstatfield | proved | all subs proved
| validrefs-put-statfield,
validrefs-one,
pathex-one,
pathex-def,
|
| pathex-subset-02 | proved | all subs proved
| pathex-subset,
|
| validrefs-bytearray | proved | all subs proved
| validrefs-one,
validrefs-primtype-01,
validrefs-array,
validrefs-is-junk,
validrefs-null,
|
| validrefs-nopathex | proved | all subs proved
| validrefs-prefix,
pathex-def-simple,
validrefs-sametype,
|
| validrefs-subset-equiv-01 | proved | all subs proved
| validrefs-subset-equiv,
|
| validrefs-putbar-01 | proved | all subs proved
| validrefs-one,
validrefs-primtype-01,
validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| validrefs-nodups | proved | all subs proved
| validrefs-contains-null,
validrefs-null-01,
validrefs-delcycle,
validrefs-null-02,
|
| validrefs-applast-class-null | proved | all subs proved
| validrefs-null-01,
validrefs-class,
validrefs-append-01,
|
| validrefs-applast-class | proved | all subs proved
| validrefs-one,
validrefs-class,
validrefs-append-01,
|
| validrefs-applast-array-null | proved | all subs proved
| validrefs-null-01,
validrefs-array,
validrefs-append-01,
|
| validrefs-applast-array | proved | all subs proved
| validrefs-one,
validrefs-array,
validrefs-append-01,
|
| validref-nopath-superset | proved | all subs proved
| validrefs-subset-notnew,
validrefs-one,
pathex-def,
|
| pathex-subset-01 | proved | all subs proved
| pathex-subset,
|
| pathex-put-array-badindex | proved | all subs proved
| validrefs-put-array-badindex,
pathex-def-simple,
|
| pathex-null-01 | proved | all subs proved
| pathex-one,
pathex-null,
|
| pathex-noreftype | proved | all subs proved
| validrefs-postfix,
validrefs-primtype,
pathex-def-simple,
|
| pathex-addobj | proved | all subs proved
| validrefs-superclass,
validrefs-subtype,
validrefs-addobj-01,
pathex-def,
|
| cyclic-subset-01 | proved | all subs proved
| validrefs-subset-01,
validrefs-null-02,
cyclic-def-simple,
|
| cyclic-subset | proved | all subs proved
| validrefs-null-02,
validrefs-subset,
cyclic-def-simple,
|
| cyclic-one | proved | all subs proved
| validrefs-one,
validrefs-class,
cyclic-def-simple,
|
| cyclic-delete | proved | all subs proved
| validrefs-delete,
validrefs-delete-02,
cyclic-def-simple,
|
| cyclic-class | proved | all subs proved
| validrefs-superclass,
validrefs-class,
cyclic-def-simple,
|
| cyclic-array | proved | all subs proved
| validrefs-superclass,
validrefs-array,
cyclic-def-simple,
|
| cyclic-addarray-this-01 | proved | all subs proved
| validrefs-sametype,
validrefs-superset-junkref,
validrefs-addarray,
validrefs-array,
validrefs-is-junk,
cyclic-def-simple,
|
| cyclic-addarray-this | proved | all subs proved
| validrefs-null-02,
validrefs-array,
validrefs-is-junk,
cyclic-def-simple,
|
| cyclic-addarray-other | proved | all subs proved
| validrefs-addarray-junkref,
validrefs-addarray,
cyclic-def-simple,
|
| cyclic-addarray-noreftype | proved | all subs proved
| validrefs-array,
validrefs-is-junk,
validrefs-null,
cyclic-def-simple,
|
| validrefs-primtype-02 | proved | all subs proved
| validrefs-primtype,
|
| validrefs-delcycle | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null,
validrefs-superclass,
validrefs-null-02,
validrefs-is-junk,
validrefs-postfix,
|
| validrefs-primtype-01 | proved | all subs proved
| validrefs-primtype,
|
| validrefs-append-01 | proved | all subs proved
| validrefs-append,
|
| validrefs-subset-notnew | proved | all subs proved
| validref-refs-last-valid-subset,
|
| validrefs-trans | proved | all subs proved
| validrefs-trans-01,
|
| validrefs-subset-equiv | proved | all subs proved
| validrefs-subset-01,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null-02,
|
| pathex-subset | proved | all subs proved
| validrefs-subset-01,
pathex-def,
|
| pathex-not-is-validref-02 | proved | all subs proved
| validrefs-not,
pathex-def,
|
| pathex-validrefs-in | proved | all subs proved
| validrefs-null-02,
validrefs-is-junk,
validrefs-superclass,
validrefs-prefix,
pathex-def,
|
| validrefs-not-in-01 | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-not,
|
| pathex-levelsubset | proved | all subs proved
| validrefs-levelsubset,
pathex-def,
|
| validrefs-delcycle-01 | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-superclass,
validrefs-null-02,
validrefs-is-junk,
validrefs-postfix,
|
| pathex-def-simple | proved | all subs proved
| validrefs-not,
validrefs-null-02,
validrefs-is-junk,
validrefs-superclass,
validrefs-sametype,
pathex-def,
|
| validrefs-addobj-01 | proved | all subs proved
| validrefs-primtype,
validrefs-type,
validrefs-null-02,
validrefs-is-junk,
validrefs-addobj-new,
validrefs-class,
|
| pathexplus-pathex | proved | all subs proved
| validrefs-prefix,
validrefs-array,
validrefs-class,
step-exists-def,
validrefs-postfix,
validrefs-not,
validrefs-null-02,
validrefs-is-junk,
pathex-def,
pathex-plus-def,
|
| pathex-one | proved | all subs proved
| validrefs-one,
validrefs-null-01,
validrefs-not,
pathex-def,
|
| validrefs-delete | proved | all subs proved
| validrefs-null-01,
validrefs-array,
validrefs-class,
validrefs-delete-02,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-superset-junkref | proved | all subs proved
| validrefs-newref,
validrefs-subset,
|
| cyclic-def-simple | proved | all subs proved
| validrefs-array,
validrefs-is-junk,
validrefs-null,
cyclic-def,
cyclic-def-object,
|
| validrefs-maxlen | proved | all subs proved
| validrefs-array,
validrefs-delete-03,
validrefs-class,
validrefs-is-junk,
validrefs-null,
|
| validrefs-primtype-03 | proved | all subs proved
| validrefs-primtype,
|
| validrefs-put-notin-01 | proved | all subs proved
| validrefs-null-02,
validrefs-not,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-one,
|
| validrefs-put-notin-03 | proved | all subs proved
| validrefs-not,
validrefs-array,
validrefs-put-notin,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| validrefs-void | proved | all subs proved
| validrefs-primtype,
validrefs-null-01,
validrefs-empty,
|
| validrefs-addobj-junkref | proved | all subs proved
| validrefs-array,
validrefs-null-02,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-addarray | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-addarray-junkref | proved | all subs proved
| validrefs-array,
validrefs-null-02,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| cyclic-def-object | proved | all subs proved
| validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-sametype,
cyclic-def,
|
| validrefs-put-badarrayfield-01 | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null-02,
|
| validrefs-put-badarrayfield | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| validrefs-put-badclassfield-01 | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| validrefs-put-badclassfield | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
validrefs-null-01,
validrefs-one,
validrefs-empty,
|
| validrefs-del-junkrefs | proved | all subs proved
| validrefs-array,
validrefs-one,
validrefs-null-01,
validrefs-class,
validrefs-null,
|
| validrefs-subtype | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| validrefs-junkrefs-append | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
|
| validrefs-levelsubset | proved | all subs proved
| validrefs-class,
validrefs-array,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-levelsubset-01 | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-put-array-badindex | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-01,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-put-notin-02 | proved | all subs proved
| validrefs-null-02,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-one,
|
| validrefs-put-last | proved | all subs proved
| validrefs-array,
validrefs-null-01,
validrefs-one,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| pathex-null | proved | all subs proved
| validrefs-null-02,
pathex-def,
|
| validrefs-sametype-03 | proved | all subs proved
| validrefs-sametype,
|
| validrefs-putbyte | proved | all subs proved
| validrefs-one,
validrefs-class,
validrefs-array,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-put-statfield | proved | all subs proved
| validrefs-null-01,
validrefs-null-02,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-type | proved | all subs proved
| validrefs-one,
validrefs-class,
validrefs-array,
validrefs-null-02,
validrefs-is-junk,
|
| validrefs-addobj-new | proved | all subs proved
| validrefs-newref,
validrefs-addobj-notin,
|
| validrefs-append | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-sametype,
validrefs-superclass,
validrefs-null-02,
validrefs-one,
|
| validrefs-postfix | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
validrefs-sametype,
|
| validrefs-delete-02 | proved | all subs proved
| validrefs-null-02,
validrefs-is-junk,
validrefs-null-01,
|
| validrefs-delete-03 | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-contains-null | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-null-01,
validrefs-null-02,
|
| validrefs-prefix | proved | all subs proved
| validrefs-null-02,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-not | proved | all subs proved
| validrefs-null-02,
validrefs-is-junk,
validrefs-null-01,
|
| validrefs-put-notin | proved | all subs proved
| validrefs-null-02,
validrefs-null-01,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-subset-01 | proved | all subs proved
| validrefs-null-01,
validrefs-array,
validrefs-null-02,
validrefs-class,
validrefs-is-junk,
validrefs-null,
|
| validref-refs-last-valid-subset | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
|
| validrefs-subset | proved | all subs proved
| validrefs-null-01,
validrefs-array,
validrefs-null-02,
validrefs-class,
validrefs-is-junk,
validrefs-null,
|
| validrefs-trans-01 | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-superclass,
validrefs-null-02,
validrefs-one,
validrefs-sametype,
validrefs-empty,
|
| validrefs-primtype | proved | all subs proved
| validrefs-null-02,
validrefs-is-junk,
validrefs-null-01,
validrefs-empty,
|
| validrefs-sametype-02 | proved | all subs proved
| validrefs-sametype,
|
| validrefs-sametype-01 | proved | all subs proved
| validrefs-sametype,
|
| validrefs-primarray | proved | all subs proved
| validrefs-array,
validrefs-null,
validrefs-null-01,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-object | proved | all subs proved
| validrefs-sametype,
|
| validrefs-lastelem | proved | all subs proved
| validrefs-one,
validrefs-array,
validrefs-null-02,
validrefs-empty,
validrefs-class,
validrefs-is-junk,
validrefs-null,
|
| validrefs-junkrefs-01 | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-one,
validrefs-empty,
|
| validrefs-junkrefs | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-one,
validrefs-empty,
|
| validrefs-has-null | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-null-02,
|
| validrefs-all-same | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-null-02,
validrefs-is-junk,
validrefs-empty,
|
| validrefs-del | proved | all subs proved
| validrefs-newref,
|
| validrefs-superclass | proved | all subs proved
| validrefs-null-01,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-addobj-notin | proved | all subs proved
| validrefs-null-01,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-addobj | proved | all subs proved
| validrefs-null-01,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-one | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null-01,
|
| validrefs-sametype | proved | all subs proved
| validrefs-null-01,
validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
|
| validrefs-null-02 | proved | all subs proved
| validrefs-null,
validrefs-null-01,
|
| validrefs-not-typeex | proved | all subs proved
| validrefs-not-in,
|
| validrefs-set-null | proved | all subs proved
| validrefs-array,
validrefs-null-01,
validrefs-class,
validrefs-is-junk,
validrefs-null,
|
| validrefs-not-in | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
|
| validrefs-newref | proved | all subs proved
| validrefs-array,
validrefs-class,
validrefs-is-junk,
validrefs-null,
validrefs-empty,
|
| validrefs-null-01 | proved | all subs proved
| validrefs-null,
|
| okbar-nopath | proved | all subs proved
| validrefs-array,
pathex-def,
|
| pathex-def | axiom | | |
| pathex-plus-def | axiom | | |
| step-exists-def | axiom | | |
| validrefs-empty | axiom | | |
| cyclic-def | axiom | | |
| validrefs-class | axiom | | |
| validrefs-null | axiom | | |
| validrefs-is-junk | axiom | | |
| validrefs-array | axiom | | |