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: |
|---|
| unchanged-levelsubset-equiv | proved | all subs proved
| unchanged-symmetric,
unchanged-junkref-level,
unchanged-def-keep,
unchanged-def,
unchanged-levelsubset,
|
| unchanged-okbar | proved | all subs proved
| unchanged-null,
unchanged-validref,
unchanged-pathex-unchanged,
|
| unchanged-levelsubset | proved | all subs proved
| unchanged-junkref,
unchanged-def,
unchanged-def-keep,
|
| unchanged-validref | proved | all subs proved
| unchanged-type-01,
unchanged-junkref,
|
| unchanged-cyclic-equiv | proved | all subs proved
| unchanged-junkref,
unchanged-symmetric,
unchanged-cyclic,
|
| unchanged-junkref-level | proved | all subs proved
| unchanged-junkrefs-level,
|
| unchanged-junkref | proved | all subs proved
| unchanged-type-01,
unchanged-junkrefs,
|
| unchanged-junkrefs | proved | all subs proved
| unchNorec-isarray-02,
unchanged-array-forward,
unchNorec-index0,
unchanged-isarray,
unchNorec-length-intro,
unchNorec-isobj-02,
unchanged-class-forward,
unchNorec-field0,
unchanged-isobj,
unchNorec-type-intro,
unchanged-unchNorec-same-01,
unchanged-null,
|
| unchanged-junkrefs-level | proved | all subs proved
| unchNorec-isvalidref-01,
unchNorec-type-intro,
unchanged-array-forward,
unchNorec-isarray-01,
unchNorec-isarray-02,
unchanged-class-forward,
unchNorec-def-keep,
unchNorec-isobj-01,
unchNorec-isobj-02,
unchanged-def-keep,
|
| unchanged-rec-generic | proved | all subs proved
| unchanged-array-forward,
unchanged-class-forward,
|
| unchanged-class-forward | proved | all subs proved
| unchanged-null,
unchanged-pathex-unchanged,
|
| unchanged-array-forward | proved | all subs proved
| unchanged-pathex-unchanged,
unchanged-null,
|
| unchanged-pathex-unchanged | proved | all subs proved
| unchanged-symmetric,
unchanged-pathex-append,
unchanged-def-keep,
unchanged-def,
|
| unchanged-getbar | proved | all subs proved
| unchanged-null,
unchanged-lookup-generic,
unchanged-def,
unchanged-type-01,
unchNorec-index0,
|
| unchanged-pathex-append | proved | all subs proved
| unchanged-validrefs-unchNorec,
unchNorec-validrefs-pathex,
|
| unchanged-lookup-generic | proved | all subs proved
| unchangedNorec-def,
unchanged-def,
unchanged-pathex,
|
| unchanged-cyclic | proved | all subs proved
| unchanged-validrefs-unchNorec,
unchNorec-validrefs-equiv,
|
| unchNorec-junkrefs-equiv | proved | all subs proved
| unchNorec-sym,
unchNorec-junkrefs,
|
| unchNorec-junkrefs | proved | all subs proved
| unchNorec-index0,
unchNorec-length-intro,
unchNorec-isarray-02,
unchNorec-field0,
unchNorec-isobj-02,
unchNorec-type-intro,
|
| unchNorec-validrefs-equiv | proved | all subs proved
| unchNorec-sym,
unchNorec-validrefs,
|
| unchNorec-isvalidref-01 | proved | all subs proved
| unchNorec-isvalidref,
unchNorec-sym,
|
| unchanged-pathex | proved | all subs proved
| unchanged-pathex-unchNorec,
unchNorec-validrefs,
|
| unchNorec-validrefs-pathex | proved | all subs proved
| unchNorec-validrefs,
unchNorec-isvalidref,
|
| unchanged-isobj | proved | all subs proved
| unchNorec-isobj-01,
unchanged-def,
|
| unchanged-isarray | proved | all subs proved
| unchNorec-isarray-01,
unchanged-def,
|
| unchNorec-validrefs | proved | all subs proved
| unchNorec-index0,
unchNorec-isarray-01,
unchNorec-length-intro,
unchNorec-field0,
unchNorec-isobj-01,
unchNorec-type-intro,
|
| unchNorec-isobj-02 | proved | all subs proved
| unchNorec-isobj-01,
unchNorec-sym,
|
| unchNorec-isarray-02 | proved | all subs proved
| unchNorec-isarray-01,
unchNorec-sym,
|
| unchNorec-isvalidref | proved | all subs proved
| unchNorec-isarray-01,
unchNorec-isobj-01,
|
| unchNorec-isarray-01 | proved | all subs proved
| unchNorec-type-intro,
unchNorec-isarray,
|
| unchNorec-isobj-01 | proved | all subs proved
| unchNorec-type-intro,
unchNorec-isobj,
|
| unchanged-type-01 | proved | all subs proved
| unchanged-type,
|
| unchNorec-isobj | proved | all subs proved
| unchNorec-def-keep,
|
| unchNorec-isarray | proved | all subs proved
| unchNorec-def-keep,
|
| pseq-subset-01 | proved | all subs proved
| pseq-subset,
pseq-sym,
|
| unchNorec-transitivity | proved | all subs proved
| unchNorec-type-intro,
unchNorec-def-keep,
unchangedNorec-def,
|
| pseq-sym | proved | all subs proved
| pseq-sym-01,
|
| unchNorec-index0 | proved | all subs proved
| unchNorec-type-intro,
unchNorec-length-intro,
unchNorec-index,
|
| unchNorec-field0 | proved | all subs proved
| unchNorec-type-intro,
unchNorec-field,
|
| unchNorec-def-keep | proved | all subs proved
| unchangedNorec-def,
unchNorec-type-intro,
|
| unchanged-type | proved | all subs proved
| unchNorec-type-intro,
unchanged-def,
|
| unchanged-field-lookup-01 | proved | all subs proved
| unchanged-field-lookup,
|
| unchanged-field-lookup | proved | all subs proved
| unchanged-unchNorec-same,
unchNorec-field,
|
| unchanged-symmetric | proved | all subs proved
| unchNorec-sym,
unchanged-def,
|
| unchanged-validrefs-unchNorec | proved | all subs proved
| unchanged-pathex-unchNorec,
|
| unchanged-null | proved | all subs proved
| unchNorec-null,
unchanged-def,
|
| unchNorec-type-intro | proved | all subs proved
| unchNorec-type,
|
| pseq-sym-01 | proved | all subs proved
| maxpath-array,
pseq-jvmref,
maxpath-object,
pseq-def,
|
| pseq-subset | proved | all subs proved
| pseq-jvmref,
maxpath-array,
maxpath-object,
pseq-def,
|
| cyclic-pseq | proved | all subs proved
| maxpath-array,
maxpath-object,
pseq-def,
|
| getbytearray-pseq | proved | all subs proved
| pseq-def,
getbytearray-pseq-02,
|
| getbytearray-pseq-nojunk | proved | all subs proved
| pseq-def,
getbytearray-pseq-02,
|
| maxpath-array-ls | proved | all subs proved
| maxpath-array,
|
| unchNorec-length | proved | all subs proved
| unchNorec-length-intro,
|
| unchNorec-length0 | proved | all subs proved
| unchNorec-length-intro,
|
| unchNorec-type0 | proved | all subs proved
| unchNorec-type,
|
| unchanged-put-nopathex | proved | all subs proved
| unchNorec-put-nopathex,
unchanged-def,
|
| unchanged-type-in | proved | all subs proved
| unchNorec-null,
unchanged-def,
|
| getbytearray-pseq-02 | proved | all subs proved
| pseq-def,
|
| maxpath-array | proved | all subs proved
| maxpath-max,
validrefset-empty,
validrefset-def,
maxpath-in,
maxpath-zero,
|
| pseq-jvmref | proved | all subs proved
| pseq-def,
|
| maxpath-object | proved | all subs proved
| maxpath-max,
validrefset-empty,
validrefset-def,
maxpath-in,
maxpath-zero,
|
| unchNorec-index | proved | all subs proved
| unchangedNorec-def,
|
| unchNorec-type | proved | all subs proved
| unchangedNorec-def,
|
| unchanged-unchNorec-same | proved | all subs proved
| unchanged-def,
|
| unchNorec-field | proved | all subs proved
| unchangedNorec-def,
|
| unchNorec-length-intro | proved | all subs proved
| unchangedNorec-def,
|
| unchanged-unchNorec-same-01 | proved | all subs proved
| unchanged-def,
|
| unchanged-def-keep | proved | all subs proved
| unchanged-def,
|
| unchNorec-put-nopathex | proved | all subs proved
| unchangedNorec-def,
|
| unchNorec-sym | proved | all subs proved
| unchangedNorec-def,
|
| unchNorec-null | proved | all subs proved
| unchangedNorec-def,
|
| unchanged-pathex-unchNorec | proved | all subs proved
| unchanged-def,
|
| validref-pseq | proved | all subs proved
| pseq-def,
|
| unchNorec-reflexivity | proved | all subs proved
| unchangedNorec-def,
|
| getbytearray-pseq-nojunk-02 | proved | all subs proved
| pseq-def,
|
| unchanged-def | axiom | | |
| unchangedNorec-def | axiom | | |
| maxpath-zero | axiom | | |
| maxpath-in | axiom | | |
| validrefset-def | axiom | | |
| validrefset-empty | axiom | | |
| maxpath-max | axiom | | |
| pseq-def | axiom | | |