[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 real-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:
neg-14provedall subs proved neg-zero, add-comm, add-assoc, zero-07, negeq,
neg-zeroprovedall subs proved neg-10, add-comm, add-assoc, sub-eq-01, neg,
neg-02provedall subs proved add-comm, add-assoc, add-zero, negr-ls,
eqint-subprovedall subs proved eqint-neg, eqint-add,
neg-eqprovedall subs proved double-neg,
mone-02provedall subs proved add-comm, add-assoc, mone,
moneprovedall subs proved negeq, add-comm, add-assoc, sub-eq-01, add-in,
neg-10provedall subs proved add-comm, add-assoc, add-zero, negeq,
double-negprovedall subs proved add-comm, add-assoc, sub-eq-01, negeq,
eqint-negprovedall subs proved eqint-num, add-comm, add-assoc, sub-eq-01, eqint-add, negeq,
negr-lsprovedall subs proved negl-ls, negeq, irref, plst, ls-num, bls-01, l, add-comm, add-assoc, sub-eq-01,
neg-12provedall subs proved add-comm, add-assoc, add-zero, sub-eq, negeq,
rew-eqzeroprovedall subs proved negeq, add-comm,
rew-eqzero-01provedall subs proved negeq,
mone-01provedall subs proved negeq, add-comm,
negeqprovedall subs proved add-in, add-comm, add-assoc, sub-eq-01,
eqnum-addboth1provedall subs proved add-comm, add-assoc, add-in, eqint-add,
eqnum-addboth2provedall subs proved add-comm, add-assoc, add-in, eqint-add,
eqnum-add1provedall subs proved add-comm, add-assoc, add-in, eqint-add,
lst-05provedall subs proved not-zero-pos, irref, bls-01, add-comm, add-assoc, add-less, trans, ls, less-add-cancel-l, eq, add-in, ls-02, ex-ls-add, add-zero, pls, l,
neg-addprovedall subs proved add-assoc, add-comm, add-zero, sub-eq-01, add-in,
zero-07provedall subs proved not-zero-pos, zero, blst-01, add-comm, add-assoc, add-zero,
add-inprovedall subs proved bls-01, add-comm, add-assoc, irref, less-add-cancel-l, blst-01,
ttwoprovedall subs proved lf-07, less-add-cancel-l, trans, add-comm, add-assoc, nls,
zero-03provedall subs proved bls-01, add-comm, add-assoc, ls, trans, l, zero-05,
pls-03provedall subs proved add-comm, add-assoc, nls,
pls-04provedall subs proved add-comm, add-assoc, nls,
ex-ls-addprovedall subs proved neg-09, add-zero, sub-eq-01, add-comm, add-assoc, add-less,
blst-01provedall subs proved blst-02,
zero-05provedall subs proved add-comm, add-assoc, add-zero, blst-02, not-zero-pos,
plstprovedall subs proved lf-07, irref, add-assoc, less-add-cancel-l, add-comm, pls, bls-01, blst-02,
nlsprovedall subs proved lf-07, irref, add-comm, add-assoc, less-add-cancel-l, blst-02, pls,
lsnum-add3provedall subs proved add-comm, add-assoc, add-less, ls-02, eqint-add,
lstprovedall subs proved add-comm, add-assoc, lst-04,
lst-02provedall subs proved bls-01, add-comm, add-assoc, less-add-cancel-l, trans, l, neq-01,
lsls-add-notgrprovedall subs proved add-comm, add-assoc, less-add-cancel-l, bls-01, trans-lem,
plst-01provedall subs proved lst-04, trans, add-comm, add-assoc, irref, less-add-cancel-l, bls-01, l,
trans-lemprovedall subs proved lf-07, trans,
neq-01provedall subs proved lf-07, add-comm, add-assoc, less-add-cancel-l,
lst-04provedall subs proved add-comm, add-assoc, bls-01, less-add-cancel-l, lf-07,
blst-02provedall subs proved l, irref,
add-lessprovedall subs proved irref, add-comm, add-assoc, bls-01, ls, eq, l,
blstprovedall subs proved lf-07, trans,
lf-02provedall subs proved lf-07,
lf-03provedall subs proved lf-07,
lf-04provedall subs proved lf-07, lf-08,
lf-05provedall subs proved lf-07,
lf-06provedall subs proved lf-07,
neg-01provedall subs proved add-comm, add-assoc, neg-09, negl-ls,
forward-posprovedall subs proved lf-07, trans,
trans-lem3provedall subs proved lf-07, lf-08,
neqprovedall subs proved add-comm, add-assoc, bls-01, l, ls,
forward-any-lsleprovedall subs proved lf-07, lf-08,
zero-06provedall subs proved not-zero-pos, l, add-comm, add-assoc, add-zero,
zero-02provedall subs proved add-comm, add-assoc, bls-01, ls, trans, not-zero-pos, l,
zero-01provedall subs proved add-comm, add-assoc, ls-zero, zero, l,
pls-01provedall subs proved ls, trans, bls-01, add-comm, add-assoc, add-zero, l,
lst-01provedall subs proved add-comm, add-assoc, bls-01, less-add-cancel-l, trans, l,
lst-03provedall subs proved lf-07, add-comm, add-assoc, less-add-cancel-l,
mone-03provedall subs proved ls-num, add-zero, less-add-cancel-l, eqint-num, add-comm, add-assoc, eqint-add, l,
pls-02provedall subs proved trans, bls-01, add-comm, add-assoc, ls, l,
lprovedall subs proved total, irref, lf-08, bls-01,
neg-09provedall subs proved add-comm, add-assoc, add-zero, negradd-ls,
lf-07provedall subs proved lf-08,
neg-05provedall subs proved add-comm, add-assoc, add-zero, negl-ls,
neg-08provedall subs proved add-comm, add-assoc, add-zero, negladd-ls,
negaddprovedall subs proved add-comm, add-assoc, negradd-ls, negladd-ls,
sub-ls-02provedall subs proved add-comm, add-assoc, negladd-ls,
eqnum-add2provedall subs proved add-comm, add-assoc, eq, eqint-add,
negadd-eqprovedall subs proved add-assoc, add-comm, add-zero, sub-eq-01, sub-eq,
ls-zeroprovedall subs proved add-comm, add-assoc, bls-01, ls-02, trans,
zeroprovedall subs proved irref, trans, add-comm, add-assoc, add-zero, pls,
not-zero-posprovedall subs proved irref, add-comm, add-assoc, ls-02, add-zero, trans, less-add-cancel-l,
eqprovedall subs proved sub-eq-01, add-comm, add-assoc, add-zero,
lf-08provedall subs proved trans, bls-01, total,
negladd-lsprovedall subs proved add-assoc, add-comm, add-zero, sub-eq-01, less-add-cancel-l,
negradd-lsprovedall subs proved add-assoc, add-comm, add-zero, sub-eq-01, less-add-cancel-l,
negl-lsprovedall subs proved add-comm, add-assoc, sub-eq-01, less-add-cancel-l,
sub-eqprovedall subs proved add-assoc, add-comm, add-zero, sub-eq-01,
ls-03provedall subs proved add-comm, add-assoc, ls,
lsls-add-noteqprovedall subs proved add-comm, add-assoc, irref, less-add-cancel-l, pls,
lsnum-add2provedall subs proved add-comm, add-assoc, ls, eqint-add,
inv-addprovedall subs proved add-comm, add-assoc, sub-eq-01,
ls-02provedall subs proved add-comm, add-assoc, add-zero, less-add-cancel-l,
plsprovedall subs proved add-assoc, trans, add-comm, less-add-cancel-l,
lsprovedall subs proved add-comm, add-assoc, add-zero, less-add-cancel-l,
bls-01provedall subs proved irref, trans,
sub-eq-01provedall subs proved add-comm, add-assoc, neg,
lsnum-addboth2provedall subs proved add-comm, add-assoc, less-add-cancel-l, eqint-add,
lsnum-addboth1provedall subs proved add-comm, add-assoc, less-add-cancel-l, eqint-add,
betweenlsls-zero-oneprovedall subs proved ls-num,
lsnum-add1provedall subs proved add-comm, add-assoc, less-add-cancel-l, eqint-add,
trans-lem2provedall subs proved trans,
ex-oddevenprovedall subs proved add-comm, add-assoc,
lsnum-add4provedall subs proved add-comm, add-assoc, less-add-cancel-l, eqint-add,
negaxiom
eqint-numaxiom
ls-numaxiom
less-add-cancel-laxiom
eqint-addaxiom
irrefaxiom
totalaxiom
add-zeroaxiom
transaxiom
add-assocaxiom
add-commaxiom