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