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: |
|---|
| subst-SS-equal | proved | all subs proved
| not-value-02,
subst-Carg,
substap-is-not-S,
subst-Cfun,
subst-O,
|
| subst-SK-equal | proved | all subs proved
| not-value-02,
substap-is-not-K,
not-value,
subst-Carg,
substap-is-not-S,
subst-Cfun,
subst-O,
|
| subst-KK-equal | proved | all subs proved
| not-value,
subst-Carg,
substap-is-not-K,
subst-Cfun,
subst-O,
|
| not-value-01 | proved | all subs proved
| not-value,
|
| not-value-02 | proved | all subs proved
| subst-Carg,
ap-in-context-is-ap,
substap-is-not-S,
substap-is-not-K,
subst-Cfun,
subst-O,
|
| not-value | proved | all subs proved
| subst-Carg,
ap-in-context-is-ap,
substap-is-not-S,
substap-is-not-K,
subst-Cfun,
subst-O,
|
| value-context | proved | all subs proved
| subst-Carg,
K-is-only-OK,
S-is-only-OS,
subst-Cfun,
subst-O,
|
| ap-in-context-is-ap | proved | all subs proved
| subst-Carg,
subst-Cfun,
subst-O,
|
| substap-is-not-K | proved | all subs proved
| subst-Carg,
subst-Cfun,
subst-O,
|
| substap-is-not-S | proved | all subs proved
| subst-Carg,
subst-Cfun,
subst-O,
|
| K-is-only-OK | proved | all subs proved
| subst-Carg,
subst-Cfun,
subst-O,
|
| S-is-only-OS | proved | all subs proved
| subst-Carg,
subst-Cfun,
subst-O,
|
| subst-O | axiom | | |
| subst-Cfun | axiom | | |
| subst-Carg | axiom | | |