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: |
|---|
| lastoc-C-event-01 | proved | all subs proved
| lastoc-C-event,
projection-C-empty,
|
| projection-VC-C | proved | all subs proved
| projection-in,
projection-in-01,
projection-C-empty,
|
| lastoc-C-event | proved | all subs proved
| projection-one-empty,
projection-append,
projection-empty,
|
| projection-in | proved | all subs proved
| projection-one-01,
projection-append,
|
| projection-VN-unchanged-01 | proved | all subs proved
| projection-VN-unchanged,
projection-C-empty,
|
| projection-VC-C-01 | proved | all subs proved
| Vview,
VCview,
projection-one-if,
projection-one-empty,
projection-append,
projection-empty,
|
| projection-one-01 | proved | all subs proved
| VCview,
projection-one-if,
|
| projection-VN-unchanged | proved | all subs proved
| VNview-def,
projection-one-if,
projection-append,
projection-empty,
|
| projection-in-01 | proved | all subs proved
| Vview,
projection-one-if,
projection-append,
projection-empty,
|
| projection-C-empty | proved | all subs proved
| Cview-def,
projection-one-if,
projection-append,
projection-empty,
|
| projection-one-empty | proved | all subs proved
| Cview-def,
projection-one-if,
|
| projection-one-empty-01 | proved | all subs proved
| Vview-def,
projection-one-if,
|
| projection-one-empty-02 | proved | all subs proved
| Nview-def,
projection-one-if,
|
| projection-one-if | proved | all subs proved
| projection-one-remove,
projection-one-keep,
|
| projection-last-if | proved | all subs proved
| projection-one-remove,
projection-one-keep,
projection-empty,
projection-append,
|
| projection-one-remove | proved | all subs proved
| projection-append,
projection-remove,
|
| prefix-closed | proved | all subs proved
| transex-append,
enabled-def,
in-trace-def,
|
| projection-one | proved | all subs proved
| projection-empty,
projection-one-keep,
VNview-def,
projection-remove,
|
| reachable-trans | proved | all subs proved
| transex-one,
transex-append,
reachable-def,
|
| reachable-transex | proved | all subs proved
| transex-append,
reachable-def,
|
| transex-enabled-intrans | proved | all subs proved
| transex-append,
enabled-def,
in-trace-def,
|
| Vview | proved | all subs proved
| Vview-def,
|
| VCview | proved | all subs proved
| VCview-def,
|
| projection-one-keep | proved | all subs proved
| projection-empty,
projection-keep,
|
| projection-append | proved | all subs proved
| projection-remove,
projection-keep,
projection-empty,
|
| transex-one | proved | all subs proved
| transex-empty,
transex-rec,
|
| transex-append | proved | all subs proved
| transex-rec,
transex-empty,
|
| view-C-VN | proved | all subs proved
| VNview-def,
Cview-def,
|
| transex-empty-01 | proved | all subs proved
| transex-empty,
|
| reachable-transex-01 | proved | all subs proved
| reachable-def,
|
| enabled-transex | proved | all subs proved
| enabled-def,
|
| enabled-empty | proved | all subs proved
| transex-empty,
enabled-def,
|
| Cview | proved | all subs proved
| Cview-def,
|
| transex-rec | axiom | | |
| reachable-def | axiom | | |
| Nview-def | axiom | | |
| projection-keep | axiom | | |
| projection-remove | axiom | | |
| VNview-def | axiom | | |
| in-trace-def | axiom | | |
| projection-empty | axiom | | |
| enabled-def | axiom | | |
| transex-empty | axiom | | |
| Vview-def | axiom | | |
| VCview-def | axiom | | |
| Cview-def | axiom | | |