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