[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-eq, 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, one, prime-prime, divi-one, 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-zero-01-h, gcd-id, gcd-a, gcd-zero,
gcd-leprovedall subs proved gcd-le-both, gcd-a, gcd-zero-02,
gcd-oneprovedall subs proved gcd-addrev, gcd-a, gcd-zero,
gcdexhprovedall subs proved gcd-mod, gcd-a, gcd-zero-02,
gcd-zero-01-hprovedall subs proved gcd-id, gcd-sym-eq, gcd-a, gcd-zero, gcd-rec2,
gcd-addrevprovedall subs proved gcd-a, gcd-add, gcd-c,
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-sym-eqprovedall subs proved gcd-a, gcd-sym,
gcd-le-both-hprovedall subs proved gcd-a, gcd-id, gcd-c, gcd-rec2,
gcd-zero-02provedall subs proved gcd-a, gcd-zero, gcd-c,
gcd-addprovedall subs proved gcd-a, gcd-sym, gcd-rec2,
gcd-twicerevprovedall subs proved gcd-a, gcd-id, gcd-rec1,
gcd-twiceprovedall subs proved gcd-a, gcd-id, gcd-rec2,
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,
gcd-div-01provedall subs proved gcd-div-both,
gcd-divprovedall subs proved gcd-div-both,
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-zero-01, divi-mod, not-prime, mult-02, one, zero,
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-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, rax, three,
prime-smallestprovedall subs proved mult-02, divi-zero-01, divi-mod, not-prime, mult-03, one, zero,
modprimeprovedall subs proved divi-zero-01, divi-mod, divi-mult, Prime,
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, rax, 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,
divi-modprovedall subs proved divi-mult, divi-ls, divi-add-01,
twoprovedall subs proved divi-two-02, Prime,
gcd-div-both-hprovedall subs proved gcd-id, gcd-c, divi-zero, gcd-zero, divi-add, gcd-rec2,
gcd-alldiv-hprovedall subs proved gcd-c, gcd-id, gcd-zero, divi-zero, divi-add, gcd-rec2,
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,
divi-succprovedall subs proved divi-one-01, divi-one, divi-add-01, Divides,
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,
zeroprovedall subs proved lstwo,
multprovedall subs proved divi-mult, Prime,
oneprovedall subs proved lstwo,
divi-transprovedall subs proved divi-mult, Divides,
divi-zero-01provedall subs proved Divides, divi-zero,
dist-eqprovedall subs proved dist-snd, dist-fst, dist-same,
gcd-rec2provedall subs proved gcd-sym, gcd-rec1, gcd-c,
divi-mult-01provedall subs proved divi-mult, Divides,
divprovedall subs proved Prime, divi-ref,
divi-add-01provedall subs proved divi-mult, divi-add,
dist-addprovedall subs proved dist-same, dist-snd,
mult-01provedall subs proved divi-mult, Prime,
divi-distprovedall subs proved divi-sub, divi-add, dist-snd, dist-fst,
cong-equivprovedall subs proved divi-mult, Divides, dist-snd, dist-fst,
divi-threeprovedall subs proved Divides,
raxprovedall subs proved Prime,
lstwoprovedall subs proved Prime,
gcd-modprovedall subs proved gcd-rec1, gcd-c,
gcd-idprovedall subs proved gcd-zero, gcd-rec1,
gcd-symprovedall subs proved gcd-c,
divi-eqprovedall subs proved Divides,
divi-twoprovedall subs proved Divides,
divi-zeroprovedall subs proved Divides,
divi-two-01provedall subs proved Divides,
divi-oneprovedall subs proved Divides,
divi-one-01provedall subs proved Divides,
divi-lsprovedall 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,
div-multaddprovedall subs proved Divides,
gcd-rec1axiom
gcd-zeroaxiom
gcd-caxiom
Primeaxiom
dist-fstaxiom
dist-sndaxiom
Dividesaxiom