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