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