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: |
|---|
| injectivity | proved | all subs proved
| sel-snd,
sel-fst,
|
| exencode | proved | all subs proved
| dec-int-01,
dec-nat-01,
encode-pair,
dec-snd,
dec-fst,
|
| enc-invert | proved | all subs proved
| dec-int-01,
dec-nat-01,
encode-pair,
dec-snd,
dec-fst,
|
| sel-fst | proved | all subs proved
| dec-int,
dec-nat,
dec-fst,
encode-pair,
|
| sel-snd | proved | all subs proved
| dec-int,
dec-nat,
dec-snd,
encode-pair,
|
| dec-int-01 | proved | all subs proved
| enc-zero-02,
enc-nat-neg,
enc-nat-pos,
dec-nat-pos,
dec-nat-neg,
|
| injectivity-02 | proved | all subs proved
| dec-int,
|
| injectivity-01 | proved | all subs proved
| dec-nat,
|
| enc-zero | proved | all subs proved
| enc-zero-01,
enc-int-pos,
enc-zero-02,
encode-pair,
|
| dec-int | proved | all subs proved
| dec-int-neg,
dec-int-pos,
enc-int-pos,
enc-int-neg,
|
| dec-nat | proved | all subs proved
| dec-nat-neg,
dec-nat-pos,
enc-nat-pos,
enc-nat-neg,
|
| enc-zero-01 | proved | all subs proved
| enc-int-neg,
enc-int-pos,
|
| dec-nat-01 | proved | all subs proved
| enc-int-neg,
enc-int-pos,
dec-int-pos,
dec-int-neg,
|
| enc-zero-02 | proved | all subs proved
| enc-nat-pos,
enc-nat-neg,
|
| dec-fst | axiom | | |
| dec-snd | axiom | | |
| encode-pair | axiom | | |
| dec-nat-neg | axiom | | |
| dec-nat-pos | axiom | | |
| enc-nat-pos | axiom | | |
| enc-nat-neg | axiom | | |
| enc-int-neg | axiom | | |
| enc-int-pos | axiom | | |
| dec-int-pos | axiom | | |
| dec-int-neg | axiom | | |