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

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:
succ-inv2xprovedall subs proved inv-inv, succ-one, succ-zeros, succ-prefix, invert-one, inv-append, succ-exinv,
lastn-fill-sgnprovedall subs proved sgn-lastn-01, sgn-rec, sgn-base-03, fill-sgn-04, sgn-base-01, sgn-rec-01, sgn-append-05, sgn-append-04, sgn-append-01, fill-length, fillsgn-longer, fill-sgn, fill-lastn, fill-sgn-01,
succ-exinvprovedall subs proved succ-one, succ-zeros, succ-prefix, inv-one-01, inv-append,
fill-sgnprovedall subs proved sgn-mklist, sgn-ex, sgn-first-01, fillsgn-empty, sgn-empty, sgn-empty-01, sgn-length-01, fill-fill,
fill-sgn-04provedall subs proved fill-sgn-02,
succ-length-01provedall subs proved inv-len, succ-ones, succ-len,
succ-lengthprovedall subs proved inv-len, inv-in-01, inv-inv, succ-ones, succ-len,
succ-fillprovedall subs proved succ-len, fillsgn-fill, fillsgn-longer, succ-zero-01,
sgn-negintprovedall subs proved sgn-base-01, succ-zero-02, succ-prefix, invert-one, invert-zero,
sgn-lastnprovedall subs proved sgn-last-same, sgn-last-04,
fill-sgn-03provedall subs proved fill-sgn-01, fillsgn-empty, sgn-empty, sgn-nls, fill-rec, sgn-empty-01, fill-empty,
bitsinvert-sizeprovedall subs proved sgn-rec, inv-first-01, inv-len, sgn-base-03, inv-in, inv-empty, sgn-rec-01, sgn-one, invert-base, inv-one, inv-append,
succ-lenprovedall subs proved inv-len, succ-one, succ-zeros-01, succ-prefix,
succ-zerosprovedall subs proved inv-inv, inv-in-01, succ-zeros-01,
succ-zero-02provedall subs proved inv-in-01, inv-inv, succ-zeros-01, succ-zero-01,
sgn-last-sameprovedall subs proved sgn-empty-01, sgn-append-01, sgn-zero, sgn-true,
fill-sgn-02provedall subs proved sgn-first, sgn-length-02, sgn-notsame-01, sgn-not-empty-01, fill-rec, fillsgn-longer, sgn-base-03, sgn-rec-01, fill-one, sgn-one,
sgn-nlsprovedall subs proved sgn-length, sgn-empty-01,
fill-sgn-01provedall subs proved sgn-in, sgn-base, sgn-append, sgn-first, sgn-length, sgn-not-empty-01, fill-fill, fillsgn-fill, fillsgn-empty, sgn-empty,
sgn-length-01provedall subs proved sgn-length,
inv-first-01provedall subs proved invert-one, inv-intro, inv-in-02, inv-inv, invert-zero,
succ-mklist-01provedall subs proved inv-mklist, succ-ones,
succ-mklistprovedall subs proved inv-mklist, succ-one, succ-zero-01, succ-zeros-01,
succ-first-01provedall subs proved inv-in-02, succ-one, succ-one-01, inv-in-01, inv-in, inv-empty, succ-empty-01, succ-zeros-01, succ-first,
succ-exprovedall subs proved succ-one, succ-zeros-01, succ-prefix, succ-ones,
sgn-length-03provedall subs proved sgn-length,
sgn-last-bothprovedall subs proved sgn-append-01,
sgn-first-04provedall subs proved sgn-first-02, sgn-in-01,
sgn-append-06provedall subs proved sgn-last-04, sgn-zeros, sgn-append-01,
inv-firstprovedall subs proved invert-zero, inv-intro, inv-in-01, inv-inv, invert-one,
succ-onesprovedall subs proved succ-rec-01, inv-last, invert-base, succ-empty,
succ-zeros-01provedall subs proved succ-rec-01, inv-last, invert-base,
sgn-first-02provedall subs proved sgn-first, sgn-in-02,
sgn-last-04provedall subs proved sgn-in-02, sgn-rec, sgn-base-04, sgn-base-03, sgn-rec-01, sgn-empty, sgn-one,
sgn-append-01provedall subs proved sgn-rec, sgn-zero, sgn-true, sgn-base-01, sgn-base-02, sgn-one, sgn-rec-01, sgn-empty,
inv-in-02provedall subs proved inv-in,
inv-in-01provedall subs proved inv-in,
inv-introprovedall subs proved inv-inv,
sgn-notsame-01provedall subs proved sgn-in-01, sgn-base-01, sgn-base-02, sgn-one, sgn-rec-01, sgn-in-02, sgn-empty,
sgn-lengthprovedall subs proved sgn-base-01, sgn-base-02, sgn-not-empty, sgn-one, sgn-rec-01, sgn-not-empty-01, sgn-empty,
sgn-mklistprovedall subs proved sgn-first, sgn-not-empty-01, sgn-rec-01, sgn-sgn,
succ-succprovedall subs proved succ-rec, inv-inv, inv-false, inv-append, inv-last, succ-zero, inv-one-01, succ-one, invert-base,
succ-falsein-01provedall subs proved inv-empty, succ-falsein,
sgn-one-01provedall subs proved sgn-zero, sgn-base-01, sgn-base-02, sgn-base-04, sgn-empty, sgn-rec-01, sgn-one, sgn-true,
sgn-notsameprovedall subs proved sgn-base-01, sgn-base-02, sgn-in-01, sgn-one, sgn-rec-01, sgn-in-02, sgn-empty,
sgn-first-03provedall subs proved sgn-first, sgn-in-02,
inv-true-01provedall subs proved inv-empty, inv-one, inv-append, invert-base, inv-false,
inv-fillprovedall subs proved inv-len, fillsgn-fill, inv-one, inv-mklist, inv-append, fill-fill, fillsgn-longer,
inv-false-01provedall subs proved inv-empty, inv-append, invert-base, inv-one,
inv-lastprovedall subs proved inv-one, inv-append,
sgn-in-02provedall subs proved sgn-in-01,
sgn-trueprovedall subs proved sgn-mklist-03,
sgn-append-04provedall subs proved sgn-append-03,
sgn-append-05provedall subs proved sgn-append-03,
sgn-lastn-01provedall subs proved sgn-length-02, sgn-base-03, sgn-one, sgn-rec-01,
inv-invprovedall subs proved inv-one, inv-append, invert-base,
sgn-not-empty-01provedall subs proved sgn-not-empty, sgn-base-01, sgn-base-02, sgn-one, sgn-rec-01,
sgn-empty-01provedall subs proved sgn-empty, sgn-not-empty,
sgn-first-01provedall subs proved sgn-first,
inv-emptyprovedall subs proved inv-one, inv-append, invert-base,
inv-inprovedall subs proved inv-one, inv-append, invert-base,
inv-lenprovedall subs proved inv-one, inv-append, invert-base,
sgn-mklist-05provedall subs proved sgn-empty, sgn-mklist-03,
sgn-last-diffprovedall subs proved sgn-two, sgn-two-01, sgn-base-03, sgn-in, sgn-append, sgn-empty, sgn-one, sgn-last-03,
sgn-last-02provedall subs proved sgn-last-01,
sgn-fillprovedall subs proved sgn-mklist-04, fillsgn-longer, fill-fill,
sgn-ex-01provedall subs proved sgn-mklist-02, sgn-base-01, sgn-base-02, sgn-base-03, sgn-mklist-04,
sgn-append-02provedall subs proved sgn-rec, sgn-zero, sgn-base-02, sgn-base-01, sgn-one, sgn-rec-01, sgn-empty,
invert-restprovedall subs proved inv-rest,
inv-sgnprovedall subs proved sgn-rec, sgn-base-01, invert-one, invert-zero, sgn-base-02, sgn-one, sgn-rec-01, inv-one, inv-append, invert-base, sgn-empty,
inv-last-03provedall subs proved invert-base, inv-one, inv-append,
fix-emptyprovedall subs proved fill-empty, fix-shorter, fix-longer, fix-zero,
fill-lastn-04provedall subs proved fill-rec, fill-length, fillsgn-empty, fill-fill, fill-empty,
fill-lastn-02provedall subs proved fill-lastn-03,
fill-firstprovedall subs proved fillsgn-longer, fill-rec, fill-empty,
fill-fill-01provedall subs proved fill-nls, fill-length, fillsgn-longer,
succ-firstprovedall subs proved succ-zero-01,
inv-one-01provedall subs proved inv-one,
succ-prefixprovedall subs proved succ-rec, succ-one, succ-zero,
sgn-mklist-03provedall subs proved sgn-rec-01, sgn-one,
sgn-sgnprovedall subs proved sgn-base-01, sgn-base-02, sgn-one, sgn-rec-01, sgn-empty,
sgn-last-03provedall subs proved sgn-last,
sgn-two-01provedall subs proved sgn-one, sgn-rec-01,
sgn-twoprovedall subs proved sgn-one, sgn-rec-01,
sgn-base-04provedall subs proved sgn-rec, sgn-one, sgn-base-03,
sgn-last-01provedall subs proved sgn-base-03, sgn-in, sgn-append, sgn-last,
sgn-in-01provedall subs proved sgn-base-01, sgn-base-02, sgn-rec-01, sgn-one,
sgn-mklist-04provedall subs proved sgn-append,
sgn-not-emptyprovedall subs proved sgn-base-01, sgn-base-02, sgn-rec-01, sgn-one,
sgn-zerosprovedall subs proved sgn-rec-01,
sgn-append-03provedall subs proved sgn-rec, sgn-base-01, sgn-base-02, sgn-one, sgn-rec-01,
sgn-zeroprovedall subs proved sgn-base-02, sgn-rec-01, sgn-one,
inv-restprovedall subs proved inv-rec,
inv-falseprovedall subs proved inv-one,
fix-zeroprovedall subs proved fill-zero, fix-longer, fix-shorter,
sgn-length-02provedall subs proved sgn-base-01, sgn-base-02, sgn-one, sgn-rec-01,
sgn-firstprovedall subs proved sgn-base-01, sgn-rec, sgn-base-02, sgn-rec-01, sgn-one,
sgn-exprovedall subs proved sgn-base-01, sgn-base-02, sgn-rec-01, sgn-one, sgn-empty,
fill-lastn-03provedall subs proved fillsgn-longer, fill-lastn, fill-fill,
fill-emptyprovedall subs proved fill-fill, fillsgn-longer, fillsgn-empty,
fill-nlsprovedall subs proved fillsgn-longer, fill-fill,
inv-appendprovedall subs proved inv-rec, invert-base,
succ-trueinprovedall subs proved succ-truein-01,
succ-trueprovedall subs proved succ-zero, succ-empty-01, succ-rec, succ-one, succ-empty,
succ-restprovedall subs proved succ-zero-01,
succ-falsein-02provedall subs proved succ-rec-02, succ-zero-03,
succ-falseprovedall subs proved succ-zero, succ-empty-01, succ-rec, succ-empty,
succ-01provedall subs proved succ-one, succ-rec,
sgn-two-03provedall subs proved sgn-base-03,
sgn-two-02provedall subs proved sgn-base-03,
sgn-true-mklistprovedall subs proved sgn-one, sgn-base-03,
sgn-sgn-01provedall subs proved sgn-rec, sgn-base-01, sgn-base-02, sgn-one, sgn-rec-01, sgn-empty,
sgn-base-05provedall subs proved sgn-base-03,
sgn-2potprovedall subs proved sgn-one, sgn-base-03,
inv-rec-01provedall subs proved inv-rec,
fix-sizeprovedall subs proved fill-length, fix-shorter, fix-longer,
fill-refillprovedall subs proved fill-length, fillsgn-longer,
fill-rec-falseprovedall subs proved fillsgn-fill, fill-fill,
fill-one-02provedall subs proved fill-fill,
fill-one-01provedall subs proved fill-rec-one,
fill-lastn-05provedall subs proved fill-length, fillsgn-empty, fill-rec,
fill-lastprovedall subs proved fill-rec, fillsgn-longer,
fill-inprovedall subs proved fill-fill, fillsgn-longer,
succ-truein-01provedall subs proved succ-zero, succ-rec, succ-empty,
succ-rec-01provedall subs proved succ-rec,
succ-one-01provedall subs proved succ-empty, succ-rec,
succ-zero-01provedall subs proved succ-zero, succ-rec, succ-empty,
succ-zero-03provedall subs proved succ-zero,
succ-rec-02provedall subs proved succ-rec,
succ-falseinprovedall subs proved succ-zero, succ-rec,
succ-empty-01provedall subs proved succ-zero, succ-rec, succ-empty,
succ-oneprovedall subs proved succ-zero,
sgn-lastprovedall subs proved sgn-rec, sgn-base, sgn-one,
sgn-mklist-02provedall subs proved sgn-rec,
sgn-base-02provedall subs proved sgn-base,
sgn-base-01provedall subs proved sgn-base,
inv-mklistprovedall subs proved invert-one, invert-zero, invert-base,
inv-recprovedall subs proved invert-zero, invert-one,
fill-zeroprovedall subs proved fillsgn-longer,
fill-oneprovedall subs proved fillsgn-longer,
sgn-appendprovedall subs proved sgn-rec,
sgn-inprovedall subs proved sgn-rec, sgn-one,
fill-rec-oneprovedall subs proved fillsgn-fill,
fill-lastnprovedall subs proved fillsgn-longer,
fill-recprovedall subs proved fillsgn-fill,
fill-lengthprovedall subs proved fillsgn-fill, fillsgn-empty,
fill-fillprovedall subs proved fillsgn-fill,
inv-oneprovedall subs proved invert-zero, invert-base, invert-one,
sgn-rec-01provedall subs proved sgn-rec,
sgn-base-03provedall subs proved sgn-base,
succ-zeros-03provedall subs proved succ-zero,
succ-zeros-02provedall subs proved succ-zero,
sgn-rec-01-01provedall subs proved sgn-rec,
sgn-mklist-01provedall subs proved sgn-rec, sgn-one,
inv-rew-01provedall subs proved invert-zero,
inv-rewprovedall subs proved invert-one,
inv-last-02provedall subs proved invert-base, invert-zero,
inv-last-01provedall subs proved invert-base, invert-one,
fill-sizeprovedall subs proved fillsgn-longer,
fill-mklistprovedall subs proved fillsgn-longer,
fill-lastn-01provedall subs proved fillsgn-longer,
succ-emptyaxiom
succ-zeroaxiom
succ-recaxiom
invert-oneaxiom
invert-zeroaxiom
fix-longeraxiom
fix-shorteraxiom
sgn-baseaxiom
sgn-emptyaxiom
fillsgn-fillaxiom
fillsgn-emptyaxiom
fillsgn-longeraxiom
invert-baseaxiom
sgn-oneaxiom
sgn-recaxiom