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

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:
divi-primmultprovedall subs proved div, gcdnex-prime, gcd-div-one-01, divi-mult-01,
gcd-div-one-01provedall subs proved gcd-div-one,
gcd-div-one-02provedall subs proved gcd-div-one,
gcd-conq-oneprovedall subs proved dist-snd-01, Divides, gcd-mod-one-01, divi-one-01, gcd-one, dist-same, divi-zero-01, gcd-a, gcd-zero-02,
gcd-div-oneprovedall subs proved dist-mult, Divides, gcdex-dist,
gcd-mod-one-01provedall subs proved gcd-a, gcd-zero, gcd-mod-one,
gcdnex-primeprovedall subs proved divi-mult, Divides, prime-prime, gcdnex,
gcdnexprovedall subs proved divi-zero, gcd-zero-01, gcd-c, gcd-divs, gcd-zero-02, gcd-zero, gcd-alldiv, gcd-a, gcd-one, divi-one,
gcd-mod-oneprovedall subs proved gcdex,
gcdex-distprovedall subs proved dist-snd-01, dist-fst, gcdex,
gcd-twoprovedall subs proved gcd-a, gcd-zero-01, gcd-le,
gcd-maxprovedall subs proved gcd-a, gcd-zero-01, divi-ls, gcd-alldiv,
gcd-eqprovedall subs proved gcd-c, gcd-le,
gcdexprovedall subs proved gcd-c, gcdexh,
gcd-zero-01provedall subs proved gcd-c, gcd-a, gcd-zero-01-h, gcd-id, gcd-zero,
gcd-leprovedall subs proved gcd-le-both, gcd-zero-02,
gcdexhprovedall subs proved gcd-mod, gcd-a, gcd-zero-02,
gcd-zero-01-hprovedall subs proved gcd-id, gcd-c, gcd-a, gcd-zero, gcd-rec2,
gcd-le-bothprovedall subs proved gcd-c, gcd-a, gcd-id, gcd-le-both-h,
gcd-transprovedall subs proved gcd-c, divi-trans, gcd-a, gcd-divs, gcd-alldiv,
gcd-multprovedall subs proved gcd-zero-02, gcd-a, gcd-zero, gcd-rec2, gcd-rec1,
gcd-id-01provedall subs proved gcd-a, gcd-id, gcd-alldiv,
gcd-aprovedall subs proved gcd-div-03, gcd-c, gcd-div-02, gcd-alldiv, divi-eq,
gcd-div-02provedall subs proved gcd-div-03, gcd-div-04, gcd-alldiv,
gcd-div-04provedall subs proved gcd-divs,
gcd-div-03provedall subs proved gcd-divs, gcd-c, gcd-div, gcd-div-01,
gcd-multdivprovedall subs proved Divides, gcd-divs,
gcd-divsprovedall subs proved divi-ref, gcd-div,
divi-sameprovedall subs proved dist-c, divi-add-01, dist-add, divi-mult, dist-mult, dist-add-01, dist-snd, dist-fst, Divides,
prime-primeprovedall subs proved divi-mod, not-prime, mult-02, one, zero,
gcd-div-01provedall subs proved gcd-div-both,
gcd-divprovedall subs proved gcd-div-both,
dist-add-01provedall subs proved dist-c, dist-add, dist-snd, dist-fst,
dist-multprovedall subs proved dist-c, dist-mult-01, dist-snd, dist-fst,
twodivprovedall subs proved mult, Divides, two,
two-01provedall subs proved lstwo, two,
succprovedall subs proved twodiv-01, Prime, three,
prime-smallestprovedall subs proved mult-02, divi-mod, not-prime, mult-03, one, zero,
mod2provedall subs proved mult, two,
mod-zeroprovedall subs proved mult, two,
dist-zeroprovedall subs proved dist-snd-01,
twodiv-01provedall subs proved divi-two-03, Prime, divi-two,
mult-03provedall subs proved mult,
mult-02provedall subs proved mult, Prime,
not-primeprovedall subs proved divi-mult-01, divi-mult, Divides, divi-trans, divi-zero-01, divi-ls, Prime,
twoprovedall subs proved divi-two-02, Prime,
gcd-div-bothprovedall subs proved gcd-id, gcd-c, gcd-div-both-h,
gcd-alldivprovedall subs proved gcd-id, gcd-c, gcd-alldiv-h,
dist-snd-01provedall subs proved dist-add,
dist-mult-01provedall subs proved dist-add,
dist-cprovedall subs proved dist-add, dist-fst, dist-snd,
twodiv-02provedall subs proved divi-two-03, divi-three, Prime,
modprimeprovedall subs proved divi-zero-01, divi-mod, divi-mult, Prime,
divi-two-03provedall subs proved divi-two-01, divi-zero, divi-two,
divi-two-02provedall subs proved Divides, divi-ref,
threeprovedall subs proved divi-three, Prime,
divi-modprovedall subs proved Divides, divi-mult,
multprovedall subs proved divi-mult, Prime,
divi-transprovedall subs proved divi-mult, Divides,
gcd-le-both-hprovedall subs proved gcd-id, gcd-c, gcd-rec2,
gcd-div-both-hprovedall subs proved gcd-id, gcd-c, divi-zero, gcd-zero, divi-add, gcd-rec2,
divi-zero-01provedall subs proved Divides, divi-zero,
gcd-alldiv-hprovedall subs proved gcd-c, gcd-id, gcd-zero, divi-zero, divi-add, gcd-rec2,
divi-add-01provedall subs proved divi-mult, divi-add,
divi-mult-01provedall subs proved divi-mult, Divides,
divprovedall subs proved Prime, divi-ref,
dist-addprovedall subs proved dist-same, dist-snd,
mult-01provedall subs proved divi-mult, Prime,
gcd-addprovedall subs proved gcd-c, gcd-rec2,
divi-distprovedall subs proved divi-sub, divi-add, dist-snd, dist-fst,
dist-eqprovedall subs proved dist-snd, dist-fst, dist-same,
cong-equivprovedall subs proved divi-mult, Divides, dist-snd, dist-fst,
lstwoprovedall subs proved Prime,
divi-threeprovedall subs proved Divides,
zeroprovedall subs proved Prime,
oneprovedall subs proved Prime,
divi-oneprovedall subs proved Divides,
gcd-modprovedall subs proved gcd-rec1, gcd-c,
divi-lsprovedall subs proved Divides,
gcd-zero-02provedall subs proved gcd-zero, gcd-c,
gcd-oneprovedall subs proved gcd-rec1, gcd-zero,
divi-one-01provedall subs proved Divides,
gcd-idprovedall subs proved gcd-zero, gcd-rec1,
gcd-rec2provedall subs proved gcd-rec1, gcd-c,
divi-eqprovedall subs proved Divides,
divi-twoprovedall subs proved Divides,
divi-zeroprovedall subs proved Divides,
divi-two-01provedall subs proved Divides,
divi-subprovedall subs proved Divides,
divi-addprovedall subs proved Divides,
divi-refprovedall subs proved Divides,
dist-sameprovedall subs proved dist-fst,
divi-multprovedall subs proved Divides,
leoneprovedall subs proved Prime,
divi-symprovedall subs proved Divides,
divi-succprovedall subs proved Divides,
div-multaddprovedall subs proved Divides,
gcd-rec1axiom
gcd-zeroaxiom
gcd-caxiom
Primeaxiom
dist-fstaxiom
dist-sndaxiom
Dividesaxiom