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: |
|---|
| n2s-length-10 | proved | all subs proved
| n2s-length-09,
n2s-length-01,
n2s-length,
n2s-rec,
|
| n2s-length-09 | proved | all subs proved
| n2s-length-08,
n2s-length-01,
n2s-length,
n2s-rec,
|
| n2s-length-08 | proved | all subs proved
| n2s-length-07,
n2s-length-01,
n2s-length,
n2s-rec,
|
| n2s-length-07 | proved | all subs proved
| n2s-length-06,
n2s-length-01,
n2s-length,
n2s-rec,
|
| n2s-length-06 | proved | all subs proved
| n2s-length-05,
n2s-length-01,
n2s-length,
n2s-rec,
|
| n2s-length-05 | proved | all subs proved
| n2s-length-04,
n2s-length-01,
n2s-length,
n2s-rec,
|
| n2s-length-04 | proved | all subs proved
| n2s-length-03,
n2s-length-01,
n2s-length,
n2s-rec,
|
| n2s-length-03 | proved | all subs proved
| n2s-length-02,
n2s-length-01,
n2s-length,
n2s-rec,
|
| n2s-length-02 | proved | all subs proved
| n2s-length,
n2s-length-01,
n2s-rec,
|
| test-02 | proved | all subs proved
| charn5,
charn4,
charn3,
charn2,
charn1,
s2n-num,
|
| s2n-rec-last | proved | all subs proved
| s2n-app,
|
| n2s-zero | proved | all subs proved
| n2s-empty,
n2s-length-01,
n2s-char,
n2s-rec,
char0,
|
| n2s-s2n-identity | proved | all subs proved
| s2n-char,
n2s-length-01,
n2s-empty,
s2n-app,
n2s-rec,
n2s-char,
|
| inject-n2s | proved | all subs proved
| n2s-empty,
n2s-length-01,
n2s-rec,
n2s-char,
|
| s2n-num | proved | all subs proved
| s2n-rec-01,
|
| charn1 | proved | all subs proved
| s2n-char-01,
|
| charn2 | proved | all subs proved
| s2n-char-01,
|
| charn3 | proved | all subs proved
| s2n-char-01,
|
| charn4 | proved | all subs proved
| s2n-char-01,
|
| charn5 | proved | all subs proved
| s2n-char-01,
|
| s2n-app | proved | all subs proved
| s2n-rec-01,
|
| n2s-length-01 | proved | all subs proved
| n2s-length,
|
| test-01 | proved | all subs proved
| char5,
char4,
char3,
char2,
char1,
n2s-rec,
|
| charn9 | proved | all subs proved
| s2n-char-01,
|
| charn8 | proved | all subs proved
| s2n-char-01,
|
| charn7 | proved | all subs proved
| s2n-char-01,
|
| charn6 | proved | all subs proved
| s2n-char-01,
|
| charn0 | proved | all subs proved
| s2n-char-01,
|
| char1 | proved | all subs proved
| n2s-char,
|
| char2 | proved | all subs proved
| n2s-char,
|
| char3 | proved | all subs proved
| n2s-char,
|
| char4 | proved | all subs proved
| n2s-char,
|
| char5 | proved | all subs proved
| n2s-char,
|
| s2n-rec-01 | proved | all subs proved
| s2n-rec,
|
| char0 | proved | all subs proved
| n2s-char,
|
| n2s-length | proved | all subs proved
| n2s-char,
|
| n2s-empty | proved | all subs proved
| n2s-rec,
n2s-char,
|
| s2n-char-01 | proved | all subs proved
| s2n-char,
|
| n2s-chars | proved | all subs proved
| n2s-char,
n2s-rec,
|
| char9 | proved | all subs proved
| n2s-char,
|
| char8 | proved | all subs proved
| n2s-char,
|
| char7 | proved | all subs proved
| n2s-char,
|
| char6 | proved | all subs proved
| n2s-char,
|
| s2n-rec | axiom | | |
| s2n-char | axiom | | |
| n2s-rec | axiom | | |
| n2s-char | axiom | | |