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