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