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