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: |
|---|
| valid-peb-sqns-nonempty0 | proved | all subs proved
| valid-peb-sqns-nonempty,
valid-sqns,
|
| valid-peb-sqns-nonempty | proved | all subs proved
| valid-sqns-extract-sqn,
valid-sqns,
|
| valid-sqns-write | proved | all subs proved
| valid-sqns-write-h,
valid-sqns,
|
| valid-sqns-extract2-sqn | proved | all subs proved
| valid-sqns-extract2-sqn-h,
valid-sqns,
|
| valid-sqns-write-h | proved | all subs proved
| valid-peb-in-sqnums-h,
valid-sqns-rec,
valid-sqns-base,
|
| valid-sqns-extract2-sqn-h | proved | all subs proved
| valid-sqns-extract-sqn-h,
valid-sqns-rec,
|
| valid-sqns-extract-sqn | proved | all subs proved
| valid-sqns-extract-sqn-h,
valid-sqns,
|
| valid-sqns-subseteq | proved | all subs proved
| valid-sqns-subseteq-h,
valid-sqns,
|
| valid-sqns-subarray | proved | all subs proved
| valid-sqns-subarray-h,
valid-sqns,
|
| valid-sqns-nonempty-extract-max | proved | all subs proved
| valid-sqns-nonempty-extract-max-h,
valid-sqns,
|
| valid-peb-in-sqnums | proved | all subs proved
| valid-peb-in-sqnums-h,
valid-sqns,
|
| valid-sqns-subseteq-h | proved | all subs proved
| valid-sqns-rec,
valid-sqns-base,
|
| valid-sqns-subarray-h | proved | all subs proved
| valid-sqns-rec,
valid-sqns-base,
|
| valid-sqns-nonempty-extract-max-h | proved | all subs proved
| valid-sqns-rec,
valid-sqns-base,
|
| valid-sqns-extract-sqn-h | proved | all subs proved
| valid-sqns-rec,
|
| valid-peb-in-sqnums-h | proved | all subs proved
| valid-sqns-rec,
|
| valid-sqns-array-0 | proved | all subs proved
| valid-sqns-base,
valid-sqns,
|
| valid-sqns-base | axiom | | |
| valid-sqns-rec | axiom | | |
| valid-sqns | axiom | | |