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