[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 int-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:
ex-oddevenprovedall subs proved add-pred-01, eq, pred, add-in, succ-01, add-c, add-a, zero-07,
pls-04provedall subs proved add-c, add-a, nls,
rewzprovedall subs proved mone-01, add-c, add-a, mone-03,
pls-03provedall subs proved add-c, add-a, nls,
ttwoprovedall subs proved pls, add-c, add-a, nls,
mone-01provedall subs proved succ-01, add-c, add-a, add-less, mone-03,
nlsprovedall subs proved pls, add-c, add-a, ls-01,
zero-07provedall subs proved zero-06, zero, add-c, add-a,
zero-03provedall subs proved add-c, add-a, add-less, ls,
ex-ls-addprovedall subs proved zero-02, eq, add-pred-01, add-in, ls-01, lst-03, succ-01, add-zero-rev, add-c, add-a, add-less,
pls-01provedall subs proved add-c, add-a, zero-01, ls,
plstprovedall subs proved pls, add-c, add-a, ls-add-both,
lst-05provedall subs proved add-c, pls,
zeroprovedall subs proved add-c, add-a, ls-02,
plsprovedall subs proved lst-02, add-pred-01, lst-03, succ-01, add-c, add-a, ls, add-zero-rev,
zero-01provedall subs proved add-c, add-a, ls-02,
add-lessprovedall subs proved add-c, add-a, ls-02,
predprovedall subs proved add-c, add-a, add-in, succ-01,
add-succ-01provedall subs proved add-c, add-a, add-in, succ-01,
ls-succ-03provedall subs proved add-c, add-a, lst-03, ls, succ-01,
lstprovedall subs proved add-c, add-a, lst-04,
ls-succ-02provedall subs proved add-c, add-a, ls-add-both, succ-01, lst-02, ls-01,
plst-01provedall subs proved ls-01, lst-04, lst-01, add-c, add-a, lst-03,
ls-succ-01provedall subs proved add-c, add-a, ls-add-both, succ-01, lst-03, ls-01,
lst-01provedall subs proved add-c, add-a, ls-01,
zero-06provedall subs proved add-c, add-a, zero-05,
ls-02provedall subs proved add-c, add-a, add-zero-rev, ls-01,
lst-02provedall subs proved add-c, add-a, ls-01,
ls-add-bothprovedall subs proved add-c, add-a, ls-01,
lst-04provedall subs proved add-c, add-a, ls-01,
mone-03provedall subs proved add-c, add-a, zero-05,
lst-03provedall subs proved add-c, add-a, ls-01,
add-inprovedall subs proved add-pred-01, succ-01, add-c, add-a, add-zero-rev,
neq-01provedall subs proved add-c, add-a, ls-01,
num-betweenprovedall subs proved add-c, add-a, ls-01, succ-01,
mthreeprovedall subs proved add-c, add-a, zero-05,
succprovedall subs proved add-c, add-a, eq, succ-01,
ls-zeroprovedall subs proved add-c, add-a, ls-01, succ-01,
mone-02provedall subs proved succ-01, add-a, add-c,
zero-05provedall subs proved add-c, add-a, ls,
zero-02provedall subs proved add-c, add-a, ls,
ls-01provedall subs proved add-pred-01, add-succ-02, add-c, add-a, add-zero-rev,
succ-01provedall subs proved add-c, add-a, add-zero-rev, add-succ,
eqprovedall subs proved add-pred, add-succ, add-c, add-a, add-zero,
pls-02provedall subs proved add-c, add-a, ls,
ls-03provedall subs proved add-c, add-a, ls,
neqprovedall subs proved add-c, add-a, ls,
not-zero-posprovedall subs proved add-c, add-a, ls,
add-cprovedall subs proved add-pred-01, add-pred, add-succ-02, add-succ, add-a, add-zero-rev, add-zero,
add-pred-01provedall subs proved add-succ-02,
add-succ-02provedall subs proved add-pred, add-succ, add-a, add-zero,
lsprovedall subs proved add-pred, add-succ, add-a, add-zero,
add-zero-revprovedall subs proved add-pred, add-succ,
add-aprovedall subs proved add-pred, add-succ, add-zero,
add-zeroaxiom
add-succaxiom
add-predaxiom