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: |
|---|
| trace-fininf-append | proved | all subs proved
| traceomega,
trace-append,
|
| move-cut | proved | all subs proved
| move-split,
|
| move-cut-2 | proved | all subs proved
| move-split,
|
| trace-finany-append | proved | all subs proved
| trace-append,
traceomega,
|
| move-split | proved | all subs proved
| move-empty,
finfrag-one,
fragstar,
finfrag-split,
move,
|
| trace-append | proved | all subs proved
| frag,
frag-split,
finexec,
fintrace,
exec,
trace,
|
| frag-from-fin | proved | all subs proved
| frag-from,
|
| inffrag-rec1 | proved | all subs proved
| inffrag-rec,
|
| move-trans | proved | all subs proved
| finfrag-split,
fragstar,
not-finfrag-empty,
move,
|
| inffrag-split | proved | all subs proved
| frag-split,
fragomega-def,
frag-from-inf,
frag-to-inf,
|
| emptymove-splitfirst | proved | all subs proved
| finfrag-rec,
finfrag-onlyone,
not-finfrag-empty,
move,
|
| moveone-splitstep | proved | all subs proved
| move-empty,
finfrag-rec,
not-finfrag-empty,
move,
|
| infappend-moves | proved | all subs proved
| infappend-moves-gen,
|
| inffrag-rec2 | proved | all subs proved
| inffrag-rec,
|
| fintrace | proved | all subs proved
| fragstar-def,
frag,
frag-split,
finexec,
exec,
trace,
tracestar-def,
|
| infappend-moves-gen | proved | all subs proved
| move,
frag-inf-al,
frag-finite-al,
fragstar,
frag,
exec,
trace,
not-finfrag-empty,
|
| finfrag-onlyone | proved | all subs proved
| fragstar,
finfrag-one,
not-finfrag-empty,
|
| finfrag-rec | proved | all subs proved
| not-finfrag-empty,
frag-onestate,
fragstar-def,
frag-rec,
|
| frag-to-inf | proved | all subs proved
| fragomega-def,
frag-to,
|
| frag-from-inf | proved | all subs proved
| frag-from-1,
|
| finfrag-split | proved | all subs proved
| fragstar-def,
frag-finite-sl,
frag-split,
|
| inffrag-rec | proved | all subs proved
| fraginf,
|
| frag-from | proved | all subs proved
| frag-from-1,
|
| frag-move | proved | all subs proved
| move,
not-finfrag-empty,
|
| frag-one | proved | all subs proved
| frag-onestate,
|
| not-frag-inf-fin | proved | all subs proved
| frag-finite-sl,
|
| preserve-INV-fin | proved | all subs proved
| not-finfrag-empty,
fragstar-def,
preserve-INV,
|
| frag-two | proved | all subs proved
| finfrag-two,
frag-finite-al,
|
| frag-to-fin | proved | all subs proved
| fragstar-def,
frag-to,
|
| move-one-ext | proved | all subs proved
| move-one,
|
| move-one | proved | all subs proved
| finfrag-two,
move,
|
| frag-to | proved | all subs proved
| fragstar,
frag,
|
| move-empty | proved | all subs proved
| finfrag-one,
move,
|
| frag-from-1 | proved | all subs proved
| frag,
frag-size,
|
| fraginf | proved | all subs proved
| frag,
fragomega-def,
frag-step-inf-inf,
|
| frag-finite-al | proved | all subs proved
| frag-inf-sl,
fragstar-def,
|
| frag-onestate | proved | all subs proved
| finfrag-one,
frag,
|
| frag-split | proved | all subs proved
| fragstar,
frag,
|
| frag-finite-sl | proved | all subs proved
| frag-inf-al,
fragstar-def,
|
| not-finfrag-empty | proved | all subs proved
| fragstar,
|
| fragfin-size-ls1 | proved | all subs proved
| fragstar,
|
| fragfin-size-le1 | proved | all subs proved
| fragfin-size-le,
|
| finfrag-one-action | proved | all subs proved
| fragstar,
|
| not-frag-fin-inf | proved | all subs proved
| frag-inf-sl,
|
| not-exec-empty | proved | all subs proved
| not-frag-empty,
exec,
|
| fragfin-size-notls | proved | all subs proved
| fragfin-size-le,
|
| exec-step-inf | proved | all subs proved
| frag-step-inf,
exec,
|
| exec-step-fin | proved | all subs proved
| frag-step-fin,
exec,
|
| frag-notsizeleq | proved | all subs proved
| fragstar,
|
| finfrag-rec-end | proved | all subs proved
| fragstar-def,
frag-rec-end,
|
| exec-step-fin-zero | proved | all subs proved
| frag-step-fin-zero,
exec,
|
| infappend-frags | proved | all subs proved
| frag,
not-frag-empty,
|
| frag-noactions | proved | all subs proved
| finfrag-one,
frag,
|
| fragstar-onestate | proved | all subs proved
| fragstar,
finfrag-one,
|
| exec-step-inf-zero | proved | all subs proved
| frag-step-inf-zero,
exec,
|
| frag-rec-end2 | proved | all subs proved
| frag-rec-end,
|
| inftrace | proved | all subs proved
| fragomega-def,
frag-inf-al,
exec,
trace,
traceomega,
infexec,
|
| exec-step | proved | all subs proved
| frag-step,
exec,
|
| exec-step-fin-2 | proved | all subs proved
| frag-step-fin-2,
exec,
|
| exec-step-zero | proved | all subs proved
| frag-step-zero,
exec,
|
| shortest-frag | proved | all subs proved
| not-frag-empty,
|
| frag-step-zero | proved | all subs proved
| frag,
|
| frag-step-fin-2 | proved | all subs proved
| frag,
|
| frag-step | proved | all subs proved
| frag,
|
| infexec | proved | all subs proved
| fragomega-def,
exec,
execomega,
|
| frag-step-inf-zero | proved | all subs proved
| frag,
|
| frag-step-inf-inf | proved | all subs proved
| frag,
|
| finfrag-two | proved | all subs proved
| frag,
|
| preserve-INV | proved | all subs proved
| frag,
|
| frag-rec | proved | all subs proved
| frag,
|
| frag-size | proved | all subs proved
| frag,
|
| frag-step-fin-zero | proved | all subs proved
| frag,
|
| frag-rec-end | proved | all subs proved
| frag,
|
| frag-step-fin | proved | all subs proved
| frag,
|
| frag-step-inf | proved | all subs proved
| frag,
|
| finexec | proved | all subs proved
| fragstar-def,
exec,
execstar,
|
| not-frag-empty | proved | all subs proved
| frag,
|
| frag-inf-sl | proved | all subs proved
| frag,
fragomega-def,
|
| fragfin-size-le | proved | all subs proved
| frag,
|
| finfrag-one | proved | all subs proved
| frag,
|
| frag-inf-al | proved | all subs proved
| frag,
fragomega-def,
|
| fragstar | proved | all subs proved
| frag,
fragstar-def,
|
| frag-size-2 | proved | all subs proved
| frag,
|
| fragfin-size-notls-02 | proved | all subs proved
| frag,
|
| fragfin-size-02 | proved | all subs proved
| frag,
|
| fragfin-size | proved | all subs proved
| frag,
|
| fragfin-size-ls-02 | proved | all subs proved
| frag,
|
| frag-trans | proved | all subs proved
| frag,
|
| exec-fin2 | proved | all subs proved
| frag,
exec,
|
| fragfin-size-ls | proved | all subs proved
| frag,
|
| exec-fin1 | proved | all subs proved
| frag,
exec,
|
| allfragto-frag | proved | all subs proved
| frag,
|
| execstar | axiom | | |
| execomega | axiom | | |
| tracestar-def | axiom | | |
| trace | axiom | | |
| exec | axiom | | |
| move | axiom | | |
| traceomega | axiom | | |
| fragstar-def | axiom | | |
| fragomega-def | axiom | | |
| frag | axiom | | |