[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 nat-basic1

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:
twols-01provedall subs proved twols-02,
one-02provedall subs proved one,
lstwoprovedall subs proved twols-02,
oneprovedall subs proved numeral-1, disj-1, one-01, s, gen,
twols-02provedall subs proved one-01, numeral-2, numeral-1, disj-1, gen, f,
one-01provedall subs proved zero-01, numeral-2, disj-1, gen, f,
ilf-03provedall subs proved ls-01, s, psh-06,
numeral-2provedall subs proved psh-04, psh-07,
psh-06provedall subs proved s, psh-02, psh-09, psh-03,
psh-08provedall subs proved ls-03, ref-1, psh-02,
psh-05provedall subs proved psh-04, disj-1, numeral-1, psh-07, lrec, elim-1,
pshprovedall subs proved ref-1, psh-02, zero-01,
psh-02provedall subs proved s, psh-09,
psh-07provedall subs proved s-03, trans-1, trans, ls-01, f, s, ls-04, psh-01,
prop-p-01provedall subs proved s-03, trans-1, trans, ls-01, f, ls-04, psh-04,
prop-lsprovedall subs proved ls-02, trans-1, trans, f, ls-04,
lf-08provedall subs proved s-03, trans-1, trans, ls-01, f, ls-04,
lf-07provedall subs proved ls-02, trans-1, trans, f, ls-04,
lf-06provedall subs proved ls-02, trans-1, trans, f, ls-04,
lf-03provedall subs proved ls-02, trans-1, trans, f, ls-04,
lfprovedall subs proved disj-1, trans-1, trans, f, s, ls-04,
psh-09provedall subs proved disj-1, elim-pred-c, s,
transprovedall subs proved disj-1, trans-1, f, s, ls-04,
neqprovedall subs proved ls-03, ls-02, s,
lsprovedall subs proved ref-1, s,
lf-05provedall subs proved ls-02, ls-04,
lf-04provedall subs proved ls-02, ls-04,
lf-02provedall subs proved ls-02, ls-04,
lf-01provedall subs proved ls-02, ls-04,
eqprovedall subs proved s, neq-01, ref-1, lrec,
ls-04provedall subs proved ls-03, ls-02,
sprovedall subs proved ls-03, ls-02, rax,
ls-03provedall subs proved neq-01,
qprovedall subs proved inj-1, disj-1, numeral-1, gen,
psh-01provedall subs proved psh-04, f,
numeral-1provedall subs proved psh-03, sel-1,
neq-01provedall subs proved tot, ls-02,
psu-01provedall subs proved psh-03, psu-02,
prop-pprovedall subs proved psu, psh-03,
ilf-02provedall subs proved s-02, psh-03,
ilf-01provedall subs proved ls-01, psh-04,
ilfprovedall subs proved s-03, psh-04,
totprovedall subs proved rax, lrec, inj-1, zero-01, disj-1, zero, gen,
psh-03provedall subs proved sel-1, psu,
ls-01provedall subs proved f, lrec, gen,
psh-04provedall subs proved lrec, elim-pred-c,
s-03provedall subs proved f, lrec, gen,
psu-04provedall subs proved ref-1, psu, f,
zeroprovedall subs proved z,
psuprovedall subs proved psu-02,
ls-02provedall subs proved ref-1, trans-1, f,
lrecprovedall subs proved f, inj-1, zero-01, disj-1, gen, rax,
psu-03provedall subs proved f, psu-02,
zprovedall subs proved rax, disj-1, gen,
psu-02provedall subs proved elim-pred-c, disj-1,
fprovedall subs proved zero-01,
elim-pred-cprovedall subs proved inj-1, gen, sel-1,
raxprovedall subs proved less-2,
s-02provedall subs proved inj-1, gen,
zero-01provedall subs proved less-1,
s-01provedall subs proved inj-1, gen,
less-1axiom
less-2axiom
elim-1axiom
trans-1axiom
disj-1axiom
ref-1axiom
sel-1axiom
genaxiom
inj-1axiom