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