[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 nat

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:
ls-add-not-03provedall subs proved le-sum, ls-add-not-01,
ls-add-not-01provedall subs proved ls-add-not,
ls-add-not-02provedall subs proved le-sum, ls-add-not,
le-add-02provedall subs proved le-add, eqle-one, le-addex,
le-add-01provedall subs proved le-add, lep-02,
ls-add-notprovedall subs proved le-ls-simp, lels-01, lep-02, le-sum, trans-ls-le,
le-addprovedall subs proved ler, lep-01,
sub-succprovedall subs proved sub-add, fle, ls-03, eq-02, le-ls-simp, lels-01,
sub-add-01provedall subs proved eq-01, sub-add, ls-03, le-ls-simp, lels-01, elim-sub,
predprovedall subs proved num-01, rec, lels-01, elim-pred-c,
add-sub-lessprovedall subs proved sub-add, fle, ls-03, eq-02, le-ls-simp, lels-01,
recprovedall subs proved add-01,
le-sumprovedall subs proved lep-02, ls-le-simp, succ-01, lels, anti, ler, le-one, fle, le-ls-simp, lels-01, lez-01,
le-addexprovedall subs proved lez-01, le-rec, lep,
lep-01provedall subs proved one-01, lep-02, lez-01, ler,
sub-addprovedall subs proved add,
succ-04provedall subs proved num-01, add-01,
prop-06provedall subs proved cancel-01, elim-pred-c,
prop-05provedall subs proved eq-01, add-01, elim-sub,
prop-02provedall subs proved eq-01, add-01, elim-sub,
propprovedall subs proved cancel-01, elim-pred-c,
pred-02provedall subs proved cancel-01, elim-pred-c,
not-zeroprovedall subs proved lez-01,
lessprovedall subs proved ls-le-simp, lep-02, elim-sub, zero-01, eq-02, lels-03, lels-02, zero-02, fle, lels,
lels-04provedall subs proved pls,
add-03provedall subs proved add-01,
addprovedall subs proved eq-02, le-ls-simp, lels-01,
cancel-01provedall subs proved eq-01, shift-01, lels-01, lep-02, elim-sub,
zero-02provedall subs proved zero-01, lels-02, zero,
plsprovedall subs proved fle, ls-le-simp, lep-02, anti, lels,
le-recprovedall subs proved lels-01, lels-02,
lez-01provedall subs proved lels-02,
eqle-oneprovedall subs proved ls-le-simp, lels, succ-01,
add-01provedall subs proved fle, eq-02, le-ls-simp, lels-01,
succprovedall subs proved eq-01,
sub-sameprovedall subs proved eq-02, ls-03, le-ls-simp, lels-01, elim-sub,
sub-ls-rewprovedall subs proved elim-sub, ls-01, lels-03,
sub-le-rewprovedall subs proved lep-02, elim-sub, ls-03, le-ls-simp, lels-01,
prop-07provedall subs proved eq-02, lels-03,
prop-04provedall subs proved ls, lels-01,
pred-01provedall subs proved num-02, zero-01,
one-02provedall subs proved lels-02,
ls-predprovedall subs proved ls-01, fle, lels, succ-01, ls-02, lels-01,
ls-07provedall subs proved elim-sub, ls-01, le-ls-simp, lels-01,
ls-06provedall subs proved ls-01, le-ls-simp, lels-01, sub-base,
ls-05provedall subs proved zero-01,
ls-04provedall subs proved elim-sub, ls-01, le-ls-simp, lels-01,
less-03provedall subs proved elim-sub, eq-02, lels, ls-01, le-ls-simp, lels-01,
less-02provedall subs proved ls-le-simp, lels, lep, elim-sub,
less-01provedall subs proved le, le-ls-simp, lels-01, lep-02,
lesprovedall subs proved lep-02, lels-02,
leprfprovedall subs proved succ-01, ls-02, lels-01,
leprprovedall subs proved succ-01, ls-02, lels-01,
le-num-05provedall subs proved ls-02, lels-03,
le-num-04provedall subs proved ls-03, lels-03,
le-num-02provedall subs proved le, lels-03,
l-num-05provedall subs proved ls, lels-03,
l-num-04provedall subs proved ls-01, lels-03,
geprovedall subs proved lels-01, ls-le-simp, ge-def,
eq-pred-01provedall subs proved eq-01,
eq-predprovedall subs proved eq-01,
eq-03provedall subs proved eq-01,
add-num-04provedall subs proved eq-02, lels-03, eq-01,
add-num-02provedall subs proved eq-02, lels-03,
add-num-01provedall subs proved eq-02, lels-03,
add-ls-right2-leprovedall subs proved le-ls-simp, lels-01, lep-02, trans-le-le, ls-le-simp, lels,
add-le-right2-lsprovedall subs proved trans-le-le, ls-le-simp, lep-02, lels,
zeroprovedall subs proved lels-01, elim-sub,
trans-ls-leprovedall subs proved le-ls-simp, fle, lels,
zero-01provedall subs proved ler, lels-03, elim-sub,
lels-02provedall subs proved le-ls-simp, lels-03,
ls-02provedall subs proved lep-02, elim-sub,
leprovedall subs proved lep-02, elim-sub,
lsprovedall subs proved elim-sub,
ls-01provedall subs proved elim-sub,
ls-03provedall subs proved lep-02, elim-sub,
eq-01provedall subs proved lels-01, elim-sub,
ls-le-simpprovedall subs proved le-ls-simp,
trans-le-leprovedall subs proved le-ls-simp, fle, lels-01,
eq-02provedall subs proved elim-sub,
trans-le-lsprovedall subs proved le-ls-simp, fle, lels,
succ-05provedall subs proved elim-pred-c, lep, lels-01, elim-sub,
succ-02provedall subs proved lels-01, le-ls-simp,
sub-lsprovedall subs proved lep, lels-01, elim-sub,
prop-01provedall subs proved elim-sub,
neq-01provedall subs proved le-ls-simp, succ-01,
letprovedall subs proved le-ls-simp, fle, lels-01,
le-num-01provedall subs proved lep-02, lels-03, elim-sub,
l-num-02provedall subs proved lels-03, elim-sub,
l-num-01provedall subs proved lels-03, elim-sub,
fle-01provedall subs proved le-ls-simp, fle, lels,
le-oneprovedall subs proved fle, lels-01,
elim-subprovedall subs proved elim-pred-c, num-01, shift-01, num-02, lels-01, succ-01, sub-base,
le-ls-simpprovedall subs proved fle,
elim-pred-cprovedall subs proved num-01, num-02,
lep-02provedall subs proved succ-01, lez, lep,
fleprovedall subs proved ler, anti, lels-01, lels,
shiftprovedall subs proved shift-01,
lezprovedall subs proved lels-01,
lepprovedall subs proved lels-01,
lerprovedall subs proved lels-01,
num-02provedall subs proved num-01,
shift-01provedall subs proved rax, sub-base,
le-num-03provedall subs proved lels-01,
raxprovedall subs proved pred-03, sub-rec,
one-01provedall subs proved succ-01,
num-01provedall subs proved pred-03,
lels-01provedall subs proved lels, le-def,
le-num-06provedall subs proved succ-01,
l-num-03provedall subs proved succ-01, lels,
eqprovedall subs proved succ-01,
add-02provedall subs proved succ-01,
pred-03provedall subs proved sub-base, sub-rec,
antiprovedall subs proved le-def,
lels-03provedall subs proved le-def,
lelsprovedall subs proved le-def,
succ-01provedall subs proved le-def,
sub-recaxiom
ge-defaxiom
sub-baseaxiom
le-defaxiom