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: |
|---|
| compat-throw-02 | proved | all subs proved
| value-compat,
modeval-compat,
mode-compat,
compatrefs-mode,
compatstatic-mode,
store-compat,
|
| compatrefs-mode | proved | all subs proved
| compatarray-mode,
compatobj-mode,
refs-compat,
|
| compat-put | proved | all subs proved
| array-compat,
obj-compat,
refs-compat,
fields-compat,
static-compat,
compatval-put,
modeval-compat,
mode-compat,
store-compat,
|
| compat-addclass | proved | all subs proved
| compatval-addclass,
array-compat,
obj-compat,
refs-compat,
value-compat,
fields-compat,
static-compat,
modeval-compat,
mode-compat,
store-compat,
|
| compatobj-mode | proved | all subs proved
| compatfields-mode,
obj-compat,
|
| compatarray-mode | proved | all subs proved
| compatval-noref,
value-compat,
array-compat,
|
| compatstatic-mode | proved | all subs proved
| compatval-noref,
value-compat,
fields-compat,
static-compat,
|
| compatval-put | proved | all subs proved
| compatval-noref,
value-compat,
|
| compatval-addclass | proved | all subs proved
| compatval-noref,
value-compat,
|
| compat-addobj | proved | all subs proved
| compatval-noref,
array-compat,
obj-compat,
refs-compat,
fields-compat,
static-compat,
value-compat,
modeval-compat,
mode-compat,
store-compat,
|
| compatfields-mode | proved | all subs proved
| value-compat,
fields-compat,
|
| compatval-noref | proved | all subs proved
| value-compat,
|
| compatobj-isobj | proved | all subs proved
| value-compat,
fields-compat,
obj-compat,
|
| compatarray-void | proved | all subs proved
| value-compat,
array-compat,
|
| compatarray-isarray-01 | proved | all subs proved
| array-compat,
|
| compatarray-isarray | proved | all subs proved
| value-compat,
array-compat,
|
| compatarray-abstract | proved | all subs proved
| value-compat,
array-compat,
|
| compat-newref | proved | all subs proved
| value-compat,
|
| store-compat | axiom | | |
| mode-compat | axiom | | |
| modeval-compat | axiom | | |
| static-compat | axiom | | |
| fields-compat | axiom | | |
| value-compat | axiom | | |
| refs-compat | axiom | | |
| obj-compat | axiom | | |
| array-compat | axiom | | |