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: |
|---|
| restrict-intersect-empty-write-add | proved | all subs proved
| dom-ins,
restrict-intersect-empty,
|
| rem-write-cases | proved | all subs proved
| rem-write-other,
rem-write,
|
| Diff-mod | proved | all subs proved
| Diff-del-rw,
Diff-rec-rev,
Diff-rec,
|
| restrict-intersect-empty | proved | all subs proved
| Diff-ext,
Dom,
Diff-mems-get,
Diff-get,
|
| rem-write | proved | all subs proved
| Diff-mems-get,
Diff-get,
Diff-ext,
|
| rem-write-other | proved | all subs proved
| Diff-ext,
Diff-mems-get,
Diff-get,
|
| Diff-rec-rev | proved | all subs proved
| Diff-del-rw,
Diff-rec,
|
| restrict-at | proved | all subs proved
| Dom,
Diff-mems-get,
Diff-get,
restrict,
|
| dom-restrict | proved | all subs proved
| Dom,
dom-rem,
restrict,
|
| Diff-mems-get | proved | all subs proved
| Diff-ext,
|
| dom-rem | proved | all subs proved
| Diff-ext,
Dom,
|
| Diff-del-rw | proved | all subs proved
| Diff-get,
Diff-ext,
|
| restrict-in | proved | all subs proved
| Dom,
Diff-ext,
restrict,
|
| restrict-empty | proved | all subs proved
| Dom,
Diff-ext,
restrict,
|
| dom-emp | proved | all subs proved
| dom-isemp,
|
| diff-get-add | proved | all subs proved
| Diff-get,
Diff-rec,
|
| diff-add-notin | proved | all subs proved
| Diff-ext,
Diff-rec,
|
| Diff-Diff-com | proved | all subs proved
| Diff-get,
Diff-ext,
|
| Data-in-other | proved | all subs proved
| Data-in,
Data-notin-other,
|
| dom-ins | proved | all subs proved
| Dom,
|
| dom-isemp | proved | all subs proved
| Dom,
|
| Diff-ext | proved | all subs proved
| Diff-rec,
Diff-base,
|
| Diff-get | proved | all subs proved
| Diff-rec,
Diff-base,
|
| Data-notin-other | proved | all subs proved
| Data-in,
|
| oplus-shift-put-l | proved | all subs proved
| oplus-l-at-right,
oplus-l-at-left,
oplus-l-in,
|
| oplus-empty | proved | all subs proved
| oplus-l-at-left,
oplus-l-in,
|
| in-dom-inter | proved | all subs proved
| Dom,
|
| empty-oplus | proved | all subs proved
| oplus-l-at-right,
oplus-l-in,
|
| dom-union-l | proved | all subs proved
| oplus-l-in,
Dom,
|
| dom-del | proved | all subs proved
| Dom,
|
| dom-add-in | proved | all subs proved
| Dom,
|
| diff-add-rem | proved | all subs proved
| Diff-rec,
|
| In-data-in | proved | all subs proved
| Data-in,
|
| Diff-empty | proved | all subs proved
| Diff-rec,
Diff-base,
|
| Data-notin-other-3 | proved | all subs proved
| Data-in,
|
| Data-notin-other-2 | proved | all subs proved
| Data-in,
|
| Data-in-putsame | proved | all subs proved
| Data-in,
|
| Data-in-puteq | proved | all subs proved
| Data-in,
|
| Data-in-putdelput | proved | all subs proved
| Data-in,
|
| Data-in-putdel | proved | all subs proved
| Data-in,
|
| Data-in-delput-2 | proved | all subs proved
| Data-in,
|
| Data-in-delput | proved | all subs proved
| Data-in,
|
| Data-in-del | proved | all subs proved
| Data-in,
|
| oplus-l-at-left | axiom | | |
| oplus-l-at-right | axiom | | |
| oplus-l-in | axiom | | |
| restrict | axiom | | |
| Dom | axiom | | |
| Diff-base | axiom | | |
| Diff-rec | axiom | | |
| Data-in | axiom | | |