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

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-notlssuccprovedall subs proved less-less-leftsucc, less-fin, add-comm, add-assoc, add-all-zero, add-ls-cancel-num-04,
less-less-leftsuccprovedall subs proved ls-natinf-to-nat-2-1, less-fin, eq-natinf-to-nat-2-1, inf-less, addeqinf-cancel, add-less, lsle-trans, ls-irref, add-comm, add-assoc, add-all-zero, add-ls-cancel-num-04,
eqls-succprovedall subs proved add-comm, add-assoc, add-all-zero, add-ls-cancel-num-04,
add-ls-cancel-num-04provedall subs proved add-comm, add-ls-cancel-01, add-assoc, add-fin,
eqsucc-lsprovedall subs proved less-inf1, add-inf2, add-comm, add-assoc, add-less,
add-ls-cancel-num-03provedall subs proved add-comm, add-assoc, add-ls-cancel-01, add-fin,
add-ls-cancel-num-02provedall subs proved add-comm, add-ls-cancel-01, add-assoc, add-fin,
add-ls-cancel-num-01provedall subs proved add-comm, add-assoc, add-ls-cancel-01, add-fin,
add-cancel-num-04provedall subs proved add-comm, add-cancel-01, add-assoc, add-fin,
add-cancel-num-03provedall subs proved add-comm, add-cancel-01, add-assoc, add-fin,
add-cancel-num-02provedall subs proved sum-zero, add-cancel-03, add-fin, add-comm, add-assoc, add-all-zero,
add-cancel-num-01provedall subs proved add-cancel-01, add-fin, add-comm, add-assoc, eq-natinf-to-nat-2-1,
add-lessprovedall subs proved add-less-fin-01, less-inf1, add-comm, add-assoc, add-all-inf,
add-ls-cancel-01provedall subs proved ls-natinf-to-nat-2-2, less-fin, less-inf1, addeqinf-cancel, inf-less, add-comm, add-assoc, add-inf2,
sum-zeroprovedall subs proved sum-zero-fin, add-all-inf, add-comm, add-assoc, num-add,
add-cancel-01provedall subs proved eq-natinf-to-nat-2-2, addeqinf-cancel, add-inf2, add-fin, add-comm, add-assoc, add-all-zero,
sum-notinfprovedall subs proved add-comm, add-assoc, addeqinf-cancel,
add-cancel-02provedall subs proved add-all-zero, add-cancel-03, add-comm, add-assoc, add-all-inf,
sum-zero-finprovedall subs proved eq-natinf-to-nat-2-1, add-inf2, add-fin, add-all-zero, add-comm, add-assoc, num-add,
add-less-fin-01provedall subs proved ls-natinf-to-nat-1-2, less-inf2, add-inf2, less-fin, add-comm, add-assoc, add-all-zero,
add-cancel-03provedall subs proved add-all-zero, eq-natinf-to-nat-2-1, add-comm, add-assoc, add-inf2,
addeqinf-cancelprovedall subs proved add-inf2, add-comm, add-assoc, add-inf-02,
ls-succ-01provedall subs proved add-comm, add-assoc, less-fin, less-succ-leq, less-inf2, less-inf1,
ls-succprovedall subs proved add-comm, add-assoc, less-fin, less-succ-leq, less-inf2, less-inf1, add-fin,
less-notgeqinfprovedall subs proved add-comm, add-not-less, add-assoc, add-fin,
eqsucc-notlsprovedall subs proved add-comm, add-assoc, add-not-less,
eqls-ls-notlsprovedall subs proved add-comm, add-assoc, ls-le, less-succ-leq,
add-inf-01provedall subs proved add-inf2, add-inf-02, add-comm, add-assoc, add-all-inf,
num-addprovedall subs proved add-comm, add-assoc, eq-natinf-to-nat-2-2, add-fin,
add-not-lessprovedall subs proved ls-natinf-to-nat-2-1, add-inf2, less-inf1, add-comm, add-assoc, add-all-inf,
less-succ-leqprovedall subs proved less-fin, ls-natinf-to-nat-1-2, less-inf1, less-inf2, add-comm, add-assoc, add-inf2,
ls-leprovedall subs proved ls-irref, ls-trans,
add-inf-02provedall subs proved add-fin, add-comm, add-assoc, add-inf2,
add-all-zeroprovedall subs proved eq-natinf-to-nat-2-1, add-comm, add-assoc, add-inf2,
rem-seln-on-addprovedall subs proved add-comm, add-assoc, prime-add-fin,
ls-lsaddprovedall subs proved ls-natinf-to-nat-1-2, less-inf2, add-comm, add-assoc, add-inf2,
leq-notgraddprovedall subs proved ls-natinf-to-nat-2-1, less-inf1, add-comm, add-assoc, add-inf2,
lele-reflprovedall subs proved less-inf2, less-fin, inf-less, less-inf1, ls-irref, lele-trans,
inf-inseq-reduceprovedall subs proved add-comm, add-assoc, ls-natinf-to-nat-1-2,
eqsum-notlessprovedall subs proved add-comm, add-assoc, ls-natinf-to-nat-2-2,
ls-transprovedall subs proved less-fin, less-inf1, inf-less, lels-trans, lsle-trans,
lele-transprovedall subs proved lels-trans, lsle-trans,
add-assocprovedall subs proved add-fin, add-inf2, add-inf1, add-comm, add-all-inf,
ls-natinf-to-nat-3-3provedall subs proved ls-natinf-to-nat-3-2, add-fin,
eq-natinf-to-nat-3-3provedall subs proved eq-natinf-to-nat-3-2, add-fin,
ls-natinf-to-nat-3-2provedall subs proved ls-natinf-to-nat-2-2, add-fin,
lels-transprovedall subs proved lsle-trans,
eq-natinf-to-nat-3-2provedall subs proved eq-natinf-to-nat-2-2, add-fin,
add-commprovedall subs proved eq-natinf-to-nat-2-2, add-inf2, add-inf1, add-inf, add-all-inf,
ls-natinf-to-nat-2-3provedall subs proved ls-natinf-to-nat-2-2, add-fin,
lsle-transprovedall subs proved less-inf1, less-fin, inf-less,
ls-natinf-to-nat-2-2provedall subs proved ls-natinf-to-nat-2-1, add-fin,
eq-natinf-to-nat-2-2provedall subs proved eq-natinf-to-nat-2-1, add-fin,
min-inf2provedall subs proved inf-less, min-def,
ls-oneprovedall subs proved less-fin, less-inf1, zerols-neqzero,
ls-natinf-to-nat-3-1provedall subs proved ls-natinf-to-nat-2-1, add-fin,
ls-natinf-to-nat-1-3provedall subs proved ls-natinf-to-nat-1-2, add-fin,
eq-natinf-to-nat-3-1provedall subs proved eq-natinf-to-nat-2-1, add-fin,
prime-add-finprovedall subs proved add-fin,
zerols-neqzeroprovedall subs proved less-fin, less-inf2,
ls-irrefprovedall subs proved less-fin, less-inf1,
ls-natinf-to-nat-2-1provedall subs proved less-fin, add-fin,
inf-lessprovedall subs proved less-inf2, less-inf1,
ls-natinf-to-nat-1-2provedall subs proved less-fin, add-fin,
add-all-infprovedall subs proved add-inf2, add-inf,
eq-natinf-to-nat-2-1provedall subs proved add-fin,
onels-neqzeroprovedall subs proved less-fin, less-inf2,
not-less-zeroprovedall subs proved less-fin, less-inf1,
min-inf1provedall subs proved less-inf1, min-def,
min-defaxiom
less-finaxiom
less-inf2axiom
less-inf1axiom
add-inf1axiom
add-finaxiom
add-infaxiom
add-inf2axiom