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

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-03provedall subs proved nat2int-14, num-n2i-ls-02,
nat2int-14provedall subs proved num-n2i-ls,
num-n2i-lsprovedall subs proved num-i2n-le, num-n2i-ls-02, nat2int, abs-zero, inni-le,
ls-fin-addprovedall subs proved nat2int-04, sub, i2i-pos, rax-04, n2i-add, nat2int-08, num-i2n-le-02, ls-int-ls-nat, num-n2i-ls-02, nat2int-03, abs-zero, pos-int,
zero-11provedall subs proved zero-12,
nat2int-11provedall subs proved ls-int-ls-nat,
num-i2n-leprovedall subs proved i2i-pos, nat2int-04, num-n2i-ls-02, nat2int, abs-zero, inni-le,
zero-12provedall subs proved nat2int-02, num-n2i-ls-02,
ls-int-ls-natprovedall subs proved num-n2i-ls-04, add-nonneg-int-to-nat, nat2int-08, num-n2i-ls-02,
le-int-le-natprovedall subs proved add-nonneg-int-to-nat, nat2int-08, num-n2i-ls-06,
mod-zero-02provedall subs proved num-n2i-ls-02,
mult-ls-03provedall subs proved num-n2i-ls-02,
zero-02provedall subs proved nat2int-08, num-n2i-ls-02,
mult-ls-02provedall subs proved num-n2i-ls-02,
num-i2n-lsprovedall subs proved i2i-pos-01, le, num-n2i-ls-02, inni-ls,
zero-09provedall subs proved num-n2i-ls-02,
num-n2i-ls-02provedall subs proved inni-ls, i2i-pos-01, le,
num-n2i-ls-06provedall subs proved inni-le, i2i-pos-01, nat2int-04,
inni-ls-01provedall subs proved inni-le, n2i-add, pos-add,
inni-le-01provedall subs proved inni-ls, n2i-add,
inni-leprovedall subs proved switch-le, pos-int,
inni-lsprovedall subs proved switch-ls,
n2i2provedall subs proved num-n2i-eq, n2i-add,
abs-pred-02provedall subs proved num-i2n-le-02, sub,
i2n-divtwoprovedall subs proved n2n, abs-neg, n2i-mult, n2i-add, num-i2n-eq-01, num-i2n-eq,
sub-sameprovedall subs proved nat2int-08, i2i-pos, n2i-add, num-i2n-ls-02, abs-zero,
abs-predprovedall subs proved abs-neg, Int2nat-neg, Int2nat-pos, abs-zero, num-i2n-le-02, sub,
num-i2n-ls-02provedall subs proved ini2-abs, nat2int-04,
switch-lsprovedall subs proved ini2-abs, nat2int-04,
num-n2i-ls-04provedall subs proved ini2-abs, le,
num-i2n-eqprovedall subs proved n2n, ini2-abs,
num-i2n-le-02provedall subs proved ini2-abs, le,
switch-leprovedall subs proved ini2-abs, le,
num-n2i-eqprovedall subs proved ini2-abs, n2n,
abs-succprovedall subs proved num-i2n-le-03, abs-pred-01, abs-zero, rax-04,
mone-01provedall subs proved num-i2n-eq-01,
i2i-neg-01provedall subs proved ini2-abs,
twoprovedall subs proved num-i2n-eq-01,
abs-oneprovedall subs proved num-i2n-eq-01,
num-i2n-eq-01provedall subs proved n2n, abs-neg, i2i-neg,
num-i2n-le-03provedall subs proved i2i-neg, le,
ini2-absprovedall subs proved i2i-pos-01, i2i-neg,
le-fin-addprovedall subs proved i2i-pos-01, le, pos-int, n2i-add,
num-i2n-ls-01provedall subs proved i2i-neg, nat2int-04,
num-i2n-le-01provedall subs proved i2i-neg, le,
num-i2n-ls-03provedall subs proved i2i-neg, nat2int-04,
add-n2i-numprovedall subs proved i2i-pos-01, n2i-add,
i2i-negprovedall subs proved abs-neg, i2i-pos,
leprovedall subs proved nat2int-04, n2i-add, nat2int,
i2i-pos-01provedall subs proved i2i-pos,
natprovedall subs proved abs-neg, natpos,
zero-13provedall subs proved nat2int-04,
natposprovedall subs proved labs-01, i2n, add, abs-zero,
i2i-posprovedall subs proved n2n, abs-02, abs-eq,
nat2int-04provedall subs proved nat2int-06, nat2int-03, nat2int-10,
abs-succ-01provedall subs proved labs-01, rax-04,
nat2int-09provedall subs proved n2n, nat2int, rax-04,
nat-to-int-ge-0provedall subs proved pos-add, n2i-add,
i2n-modprovedall subs proved labs-01, abs-zero, i2n-mult, add-01,
nat2int-10provedall subs proved num-n2i-ls-05, n2i-add,
abs-eqprovedall subs proved rlabs,
n2i-multprovedall subs proved n2i-add,
pos-addprovedall subs proved nat2int-08, n2i-add,
labs-01provedall subs proved rlabs,
n2nprovedall subs proved add-nonneg-int-to-nat, n2i-add,
n2i-subprovedall subs proved n2i-add,
rlabsprovedall subs proved labs,
n2i-addprovedall subs proved nat2int-03, inj,
nat2int-05provedall subs proved inj, nat2int-07, nat2int-03,
absprovedall subs proved labs,
i2n-multprovedall subs proved i2np,
i2nprovedall subs proved abs-neg, i2np,
labsprovedall subs proved abs-neg, labsp,
injprovedall subs proved nat2int-07, nat2int-03, nat2int-02,
minus-oneprovedall subs proved nat2int-02, nat2int-08,
labspprovedall subs proved rax-04, sub, Int2nat-pos, abs-zero,
nat2int-02provedall subs proved nat2int-07, nat2int-03,
i2npprovedall subs proved add-01, rax-04, rax, sub, add, Int2nat-pos,
nat2int-12provedall subs proved num-n2i-ls-01,
rax-01provedall subs proved sub,
qzero-02provedall subs proved num-n2i-ls-07,
zero-10provedall subs proved nat2int-07, nat2int,
abs-succ-02provedall subs proved sub,
abs-02provedall subs proved nat2int,
num-n2i-ls-07provedall subs proved pos-int,
nat2int-07provedall subs proved num-n2i-eq-01,
subprovedall subs proved add-01,
num-n2i-ls-01provedall subs proved pos-int,
zero-08provedall subs proved nat2int,
mult-ls-05provedall subs proved nat2int,
mult-ls-04provedall subs proved nat2int,
num-n2i-eq-01provedall subs proved nat2int-08,
num-n2i-ls-05provedall subs proved nat2int-08,
add-01provedall subs proved add,
abs-pred-01provedall subs proved rax-02, abs-neg, Int2nat-neg, abs-zero,
nat2intprovedall subs proved nat2int-08,
pos-intprovedall subs proved nat2int-08,
sub-01provedall subs proved abs-neg, add,
num-n2i-ls-03provedall subs proved nat2int-08,
qzeroprovedall subs proved nat2int-08,
nat2int-01provedall subs proved nat2int-08,
qzero-01provedall subs proved nat2int-08,
rax-02provedall subs proved abs-neg, Int2nat-pos, rax-04, Int2nat-neg,
nat2int-08provedall subs proved nat2int-06, nat2int-03,
add-nonneg-int-to-natprovedall subs proved rax-04, nat2int-03,
addprovedall subs proved rax-04, Int2nat-neg, Int2nat-pos,
two-01provedall subs proved rax-04,
succprovedall subs proved abs-succ-03,
rax-03provedall subs proved abs-neg, Int2nat-pos, Int2nat-neg,
zero-01provedall subs proved nat2int-06,
nat2int-13provedall subs proved nat2int-06,
abs-succ-03provedall subs proved rax,
nat2int-06provedall subs proved nat2int-03,
rax-04provedall subs proved rax,
abs-negprovedall subs proved abs-negp,
abs-negpprovedall subs proved Int2nat-neg,
raxprovedall subs proved Int2nat-pos,
abs-zeroprovedall subs proved Int2nat-neg, Int2nat-pos,
nat2int-03provedall subs proved Nat2int-succ,
threeprovedall subs proved Int2nat-pos,
n2i-01provedall subs proved Nat2int-succ,
moneprovedall subs proved Int2nat-neg,
abs-01provedall subs proved Int2nat-pos,
Nat2int-succaxiom
Int2nat-negaxiom
Int2nat-posaxiom