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