[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 split-finalzeros

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:
finz-add-neqprovedall subs proved finz-add-notless, finz-add-bigger,
finz-add-notleqprovedall subs proved finz-add-notless,
finz-add-notlessprovedall subs proved finz-add-bigger,
rew-finzprovedall subs proved finz-bounded-02,
finz-bounded-04provedall subs proved finz-bounded-02, finz-bounded,
finz-bounded-01provedall subs proved finz-bounded,
finz-add-leqprovedall subs proved finz-add-bigger,
finz-bounded-02provedall subs proved split-unique-2, split-ok,
finz-boundedprovedall subs proved lead-is-odd, split-ok,
finz-add-biggerprovedall subs proved pot2-even, pot2-odd, lead-is-odd, split-ok,
lead-notzeroprovedall subs proved lead-is-odd,
pot2-evenprovedall subs proved pot2-odd,
split-unique-2provedall subs proved finz-odd, lead-odd, finz-even, lead-even,
split-okprovedall subs proved lead-odd, finz-odd, lead-even, finz-even,
lead-is-oddprovedall subs proved lead-odd, lead-even,
split-uniqueprovedall subs proved lead-odd, finz-odd, lead-even, finz-even,
finz-bounded-05provedall subs proved finz-odd, finz-even,
finz-bounded-03provedall subs proved finz-odd, finz-even,
finz-biggerprovedall subs proved finz-odd, finz-even,
lead-evenaxiom
lead-oddaxiom
finz-evenaxiom
finz-oddaxiom
pot2-oddprovedall subs proved