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: |
|---|
| mu-subset-nu | proved | all subs proved
| fixpoint-nu,
least-fixpoint,
|
| fixpoint-nu | proved | all subs proved
| compl-def,
compl-monotone,
fixpoint,
greatest-prefixpoint-def,
|
| fixpoint | proved | all subs proved
| prefixpoint-rev,
prefixpoint,
eq-bothsubset,
|
| prefixpoint-rev | proved | all subs proved
| monotone-def,
prefixpoint-aux,
prefixpoint,
|
| least-fixpoint | proved | all subs proved
| subset-refl,
least-prefixpoint-def,
subseteq-def,
|
| prefixpoint | proved | all subs proved
| subset-trans,
monotone-def,
prefixpoint-aux,
prefixpoint-aux2,
|
| prefixpoint-aux-nu | proved | all subs proved
| union-def,
subseteq-def,
nu-is-UN,
|
| nu-is-UN | proved | all subs proved
| compl-def,
subseteq-def,
least-prefixpoint-def,
union-def,
greatest-prefixpoint-def,
|
| prefixpoint-aux2 | proved | all subs proved
| least-prefixpoint-def,
subseteq-def,
|
| prefixpoint-aux | proved | all subs proved
| least-prefixpoint-def,
subseteq-def,
|
| subset-trans | proved | all subs proved
| subseteq-def,
|
| subset-refl | proved | all subs proved
| subseteq-def,
|
| compl-monotone | proved | all subs proved
| compl-def,
subseteq-def,
monotone-def,
|
| eq-bothsubset | proved | all subs proved
| subseteq-def,
|
| mu-is-IS | proved | all subs proved
| least-prefixpoint-def,
intersection-def,
|
| compl-inverse | proved | all subs proved
| compl-def,
|
| union-def | axiom | | |
| intersection-def | axiom | | |
| least-prefixpoint-def | axiom | | |
| greatest-prefixpoint-def | axiom | | |
| monotone-def | axiom | | |
| subseteq-def | axiom | | |
| compl-def | axiom | | |