[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 solitaire

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:
theoremprovedall subs proved theoremx, tolist-size, solix-to-solitaire,
theoremxprovedall subs proved ordered-precedes, orderedl-at, inv-base, orderedl-base, solixh-ordered, covers-ascsubseq, covers-empty, solixh-covers, theoremx-atmost-h, maxincseqno-def, theoremx-atleast, solix-def,
theoremx-atleastprovedall subs proved inv-last-nonempty, theoremx-atleast-ind, ascsubseq-base, inv-base, precedesex-base, solix-def, solix-inv, precedesex-solix,
precedesex-solixprovedall subs proved precedesex-base, inv-base, precedesex-solixh, solix-def,
solix-invprovedall subs proved inv-base, solixh-inv, solix-def,
solix-to-solitaireprovedall subs proved tolistl-base, inv-base, solixh-to-solitaireh, solix-def, solitaire-def,
solix-orderedprovedall subs proved inv-base, orderedl-base, solixh-ordered, solix-def,
theoremx-atmost-hprovedall subs proved coversi-append, ascsubseq-single, ascsubseq-nodups, covers-rem, ascsubseq-rem, precedes-ascsubseq-2, coversi-empty,
solixh-to-solitairehprovedall subs proved pushx-inv, pushx-cut-seq, pushix-to-push, solixh-rec, solitaireh-rec, solixh-base, solitaireh-base,
solixh-orderedprovedall subs proved pushx-ordered, pushx-inv-gen, solixh-rec, solixh-base,
solixh-invprovedall subs proved pushx-inv-gen, solixh-rec, solixh-base,
precedesex-solixhprovedall subs proved pushx-inv-gen, precedesex-pushix, solixh-rec, solixh-base,
solix-coversprovedall subs proved covers-def, solixh-covers, solix-def,
precedes-ascsubseq-2provedall subs proved precedes-ascsubseq-2-h,
ascsubseq-nodupsprovedall subs proved precedes-trans, ascsubseq-rest-notprec-first, ascsubseq-rec, ascsubseq-first-notin-rest,
theoremx-atleast-indprovedall subs proved ascsubseq-append, inv-butlast, precedesex-rev-rec1, allls-in, inv-single, ascsubseq-single, precedesex-rec0,
pushix-to-pushprovedall subs proved tolistl-cut-seq, tolist-cut-seq, allls-rec, tolist-rec, push-rec, pushx-rec, inv-rec, tolistl-rec, tolist-single, tolistl-single, pushx-base, push-base, tolistl-base,
pushx-invprovedall subs proved allls-incbound, inv-incbound, allls-rec, pushx-rec, inv-rec, allls-single, inv-single, pushx-base, inv-base,
solixh-coversprovedall subs proved pushx-covers, solixh-rec, solixh-base,
pushx-inv-genprovedall subs proved inv-incbound, allls-incbound, allls-rec, pushx-rec, inv-rec, allls-single, inv-single, pushx-base, inv-base,
ascsubseq-remprovedall subs proved precedes-def, ascsubseq-base, ascsubseq-single, ascsubseq-rec, ascsubseq-prepend,
precedesex-rev-rec1provedall subs proved precedesex-rec1, precedesex-prepend, precedesex-rec0, precedesex-2,
ascsubseq-appendprovedall subs proved ascsubseq-single, ascsubseq-rec, ascsubseq-2,
covers-ascsubseqprovedall subs proved ascsubseq-in-size, coversi-def, covers-def,
ordered-precedesprovedall subs proved precedes-def, ordered-precedes-h, precedes-notsame,
pushx-orderedprovedall subs proved ordered-rec2, allls-rec, pushx-rec, orderedl-rec, inv-rec, ordered-rec1, ordered-single, pushx-base, orderedl-base, inv-base,
pushx-coversprovedall subs proved covers-def, pushx-nonrec,
inv-incboundprovedall subs proved allls-incbound, inv-rec, inv-base,
tolistl-cut-seqprovedall subs proved tolist-cut-seq, inv-rec, tolistl-rec, tolistl-base,
precedesex-pushixprovedall subs proved precedes-def, precedesex-2, precedesex-rec1, precedesex-prepend, allls-rec, pushx-rec, inv-rec, precedesex-rec0, pushx-base, precedesex-base, inv-base,
precedes-ascsubseq-2-hprovedall subs proved precedes-trans, ascsubseq-rec,
ascsubseq-first-notin-restprovedall subs proved precedes-trans, precedes-irrefl, precedes-notsame, ascsubseq-rec, ascsubseq-single,
ascsubseq-rest-notprec-firstprovedall subs proved precedes-trans, precedes-irrefl, ascsubseq-rec, ascsubseq-single,
precedesex-appendprovedall subs proved precedes-append, precedesex-rec1, precedesex-rec0, inv-rec, precedesex-base, inv-base,
coversi-emptyprovedall subs proved coversi-def,
covers-remprovedall subs proved coversi-def,
coversi-appendprovedall subs proved coversi-def,
allls-inprovedall subs proved allls-rec,
inv-butlastprovedall subs proved inv-rec, inv-base,
inv-last-nonemptyprovedall subs proved inv-rec,
covers-emptyprovedall subs proved covers-def,
orderedl-atprovedall subs proved orderedl-base, orderedl-rec,
tolist-sizeprovedall subs proved tolistl-rec, tolistl-base,
pushx-cut-seqprovedall subs proved allls-rec, pushx-rec, inv-rec, pushx-base,
ordered-singleprovedall subs proved orderedl-base, orderedl-rec,
inv-singleprovedall subs proved inv-base, inv-rec,
allls-singleprovedall subs proved allls-base, allls-rec,
pushx-nonrecprovedall subs proved pushx-rec, pushx-base,
tolistl-singleprovedall subs proved tolistl-base, tolistl-rec,
tolist-singleprovedall subs proved tolist-base-02, tolist-rec,
tolist-cut-seqprovedall subs proved allls-rec, tolist-rec, tolist-base-02,
precedesex-prependprovedall subs proved precedesex-rec1, precedesex-base, precedesex-rec0,
precedesex-2provedall subs proved precedesex-rec0, precedesex-rec1,
precedes-appendprovedall subs proved precedes-def,
ordered-precedes-hprovedall subs proved ordered-rec2,
allls-incboundprovedall subs proved allls-rec, allls-base,
ascsubseq-in-sizeprovedall subs proved precedes-def, ascsubseq-rec, ascsubseq-single,
ascsubseq-prependprovedall subs proved ascsubseq-rec, ascsubseq-base, ascsubseq-single,
precedes-notsameprovedall subs proved precedes-def,
precedes-irreflprovedall subs proved precedes-def,
precedes-transprovedall subs proved precedes-def,
ascsubseq-2provedall subs proved precedes-def, ascsubseq-single, ascsubseq-rec,
ascsubseq-emptyprovedall subs proved ascsubseq-rec, ascsubseq-single, ascsubseq-base,
tolist-base-02axiom
maxincseqno-defaxiom
solitaireh-baseaxiom
solitaireh-recaxiom
solitaire-defaxiom
ordered-rec1axiom
tolistl-baseaxiom
push-baseaxiom
tolistl-recaxiom
push-recaxiom
tolist-recaxiom
solixh-baseaxiom
solixh-recaxiom
solix-defaxiom
pushx-baseaxiom
pushx-recaxiom
precedesex-baseaxiom
precedesex-rec1axiom
precedesex-rec0axiom
orderedl-recaxiom
orderedl-baseaxiom
ordered-rec2axiom
inv-baseaxiom
inv-recaxiom
covers-defaxiom
coversi-defaxiom
ascsubseq-baseaxiom
ascsubseq-recaxiom
ascsubseq-singleaxiom
precedes-defaxiom
allls-baseaxiom
allls-recaxiom