[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification oset

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:
bmin-two-06provedall subs proved bmin-two-07, min-inn,
min-unionprovedall subs proved min-rec, min-inn, max-in, Min-in, Max-in,
min-recprovedall subs proved min-inn, max-in, Min-in, Max-in, min-ins-03, min-one, min-ins-04,
bmin-two-07provedall subs proved bmin-two-01, bmin-two-02, size-two,
bmin-twoprovedall subs proved bmin-two-01, min-one, bmin-two-02, size-two,
bmin-two-08provedall subs proved min-two, bmin-two-01, min-two-01, min-one, bmin-two-02, size-two,
bmin-two-05provedall subs proved bmin-two-01, min-two, min-one, bmin-two-02, min-two-01, size-two,
bmin-two-04provedall subs proved bmin-two-01, min-two, min-one, bmin-two-02, min-two-01, size-two,
bmin-sub-01provedall subs proved bmin-two-01, min-one, bmin-two-02, Max-max, Min-min, Min-in, Max-in, size-two, min-sub, min-subset,
bmin-sub-02provedall subs proved bmin-two-01, min-two, min-one, bmin-two-02, min-two-01, size-two, Max-max, Min-min, Min-in, Max-in,
min-ins-04provedall subs proved min-insert, minmax-04, Max-max, Min-min, Min-in, Max-in,
min-ins-03provedall subs proved min-insert, min-ins-01, minmax-04, Max-max, Min-min, Min-in, Max-in,
bmin-two-02provedall subs proved bmin-two-01,
minmax-01provedall subs proved Max-max, Min-min, min-one-01, Min-in, Max-in, Butmin,
minmaxprovedall subs proved Max-max, Min-min, min-one-01, Min-in, Max-in, Butmax, Butmin,
bmin-two-03provedall subs proved min-two, bmin-two-01,
max-insprovedall subs proved max-ifins,
bmin-minprovedall subs proved min-delmin-01, Max-max, Min-min, Min-in, Max-in, Butmin,
bmin-del-04provedall subs proved minmax-04, bmin-del-03, Max-max, Min-min, Min-in, Max-in, Butmin,
bmin-one-03provedall subs proved min-one-01, Butmin, minmax-04, Max-max, Min-min, Min-in, Max-in,
bmin-blsprovedall subs proved min-one-01, min-delmin, Max-max, Min-min, Min-in, Max-in, Butmin,
bmax-one-01provedall subs proved max-one-01, Butmax, minmax-04, Max-max, Min-min, Min-in, Max-in,
max-ins-01provedall subs proved max-ifins,
butmin-insprovedall subs proved min-insert, min-ins-01, minmax-04, Max-max, Min-min, Min-in, Max-in, Butmin,
butmin-ins-01provedall subs proved min-insert, Butmin, minmax-04, Max-max, Min-min, Min-in, Max-in,
min-two-02provedall subs proved min-two, max-one, max-ifins, min-two-01, minmax-04, Max-max, Min-min, Min-in, Max-in,
max-one-01provedall subs proved max-one,
min-delminprovedall subs proved min-subset, min-less, Max-max, Min-min, Min-in, Max-in,
bmin-del-03provedall subs proved bmin-del-02, min-del, minmax-04, Max-max, Min-min, Min-in, Max-in, Butmin,
min-delmin-01provedall subs proved min-subset, Max-max, Min-min, Min-in, Max-in,
max-ifinsprovedall subs proved max-gr, max-q, Max-max, Min-min, Min-in, Max-in, max-one,
min-two-01provedall subs proved min-two,
min-one-01provedall subs proved min-one,
bmin-two-01provedall subs proved min-two, bmin-del-05,
min-insertprovedall subs proved min-inn, minmax-04, Max-max, Min-min, Min-in, Max-in,
bmin-in-04provedall subs proved min-subset, Max-max, Min-min, Min-in, Max-in, Butmin,
bm-shiftprovedall subs proved bmin-del-02, min-del, minmax-02, max-del-01, bmax-def, Max-max, Min-min, Min-in, Max-in, Butmax, Butmin,
bmin-intemptyprovedall subs proved Max-max, Min-min, minmax-04, Min-in, Max-in, min-less, Butmin,
min-del-01provedall subs proved min-del,
bmin-bneqprovedall subs proved min-one, max-one, Max-max, Min-min, Min-in, Max-in, Butmin,
bmin-oneprovedall subs proved min-one, bmin-del-05, Max-max, Min-min, Min-in, Max-in,
bmin-one-01provedall subs proved min-one, max-one, Max-max, Min-min, Min-in, Max-in, Butmin,
ls-rmprovedall subs proved max-in, Max-max, Min-min, minmax-04, Min-in, Max-in, Greater,
bmax-shiftprovedall subs proved max-del-01, minmax-04, Max-max, Min-min, Min-in, Max-in, Butmax,
bmin-inprovedall subs proved min-inn, Min-min, Max-max, ins-inbutmins,
bmin-sub-05provedall subs proved min-less, Max-max, Min-min, minmax-04, Min-in, Max-in, Butmin,
bmax-maxprovedall subs proved Max-max, Min-min, Min-in, Max-in, max-del, Butmax,
bmax-oneprovedall subs proved max-one, Butmax, Max-max, Min-min, Min-in, Max-in,
bmax-minprovedall subs proved minmax-02, min-del, minmax-04, Max-max, Min-min, Min-in, Max-in, Butmax,
is-minprovedall subs proved min-less, minmax-04, Max-max, Min-min, Min-in, Max-in,
min-intemptyprovedall subs proved Max-max, Min-min, minmax-04, Min-in, Max-in,
bmin-binprovedall subs proved min-one, max-one, min-subset, Max-max, Min-min, Min-in, Max-in, Butmin,
min-sub-01provedall subs proved min-less, Max-in, Min-min, Max-max, minmax-04, Min-in,
ls-addprovedall subs proved max-in, Max-max, Min-min, minmax-04, Min-in, Max-in, Greater,
max-bminprovedall subs proved minmax-02, max-del-01, Max-max, Min-min, Min-in, Max-in, Butmin,
max-delprovedall subs proved max-subset-01, Max-max,
ins-inbutminsprovedall subs proved Min-min, Max-max, bmin-f, bmin-in-01,
max-oneprovedall subs proved max-q,
min-oneprovedall subs proved min-q,
min-ins-01provedall subs proved min-q, Max-max, Min-min, Min-in, Max-in,
minmax-04provedall subs proved max-gr, Min-in, Max-in,
min-twoprovedall subs proved min-q,
max-del-01provedall subs proved max-gr, max-q, Max-max, Min-min, Min-in, Max-in,
minmax-02provedall subs proved minmax-03, max-gr, Min-min, Max-max, Min-in, Max-in,
min-delprovedall subs proved min-q, Max-max, Min-min, Min-in, Max-in,
min-subsetprovedall subs proved min-sub,
min-ins-02provedall subs proved min-q, Max-max, Min-min, Min-in, Max-in,
min-ins-05provedall subs proved min-inn,
bmin-nin-02provedall subs proved bmin-in-01,
bmin-fprovedall subs proved Butmin,
min-subprovedall subs proved Max-max, Min-min, Min-in, Max-in,
bmin-in-01provedall subs proved Butmin, Min-min, Max-max,
max-inprovedall subs proved Min-in, Max-in,
minmax-03provedall subs proved Max-max, Min-min, Min-in, Max-in,
min-innprovedall subs proved Min-in, Max-in,
max-subset-01provedall subs proved Max-max, Min-min, Min-in, Max-in,
min-lessprovedall subs proved Min-min, Max-max,
max-qprovedall subs proved Max-max, Min-min, Min-in, Max-in,
max-grprovedall subs proved Min-in, Max-in, Min-min, Max-max,
bmin-del-05provedall subs proved Butmin,
min-qprovedall subs proved Max-max, Min-min, Min-in, Max-in,
bmax-defprovedall subs proved Butmax,
bmin-del-02provedall subs proved Butmin,
bmin-in-03provedall subs proved Butmin,
min-lsprovedall subs proved Min-in, Max-in,
bmin-sizeprovedall subs proved Min-in, Max-in, Butmin,
butmin-inprovedall subs proved Butmin,
bmin-subprovedall subs proved Butmin,
bmin-del-01provedall subs proved Butmin,
bmin-one-02provedall subs proved Min-in, Max-in, Butmin, Min-min, Max-max,
ls-emptysetprovedall subs proved Greater,
maxunionprovedall subs proved Max-max, Min-min, Min-in, Max-in,
bmin-eq-01provedall subs proved Max-max, Min-min, Min-in, Max-in, Butmin,
bmin-nin-01provedall subs proved Butmin,
bmax-emptyprovedall subs proved Min-in, Max-in, Butmax,
bmin-sub-03provedall subs proved Butmin,
bmin-sub-04provedall subs proved Butmin,
bmax-in-01provedall subs proved Butmax,
bmax-in-02provedall subs proved Butmax,
bmax-inprovedall subs proved Butmax, Min-min, Max-max,
diff-minprovedall subs proved Min-in, Max-in, Min-min, Max-max,
min-incprovedall subs proved Min-in, Max-in,
bminminprovedall subs proved Min-in, Max-in, Butmin,
max-subsetprovedall subs proved Min-min, Max-max, Min-in, Max-in,
bmin-size-01provedall subs proved Min-in, Max-in, Butmin,
bmin-size-02provedall subs proved Min-in, Max-in, Butmin,
bmin-delprovedall subs proved Butmin,
bmin-eqprovedall subs proved Min-in, Max-in, Butmin,
bmin-ninprovedall subs proved Butmin,
Greateraxiom
size-twoprovedall subs proved
Butmaxaxiom
Max-inaxiom
Min-inaxiom
Max-maxaxiom
Min-minaxiom
Butminaxiom