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

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:
plsprovedall subs proved s-04, c, a, neq-02, ls-04, l-03,
neq-02provedall subs proved ref, l, c, a, s-04, less-05, f,
twolsprovedall subs proved numeral-1, z-01, one-01, numeral-2, rec, less-2, disj, gen, f, c, a,
psh-08provedall subs proved ref, psu-03, trans, trans-01, f, neq-01, psh,
ilf-03provedall subs proved l-02, eq-02, ls-04, c, a, succ, psh-06,
ilfprovedall subs proved c, a, lp, succ,
numeral-2provedall subs proved psh-04, psh-01, succ,
pshprovedall subs proved l-02, psh-04, c, a, eq-02, succ, psh-03, ls-04, less-1,
less-05provedall subs proved less,
psh-06provedall subs proved a, succ, psh-09, psh-03,
lpprovedall subs proved c, a, l-02, succ, psh-04,
psh-05provedall subs proved psh-01, lrec, psh-04, numeral-1, disj, elim,
psh-02provedall subs proved c, a, s-04, succ, psh-09,
prop-p-01provedall subs proved c, a, nls-fst, succ, psh-04,
one-02provedall subs proved one,
less-04provedall subs proved c, a, l, ls-02, less, f, ls-04,
ilf-01provedall subs proved c, a, l-02, succ, psh-04,
even-02provedall subs proved z-01, l-04, eq-01, elim-pred-c, neq-04, psh-09, l-02, eq-02, s-04, oz, succ, gen, ref, l, f, ls-04, c, a, l-03,
betweenprovedall subs proved ref, l-01, succ, trans, trans-01, succ-03, f, c, a, l,
oneprovedall subs proved one-06, oz, c, a, one-01, s-04, succ, gen,
lessprovedall subs proved ls-02, eq-01, c, a, ref, l, l-03, f, ls-04,
psh-04provedall subs proved l-05, trans, trans-01, l-02, eq-02, eq-01, elim, ref, pred, oz, one-06, psh-03, f, c, a, s-04, ls-04, psh-01, succ,
psh-09provedall subs proved oz, elim, c, a, s-04, succ,
neq-04provedall subs proved ls-03, ls-02, c, a, s-04,
succ-03provedall subs proved c, a, s-04, neq-01,
sprovedall subs proved c, a, s-04, succ,
q-add-01provedall subs proved l-05, trans, trans-01, neq-01, nls-fst, l-02, oz, f, ref, s-04, eq-02, one-06, eq-01, elim-pred-c, succ, c, a, z-02, gen, ls-04,
psh-07provedall subs proved nls-fst, c, a, s-04, ls-04, psh-01, succ,
neq-03provedall subs proved ls-02, l, ls-04, s-04, oz, c, eq-01, a, succ, gen, f,
lsprovedall subs proved c, a, ref, s-04, succ,
lfprovedall subs proved l, oz, trans, trans-01, f, c, a, s-04, ls-04, succ,
less-03provedall subs proved l-03, ref, ls-02, l, c, a, eq-01, f, ls-04,
even-05provedall subs proved l-03, c, a, l-02, l, f,
eqprovedall subs proved s-04, neq-01, c, a, l, succ,
addexprovedall subs proved ref, eq-01, eq-02, one-04, less-1, ls-04, s-04, oz, succ, gen, f, c, a, l-01,
psh-01provedall subs proved c, a, l, elim, f, succ,
l-03provedall subs proved l, eq-01, less-1, z-02, c, a, rec, less-2, disj, gen, f,
s-04provedall subs proved oz, eq-01, ls-04, ref, l, trans, trans-01, f, succ, z, one-01, c, a, gen,
ls-05provedall subs proved l, nls-fst, l-02, c, a, z-02, succ, gen,
less-06provedall subs proved succ, trans, trans-01, c, a, ls-02, l, f, ls-04,
less-02provedall subs proved succ, trans, trans-01, l, ls-02, c, a, f, ls-04,
less-01provedall subs proved succ, trans, trans-01, ls-02, c, a, l, f, ls-04,
l-07provedall subs proved c, a, ls-02, l,
l-06provedall subs proved c, a, ls-02, ls-04, l,
expand-natprovedall subs proved c, a, ls-02, ls-04, l,
lprovedall subs proved neq-01, ls-02, eq-02, ref, oz, l-addone, eq-01, l-05, trans, trans-01, l-04, f, ls-04, l-08, succ, less-1, l-02, c, a, z-02, gen,
twols-01provedall subs proved twols-02,
twols-02provedall subs proved lstwo,
l-08provedall subs proved l-02, l-05, c, a, succ, trans, trans-01, f, ls-04,
lslsprovedall subs proved l-05, c, a,
lstwoprovedall subs proved nls-fst, oz, c, a, one-06, succ, gen, f,
one-01provedall subs proved nls-fst, c, a, oz, succ, gen, f,
l-05provedall subs proved nls-fst, l-02, succ, trans, trans-01, c, a, z-02, gen, f,
lf-08provedall subs proved c, a, nls-fst, succ,
nls-fstprovedall subs proved c, a, nls-snd,
threeprovedall subs proved two-01, disj, numeral-1, rec, gen, c, a,
q-addprovedall subs proved eq-02, even, even-06, eq-01, c, a, oz, succ, gen,
ex-oddevenprovedall subs proved even, even-06, eq-01, succ, c, a, oz, gen,
two-01provedall subs proved disj, one-04, numeral-1, rec, gen, c, a,
nls-sndprovedall subs proved succ, trans, trans-01, c, a, l-02, f, ls-04,
l-addoneprovedall subs proved l-02, c, a, eq-02, ls-04,
even-06provedall subs proved even, eq-01, z-01, succ, even-01, c, a, gen,
l-01provedall subs proved l-02, eq-02, ls-04, ref, c, a, z-02,
zeroprovedall subs proved less-1, neq-01,
psu-02provedall subs proved psu, c, a, oz, succ,
psu-01provedall subs proved psu, psh-03, c, a, pred, pse, succ,
prop-pprovedall subs proved psu, psh-03,
prop-lsprovedall subs proved ls-02, succ, trans, trans-01, f, ls-04,
lf-07provedall subs proved ls-02, succ, trans, trans-01, f, ls-04,
lf-06provedall subs proved ls-02, succ, trans, trans-01, f, ls-04,
lf-05provedall subs proved ls-02, ls-04,
lf-04provedall subs proved ls-02, ls-04,
lf-03provedall subs proved ls-02, succ, trans, trans-01, f, ls-04,
lf-02provedall subs proved ls-02, ls-04,
lf-01provedall subs proved ls-02, ls-04,
even-04provedall subs proved even-01, numeral-1, add-rec, rec, a, gen,
pseprovedall subs proved pred, pe, one-06, c, a, oz, succ, elim,
psu-03provedall subs proved c, a, pred, pe, f, succ,
psuprovedall subs proved c, a, pred, pe, succ,
even-01provedall subs proved one-05, succ, c, a, gen,
neq-01provedall subs proved ls-03, ls-02,
ls-04provedall subs proved ls-03, ls-02,
one-04provedall subs proved one-06, one-05, c, a,
two-02provedall subs proved disj, numeral-1, add-rec, rec, a, gen,
qprovedall subs proved inj, disj, numeral-1, gen,
psu-04provedall subs proved ref, c, a, pred, pe, f, succ,
peprovedall subs proved eq-01, c, pred, a, succ, elim,
ls-03provedall subs proved tot, ref,
numeral-1provedall subs proved psh-03, c, a, pred, succ,
one-05provedall subs proved z-01, one-06, succ, z-02, gen, c, a,
twoprovedall subs proved even, c, a,
psprovedall subs proved eq-01, pred, c, a, oz, gen, succ,
pe-01provedall subs proved eq-01, c, pred, a, succ, gen, f,
one-03provedall subs proved z-01, oz, one-06, succ, c, a, z-02, gen,
predprovedall subs proved eq-01, succ, c, a, z-01, elim-pred-c,
one-06provedall subs proved c, a, eq-02,
totprovedall subs proved lrec, neq, inj, disj, f, ls-02, less-2, z, gen,
evenprovedall subs proved oz, eq-01, elim-pred-c, succ, z-01, c, a, gen,
s-02provedall subs proved c, a, eq-02, succ,
s-01provedall subs proved eq-02, c, a, succ,
ilf-02provedall subs proved c, a, eq-02, succ, psh-03,
eq-inc-neqprovedall subs proved c, a, z-01, eq-02,
ls-02provedall subs proved c, a, l-02, succ, trans, trans-01, f,
elim-pred-cprovedall subs proved c, a, eq-01, succ, psh-03,
eq-02provedall subs proved eq-01, c, a, z-02,
s-03provedall subs proved l-02, c, a, succ,
ls-01provedall subs proved c, a, l-02, succ,
eqsprovedall subs proved c, a, eq-01,
succprovedall subs proved inj, rec, c, a, gen,
ozprovedall subs proved c, a, z-01,
eq-01provedall subs proved inj, rec, c, a, z-02, gen,
l-02provedall subs proved lrec, a, rec, disj, gen, f,
trans-01provedall subs proved lrec, less-2, disj, gen, trans, f,
cprovedall subs proved inj, rec, add-rec, z-02, a, add-base, gen,
lrecprovedall subs proved f, inj, less-1, disj, gen, less-2,
z-01provedall subs proved disj, add-rec, add-base, gen, a,
z-02provedall subs proved inj, add-rec, a, gen,
recprovedall subs proved add-rec, inj, a, add-base, gen,
neqprovedall subs proved less-2,
zprovedall subs proved less-2, disj, gen,
psh-03provedall subs proved elim, sel,
aprovedall subs proved inj, add-rec, add-base, gen,
fprovedall subs proved less-1,
zero-01provedall subs proved less-1,
selaxiom
elimaxiom
less-2axiom
disjaxiom
l-04provedall subs proved
transaxiom
less-1axiom
refaxiom
genaxiom
add-baseaxiom
add-recaxiom
injaxiom