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: |
|---|
| succlessleninv-invsize | proved | all subs proved
| leninv-invlast-inv,
leninv-is-len-inv,
stutf-invmonls,
monls-ls,
leninv-inf-strong,
|
| leninv-invlast-inv-2 | proved | all subs proved
| leninv-invlast-inv,
|
| stutf-invmonls | proved | all subs proved
| inv-ls-notleq,
leninv-is-len-inv,
monls-def,
|
| leninv-invlast-inv | proved | all subs proved
| inv-inverts-last,
leninv-succ,
|
| lsleninv-3 | proved | all subs proved
| lsleninv-2,
|
| inv-get-inverse-succ-inf | proved | all subs proved
| inv-get-inverse-succ,
|
| inv-ls-notleq | proved | all subs proved
| inv-ls-succ,
|
| inv-inverts-last | proved | all subs proved
| leninv-invlast,
leninv-zero,
maxinf-fin,
maxinf-inf,
inv-def,
|
| inv-get-inverse-succ | proved | all subs proved
| stutf-nonempty,
leninv-succ,
stutf-def,
maxinf-fin,
stutf-alltaken,
stutf-zero,
stutf-monle,
monle-leq,
maxinf-inf,
leninv-inf,
leninv-inf-strong,
inv-def,
|
| lsleninv-2 | proved | all subs proved
| lsleninv-1,
|
| leninv-invlast-2 | proved | all subs proved
| leninv-invlast,
|
| not-ls-leninv | proved | all subs proved
| leq-leninv,
|
| inv-get-lslen | proved | all subs proved
| maxinf-fin,
stutf-alltaken,
maxinf-inf,
stutf-nonempty,
leninv-succ,
leninv-inf-strong,
inv-def,
|
| inv-get-inverse-between | proved | all subs proved
| stutf-nonempty,
stutf-def,
leninv-succ,
stutf-alltaken,
stutf-zero,
maxinf-fin,
stutf-monle,
monle-leq,
maxinf-inf,
leninv-inf,
leninv-inf-strong,
inv-def,
|
| inv-inverts | proved | all subs proved
| maxinf-fin,
maxinf-inf,
stutf-nonempty,
stutf-monle,
monle-leq,
leninv-succ,
leninv-zero,
leninv-inf-strong,
inv-def,
|
| lsleninv-1 | proved | all subs proved
| stutf-nonempty,
stutf-monle,
monle-leq,
stutf-alltaken,
leninv-succ,
leninv-zero,
|
| inv-ls-succ | proved | all subs proved
| stutf-nonempty,
maxinf-fin,
leninv-def,
stutf-alltaken,
stutf-zero,
stutf-monle,
monle-leq,
leninv-inf,
maxinf-inf,
inv-def,
|
| leq-leninv | proved | all subs proved
| stutf-nonempty,
stutf-monle,
monle-leq,
leninv-succ,
leninv-zero,
leninv-less,
|
| leninv-invlast | proved | all subs proved
| leninv-succ,
|
| leninv-inf-strong | proved | all subs proved
| stutf-zero,
leninv-inf,
|
| less-leninv | proved | all subs proved
| stutf-monle,
monle-leq,
leninv-succ,
leninv-zero,
|
| inv-get-inverse-last | proved | all subs proved
| stutf-monle,
monle-leq,
maxinf-fin,
stutf-nonempty,
stutf-maxinf-is-fin,
leninv-succ,
inv-def,
|
| eq-leninv | proved | all subs proved
| stutf-alltakenmax,
stutf-nonempty,
leninv-succ,
stutf-monle,
monle-leq,
leninv-zero,
|
| inv-get-inverse | proved | all subs proved
| stutf-nonempty,
leninv-succ,
maxinf-fin,
stutf-alltaken,
stutf-zero,
stutf-monle,
monle-leq,
maxinf-inf,
leninv-inf,
inv-def,
|
| inv-inverts-leq | proved | all subs proved
| stutf-nonempty,
maxinf-fin,
leninv-succ,
stutf-monle,
monle-leq,
leninv-inf,
maxinf-inf,
maxinf-def,
inv-def,
|
| stutf-alltakenmax | proved | all subs proved
| stutf-nonempty,
stutf-def,
stutf-zero,
|
| stutf-maxinf-is-fin | proved | all subs proved
| stutf-monle,
monle-leq,
stutf-alltaken,
maxinf-inf,
|
| leninv-inf | proved | all subs proved
| stutf-nonempty,
stutf-alltaken,
stutf-zero,
stutf-monle,
monle-leq,
maxinf-inf,
leninv-def,
|
| leninv-zero | proved | all subs proved
| stutf-nonempty,
stutf-zero,
maxinf-fin,
leninv-def,
|
| leninv-succ | proved | all subs proved
| stutf-nonempty,
stutf-def,
stutf-alltaken,
stutf-monle,
monle-leq,
maxinf-fin,
leninv-def,
|
| mininv-inverts-weak2 | proved | all subs proved
| mininv-inverts-weak,
|
| mininv-inverts-inner | proved | all subs proved
| mininv-inverts-weak,
monls-ls,
min-empty,
min-def,
|
| mininv-inverts-weak | proved | all subs proved
| min-empty,
min-def,
|
| stutf-nonempty | proved | all subs proved
| not-stutf-empty,
|
| stutf-alltaken | proved | all subs proved
| stutf-def,
stutf-zero,
|
| rem-preserves-monls | proved | all subs proved
| monls-to,
monls-mon-implies-monls,
monls-ls,
monls-def,
monls-append1,
|
| mininv-inverts | proved | all subs proved
| min-empty,
min-def,
|
| monls-exists-maxleq | proved | all subs proved
| monls-exists-maxls,
monls-ls,
|
| mon-eq | proved | all subs proved
| monls-ls,
|
| monlsinf-notsmall | proved | all subs proved
| monls-notsmall,
|
| mininv-inverts-inner-succ | proved | all subs proved
| monls-ls,
min-empty,
min-def,
|
| stutf-notbig | proved | all subs proved
| stutf-def,
stutf-zero,
|
| min-stutters | proved | all subs proved
| monls-ls,
min-def,
|
| mininv-stays-if-not-taken | proved | all subs proved
| min-empty,
min-def,
|
| monls-notsmall | proved | all subs proved
| monls-def,
|
| not-stutf-empty | proved | all subs proved
| stutf-def,
|
| min-empty | proved | all subs proved
| monls-def,
min-def,
|
| monls-append1 | proved | all subs proved
| monls-def,
|
| monls-mon-implies-monls | proved | all subs proved
| monls-def,
|
| monls-to | proved | all subs proved
| monls-def,
|
| maxinf-fin | proved | all subs proved
| maxinf-def,
|
| stutf-zero | proved | all subs proved
| stutf-def,
|
| monls-ls | proved | all subs proved
| monls-def,
|
| leninv-is-len-inv | proved | all subs proved
| inv-def,
|
| maxinf-inf | proved | all subs proved
| maxinf-def,
|
| monle-leq | proved | all subs proved
| monle-def,
|
| stutf-monle | proved | all subs proved
| stutf-def,
monle-def,
|
| monls-append2 | proved | all subs proved
| monls-def,
|
| monls-from | proved | all subs proved
| monls-def,
|
| stutf-slowincrease | proved | all subs proved
| stutf-def,
|
| min-skolemf | proved | all subs proved
| monls-def,
|
| min-zero | proved | all subs proved
| min-def,
|
| leninv-less | proved | all subs proved
| |
| monle-def | axiom | | |
| maxinf-def | axiom | | |
| monls-exists-maxls | proved | all subs proved
| |
| stutf-def | axiom | | |
| min-def | axiom | | |
| inv-def | axiom | | |
| leninv-def | axiom | | |
| monls-def | axiom | | |