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: |
|---|
| proj-exec | proved | all subs proved
| proj-exec-inf,
projstate-inf-def,
projaction-inf-def,
projaction-fin-def,
projstate-fin-def,
proj-exec-fin,
|
| proj-exec-inf | proved | all subs proved
| inffrag-pis-lim-init,
finfrag-pi-step,
inffrag-size-pis-pia,
inffrag-lim-size-pis-pia,
mon-pia,
mon-pis,
projaction-inf-def,
projstate-inf-def,
|
| inffrag-lim-size-pis-pia | proved | all subs proved
| inffrag-size-pis-pia,
mon-pis,
mon-pia,
|
| inffrag-pis-lim-init | proved | all subs proved
| projstate-base,
mon-pis,
|
| projstate-infrec-addboth | proved | all subs proved
| mon-pis,
pis-mon,
projstate-rec-addboth,
projstate-base,
projstate-rec-addboth-one,
pis-inf-simp,
|
| projstate-infrec-addR | proved | all subs proved
| mon-pis,
pis-mon,
projstate-rec-addR,
projstate-base,
projstate-rec-addR-one,
pis-inf-simp,
|
| proj-exec-fin | proved | all subs proved
| projaction-rec-addboth,
projstate-rec-addboth,
projaction-rec-addR,
projstate-rec-addR,
projaction-rec-skipL,
projstate-rec-skipL,
finfrag-pis-nonempty,
projaction-base,
projstate-base,
finfrag-init,
finfrag-pis-init,
|
| finfrag-pi-step | proved | all subs proved
| projaction-rec-addboth,
projstate-rec-addboth,
finfrag-init,
projaction-rec-addR,
projstate-rec-addR,
projaction-rec-skipL,
projstate-rec-skipL,
projstate-base,
|
| mon-pis | proved | all subs proved
| pis-mon,
|
| proj-prefix | proved | all subs proved
| mon-pia,
projaction-inf-def,
|
| projaction-infrec-addboth | proved | all subs proved
| mon-pia,
pia-mon,
projaction-rec-addboth,
projaction-base,
projaction-rec-addboth-one,
pia-inf-simp,
|
| projaction-infrec-addR | proved | all subs proved
| mon-pia,
projaction-rec-addR,
pia-mon,
projaction-base,
projaction-rec-addR-one,
pia-inf-simp,
|
| projstate-infrec-skipL | proved | all subs proved
| pis-mon,
projstate-rec-skipL,
projstate-base,
projstate-rec-skipL-one,
pis-inf-simp,
|
| finfrag-pis-nonempty | proved | all subs proved
| finfrag-pis-init,
|
| finfrag-init | proved | all subs proved
| finfrag-pis-init,
|
| mon-pia | proved | all subs proved
| pia-mon,
|
| pis-mon | proved | all subs proved
| projstate-rec-addboth,
projstate-rec-addR,
projstate-rec-skipL,
projstate-rec-addboth-one,
projstate-rec-addR-one,
projstate-rec-skipL-one,
projstate-base,
|
| pcont-pis | proved | all subs proved
| pmon-pis,
lifted-pis,
|
| pcont-pia | proved | all subs proved
| pmon-pia,
lifted-pia,
|
| projaction-infrec-skipL | proved | all subs proved
| projaction-rec-skipL,
pia-mon,
projaction-base,
projaction-rec-skipL-one,
pia-inf-simp,
|
| projaction-rec-skipL-one | proved | all subs proved
| projaction-base,
projaction-rec-skipL,
|
| projstate-rec-addR-one | proved | all subs proved
| projstate-rec-addR,
projstate-base,
|
| projstate-rec-skipL-one | proved | all subs proved
| projstate-base,
projstate-rec-skipL,
|
| projaction-rec-addR-one | proved | all subs proved
| projaction-base,
projaction-rec-addR,
|
| inffrag-size-pis-pia | proved | all subs proved
| projaction-rec-addboth,
projstate-rec-addboth,
projaction-rec-addR,
projstate-rec-addR,
projaction-rec-skipL,
projstate-rec-skipL,
projaction-base,
projstate-base,
|
| pia-inf-simp | proved | all subs proved
| projaction-inf-def,
|
| projaction-rec-addboth-one | proved | all subs proved
| projaction-base,
projaction-rec-addboth,
|
| pis-inf-simp | proved | all subs proved
| projstate-inf-def,
|
| projstate-rec-addboth-one | proved | all subs proved
| projstate-base,
projstate-rec-addboth,
|
| pia-mon | proved | all subs proved
| projaction-rec-addboth,
projaction-rec-addR,
projaction-rec-skipL,
projaction-base,
|
| finfrag-pis-init | proved | all subs proved
| projstate-rec-addboth,
projstate-rec-addR,
projstate-rec-skipL,
projstate-base,
|
| lifted-pia | proved | all subs proved
| projaction-inf-def,
projaction-fin-def,
|
| pmon-pia | proved | all subs proved
| projaction-rec-addboth,
projaction-rec-addR,
projaction-rec-skipL,
projaction-base,
|
| lifted-pis | proved | all subs proved
| projstate-inf-def,
projstate-fin-def,
|
| pmon-pis | proved | all subs proved
| projstate-rec-addboth,
projstate-rec-addR,
projstate-rec-skipL,
projstate-base,
|
| inffrag-pis-init | proved | all subs proved
| projstate-rec-addboth,
projstate-rec-addR,
projstate-rec-skipL,
projstate-base,
|
| projaction-fin-def | axiom | | |
| projstate-fin-def | axiom | | |
| projstate-inf-def | axiom | | |
| projaction-inf-def | axiom | | |
| projaction-base | axiom | | |
| projaction-rec-skipL | axiom | | |
| projaction-rec-addR | axiom | | |
| projaction-rec-addboth | axiom | | |
| projstate-base | axiom | | |
| projstate-rec-skipL | axiom | | |
| projstate-rec-addR | axiom | | |
| projstate-rec-addboth | axiom | | |