[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 list-data

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:
lfprovedall subs proved fr-06, lf-01, l, lfr,
fr-01provedall subs proved fr-02, fr,
lfrprovedall subs proved fr-02, fr-07, l,
fr-06provedall subs proved fr-07,
frprovedall subs proved fr-02, fr-07,
lr-01provedall subs proved lr-02, size-02, disj-1, elim-list-c,
le-one-01provedall subs proved sel-2, l, size-02, disj-1, gen, fr-07, lf-01,
fr-05provedall subs proved fr-07, fr-02,
fr-03provedall subs proved fr-07,
eq-oneprovedall subs proved disj-1, l, size-02, elim-list-c, fr-07, lf-01,
lr-02provedall subs proved l, length-rest,
fr-07provedall subs proved inj-1, elim-list-c, fr-02,
lr-06provedall subs proved l, length-rest, size-01,
lr-05provedall subs proved length-rest, l,
lr-04provedall subs proved l, length-rest, size-01,
lr-03provedall subs proved l, length-rest,
lrprovedall subs proved l, length-rest,
length-rest-introprovedall subs proved l, length-rest,
fr-04provedall subs proved fr-02, elim-list-c,
elim-listprovedall subs proved sel-2, sel-1, fr-02,
length-restprovedall subs proved size-02, disj-1, elim-list-c,
lf-01provedall subs proved f, l, size-02, disj-1, size-01, elim-list-c,
fr-02provedall subs proved elim-list-c,
elim-list-cprovedall subs proved f, gen, sel-2, sel-1,
le-oneprovedall subs proved l,
lprovedall subs proved size-02, gen, size-01,
fprovedall subs proved inj-1,
p-frprovedall subs proved sel-2, sel-1,
exaprovedall subs proved disj-1, gen,
size-01axiom
inj-1axiom
size-02axiom
disj-1axiom
genaxiom
sel-1axiom
sel-2axiom