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: |
|---|
| fst-nle | proved | all subs proved
| fst-zero,
fst-ls,
|
| fst-ls | proved | all subs proved
| fst-one,
fst-zero,
fst-ls-01,
|
| fst-ls-01 | proved | all subs proved
| max-snd-nle,
max-snd-le,
dec-fst,
fst-one,
|
| max-snd-le | proved | all subs proved
| max-snd-nls,
|
| snd-nle | proved | all subs proved
| snd-eq,
snd-le,
snd-zero,
|
| exencode | proved | all subs proved
| enc-invert,
|
| snd-le | proved | all subs proved
| max-nls,
dec-snd,
|
| snd-eq | proved | all subs proved
| max-zero,
max-nls,
dec-snd,
snd-zero,
|
| max-snd-nls | proved | all subs proved
| max-size,
max-nls,
dec-snd,
|
| max-snd-nle | proved | all subs proved
| max-two,
max-zero,
max-zero-01,
max-size-01,
max-nls,
dec-snd,
|
| enc-invert | proved | all subs proved
| max-size,
max-size-01,
max-nls,
encode-def,
dec-snd,
dec-fst,
|
| snd-ls | proved | all subs proved
| max-zero,
max-nls,
dec-snd,
snd-zero,
|
| fst-zero | proved | all subs proved
| snd-zero,
max-zero-02,
dec-fst,
|
| fst-one | proved | all subs proved
| snd-one,
max-one,
dec-fst,
|
| max-nls | proved | all subs proved
| max-size,
|
| max-size-01 | proved | all subs proved
| max-size,
|
| snd-zero | proved | all subs proved
| max-zero-02,
dec-snd,
|
| snd-one | proved | all subs proved
| max-one,
dec-snd,
|
| max-size | proved | all subs proved
| max-rev-01,
|
| snd-def | proved | all subs proved
| max-square,
encode-def,
dec-snd,
|
| max-le | proved | all subs proved
| max-zero,
max-rev-01,
|
| fst-def | proved | all subs proved
| dec-snd,
max-square,
encode-def,
dec-fst,
|
| max-two | proved | all subs proved
| max-zero-01,
|
| max-rev-01 | proved | all subs proved
| max-rev,
maxi-start,
|
| max-zero-02 | proved | all subs proved
| max-zero,
|
| max-one | proved | all subs proved
| max-zero-01,
|
| max-square | proved | all subs proved
| max-def-01,
|
| max-def-01 | proved | all subs proved
| max-def,
maxi-start,
|
| max-rev | proved | all subs proved
| max-def,
maxi-rec,
|
| max-zero-01 | proved | all subs proved
| max-bigger,
maxi-found,
maxi-rec,
maxi-start,
|
| max-zero | proved | all subs proved
| max-bigger,
maxi-rec,
maxi-found,
maxi-start,
|
| max-bigger | proved | all subs proved
| maxi-found,
maxi-rec,
|
| max-def | proved | all subs proved
| maxi-found,
maxi-rec,
|
| injectivity | proved | all subs proved
| encode-def,
|
| encode-zero-01 | proved | all subs proved
| encode-def,
|
| encode-zero | proved | all subs proved
| encode-def,
|
| maxi-start | axiom | | |
| maxi-rec | axiom | | |
| maxi-found | axiom | | |
| dec-fst | axiom | | |
| dec-snd | axiom | | |
| encode-def | axiom | | |