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: |
|---|
| refines-product | proved | all subs proved
| frag-repla-sametrace,
repl-exec,
|
| repl-exec | proved | all subs proved
| frag-repls-head,
repl-frag,
|
| frag-repla-sametrace | proved | all subs proved
| mon-repla-1,
replstate-inf-def,
replaction-inf-def,
repl-frag,
replaction-fin-def,
finfrag-repla-sametrace-1,
|
| repl-frag | proved | all subs proved
| repl-fin-size,
repl-size,
mon-repla,
mon-repls,
replaction-inf-def,
replstate-inf-def,
finfrag-repl-frag,
replaction-fin-def,
replstate-fin-def,
|
| frag-repls-head | proved | all subs proved
| lift-rec,
lift-base,
repls-infrec-addboth,
repls-base,
mon-repls,
replstate-inf,
nounsharedextR-notcodren-internal,
repls-infrec-skip,
repls-infrec-addS,
finfrag-repls-head,
replstate-fin-def,
|
| finfrag-repl-frag | proved | all subs proved
| product-ok-refine-cext-imp-aext,
lift-get,
lift-base,
lift-rec,
lift-size,
repla-rec-addboth,
repls-rec-addboth,
nounsharedextR-notcodren-internal,
repla-rec-skip,
repls-rec-skip,
sameshared-notcodc-notcoda,
finfrag-repls-head,
repla-rec-addS,
repls-rec-addS,
repla-base,
repls-base,
|
| repl-size | proved | all subs proved
| mon-repla,
mon-repls,
replaction-inf-def,
replstate-inf-def,
replaction-fin-def,
repl-fin-size,
replstate-fin-def,
|
| repls-infrec-addS | proved | all subs proved
| mon-repls,
repls-mon,
repls-base,
repls-rec-addS,
replstate-inf-def,
replstate-inf,
|
| repls-infrec-skip | proved | all subs proved
| repls-rec-skip,
mon-repls,
replstate-inf-def,
nounsharedextR-notcodren-internal,
replstate-inf,
|
| finfrag-repla-sametrace-1 | proved | all subs proved
| finfrag-repla-sametrace,
|
| mon-repla-1 | proved | all subs proved
| mon-repla,
|
| repla-infrec-addS | proved | all subs proved
| mon-repla,
repla-mon,
repla-base,
repla-rec-addS,
replaction-inf-def,
replaction-inf,
|
| repla-infrec-skip | proved | all subs proved
| repla-rec-skip,
mon-repla,
replaction-inf-def,
nounsharedextR-notcodren-internal,
replaction-inf,
|
| repl-fin-size | proved | all subs proved
| repla-rec-addboth,
lift-size,
repls-rec-addboth,
nounsharedextR-notcodren,
repla-rec-skip,
repls-rec-skip,
repla-rec-addS,
repls-rec-addS,
repla-base,
repls-base,
|
| repls-infrec-addboth | proved | all subs proved
| repls-rec-addboth,
repls-mon,
replstate-inf-def,
replstate-inf,
|
| mon-repls | proved | all subs proved
| repls-mon,
|
| finfrag-repla-sametrace | proved | all subs proved
| repla-rec-addboth,
nounsharedextR-notcodren,
nounsharedextR-notcodren-project,
repla-rec-skip,
same-concrete-abstract,
repla-rec-addS,
repla-base,
|
| mon-repla | proved | all subs proved
| repla-mon,
|
| finfrag-repls-head | proved | all subs proved
| lift-rec,
lift-base,
repls-rec-addboth,
repls-rec-skip,
nounsharedextR-notcodren,
repls-rec-addS,
repls-base,
|
| repla-infrec-addboth | proved | all subs proved
| repla-rec-addboth,
repla-mon,
replaction-inf-def,
replaction-inf,
|
| nounsharedextR-notcodren-project | proved | all subs proved
| nounsharedextR-notcodren-internal,
|
| repls-mon | proved | all subs proved
| nounsharedextR-notcodren-internal,
lift-rec,
lift-base,
repls-rec-addboth,
repls-rec-skip,
repls-rec-addS,
repls-base,
|
| nounsharedextR-notcodren | proved | all subs proved
| nounsharedextR-notcodren-internal,
|
| repla-mon | proved | all subs proved
| repla-rec-addboth,
nounsharedextR-notcodren-internal,
repla-rec-skip,
repla-rec-addS,
repla-base,
|
| replstate-inf | proved | all subs proved
| replstate-inf-def,
|
| replaction-inf | proved | all subs proved
| replaction-inf-def,
|
| sameshared-notcodc-notcoda | proved | all subs proved
| sameshared-def,
|
| nounsharedextR-notcodren-internal | proved | all subs proved
| nounsharedextR-def,
|
| lift-size | proved | all subs proved
| lift-rec,
lift-base,
|
| lift-get | proved | all subs proved
| lift-base,
lift-rec,
|
| sameshared-def | axiom | | |
| same-concrete-abstract | proved | all subs proved
| |
| nounsharedextR-def | axiom | | |
| replstate-fin-def | axiom | | |
| replaction-fin-def | axiom | | |
| replstate-inf-def | axiom | | |
| replaction-inf-def | axiom | | |
| repls-base | axiom | | |
| repla-base | axiom | | |
| repls-rec-addS | axiom | | |
| repla-rec-addS | axiom | | |
| repls-rec-skip | axiom | | |
| repla-rec-skip | axiom | | |
| repls-rec-addboth | axiom | | |
| repla-rec-addboth | axiom | | |
| lift-rec | axiom | | |
| lift-base | axiom | | |
| product-ok-refine-cext-imp-aext | proved | all subs proved
| |