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