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