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