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