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