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

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:
twolsprovedall subs proved nls-fst, one-03, s, oz, succ, c, a,
neq-02provedall subs proved c, a, s, less-05,
lslsprovedall subs proved l-05, c, a,
lsprovedall subs proved l, nls-fst, l-02, c, a, z, succ,
less-05provedall subs proved less,
l-05provedall subs proved nls-snd, succ, l-02, c, a, add-base,
nls-fstprovedall subs proved c, a, nls-snd,
q-01provedall subs proved pred, pe, eq-01, l-01, s, succ, c, a, z,
less-04provedall subs proved c, a, l, less,
betweenprovedall subs proved l-01, succ, succ-03, c, a, l,
addexprovedall subs proved eq-01, eq, one-01, s, oz, succ, c, a, l-01,
lessprovedall subs proved l-03, c, a, l,
nls-sndprovedall subs proved c, a, l-02,
l-01provedall subs proved l-02, s, oz, succ, c, a, z,
two-02provedall subs proved z-01, two-01, succ, c, a,
threeprovedall subs proved two-01, eq-01, one-03, oz, succ, c, a,
qprovedall subs proved eq, even, even-06, eq-01, c, a, oz, succ,
plsprovedall subs proved l, oz, succ, s, c, a, l-03,
lpprovedall subs proved c, a, l-02, succ,
less-03provedall subs proved l-03, c, a, l,
l-08provedall subs proved c, a, l-02,
ex-oddevenprovedall subs proved even, even-06, eq-01, succ, c, a, oz,
even-05provedall subs proved l-03, c, a, l-02, l,
even-02provedall subs proved l-04, l, oz, succ, z-01, c, a, l-03,
two-01provedall subs proved eq, one-01, one-03, oz, succ, c, a,
even-06provedall subs proved even, eq-01, z-01, succ, even-01, c, a,
l-02provedall subs proved z-01, l, c, a, oz, succ,
l-03provedall subs proved c, a, l,
neqprovedall subs proved l, s, oz, c, eq-01, a, succ,
less-06provedall subs proved c, a, l,
less-02provedall subs proved c, a, l,
less-01provedall subs proved c, a, l,
l-07provedall subs proved c, a, l,
l-06provedall subs proved c, a, l,
expand-natprovedall subs proved c, a, l,
even-04provedall subs proved even-01, eq-01, succ, c, a,
even-01provedall subs proved one-02, succ, c, a,
lprovedall subs proved l-04, s, succ, c, a, z,
succ-03provedall subs proved c, a, s,
one-01provedall subs proved one-03, one-02, c, a,
pseprovedall subs proved pe, oz, one-03, c, pred, a, succ,
neq-01provedall subs proved c, a, s,
peprovedall subs proved eq-01, c, pred, a, succ,
one-02provedall subs proved z-01, one-03, succ, z, c, a,
sprovedall subs proved l-addone, succ, c, a, oz,
twoprovedall subs proved even, c, a,
oneprovedall subs proved z-01, oz, one-03, succ, c, a, z,
l-addoneprovedall subs proved succ,
predprovedall subs proved eq-01, succ, c, a, z-01,
one-03provedall subs proved c, a, eq,
evenprovedall subs proved oz, eq-01, succ, z-01, c, a,
psprovedall subs proved c, a, z-01, succ,
pe-01provedall subs proved eq-01, succ, z, c, a, z-01,
eq-inc-neqprovedall subs proved c, a, z-01, eq,
succprovedall subs proved c, a, z, add-rec, one-def,
ozprovedall subs proved c, a, z-01,
eqprovedall subs proved eq-01, c, a, z,
eqsprovedall subs proved c, a, eq-01,
cprovedall subs proved rec, add-rec, z, a, add-base,
aprovedall subs proved add-rec, eq-01, add-base,
eq-01provedall subs proved rec, z,
z-01provedall subs proved add-rec, add-base,
zprovedall subs proved add-rec,
recprovedall subs proved add-rec, add-base,
one-defprovedall subs proved
l-04provedall subs proved
add-baseaxiom
add-recaxiom