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: |
|---|
| reduce-unique | proved | all subs proved
| topred-def,
reduction-is-topred-in-ctxt,
|
| reduce-topreduce | proved | all subs proved
| reduction-is-topred-in-ctxt,
|
| no-ap-irred | proved | all subs proved
| reduce-no-ap,
irred-def,
|
| reduction-is-topred-in-ctxt | proved | all subs proved
| S-reduce,
K-reduce,
S-top-reduce,
topred-def,
K-top-reduce,
one-step-red-def,
S-does-not-top-reduce,
S-does-not-reduce,
K-does-not-top-reduce,
K-does-not-reduce,
|
| reduce-no-ap | proved | all subs proved
| S-does-not-reduce,
K-does-not-reduce,
|
| irred-no-step-01 | proved | all subs proved
| fun-reduces-imp-app-reduces,
irred-def,
|
| irred-no-step-02 | proved | all subs proved
| fun-value-and-arg-reduces-imp-app-reduces,
irred-def,
|
| fun-reduces-imp-app-reduces | proved | all subs proved
| one-step-red-def,
|
| fun-value-and-arg-reduces-imp-app-reduces | proved | all subs proved
| one-step-red-def,
|
| S-reduce | proved | all subs proved
| one-step-red-def,
|
| K-reduce | proved | all subs proved
| one-step-red-def,
|
| S-top-reduce | proved | all subs proved
| topred-def,
|
| K-top-reduce | proved | all subs proved
| topred-def,
|
| S-does-not-top-reduce | proved | all subs proved
| topred-def,
|
| S-does-not-reduce | proved | all subs proved
| one-step-red-def,
|
| K-does-not-top-reduce | proved | all subs proved
| topred-def,
|
| K-does-not-reduce | proved | all subs proved
| one-step-red-def,
|
| topred-unique | proved | all subs proved
| topred-def,
|
| reduction-is-reflexive | proved | all subs proved
| it-base,
reduce-def,
|
| it-rec-01 | proved | all subs proved
| it-rec,
|
| irred-top-01 | proved | all subs proved
| one-step-red-def,
irred-def,
topred-def,
|
| irred-top | proved | all subs proved
| one-step-red-def,
topred-def,
irred-def,
|
| irred-no-step | proved | all subs proved
| irred-def,
|
| reduce-def | axiom | | |
| it-base | axiom | | |
| it-rec | axiom | | |
| irred-def | axiom | | |
| topred-def | axiom | | |
| one-step-red-def | axiom | | |