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

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:
max-perm-lsprovedall subs proved max-app-ls, max-perm,
max-permprovedall subs proved max-in-not-ls, max-del1-01, max-del1, max-one, max-rec, max-empty,
max-del1provedall subs proved max-del1-01, max-one, max-rec, max-empty,
coprimes-maxprovedall subs proved count-one, count-i2j-in, filterFun-in, filterFun-base, counti2j-empty, max-def, count-i2j-max, max-empty, filterFun-max, coprimes-def,
max-del1-01provedall subs proved max-rec, max-app, max-app-ls, max-empty, max-one,
filterFun-maxprovedall subs proved max-app-ls, max-one, max-rec, filterFun-keep, filterFun-remove, filterFun-base,
max-app-lsprovedall subs proved max-app, max-empty,
primes-le-2provedall subs proved max-le-rec, primes-rec, max-one,
max-last-not-maxprovedall subs proved max-one, max-app,
max-last-maxprovedall subs proved max-one, max-app,
max-app-ls-01provedall subs proved max-app, max-empty,
max-le-recprovedall subs proved max-empty, max-one, max-rec,
max-appprovedall subs proved max-one, max-rec,
count-i2j-maxprovedall subs proved count-i2j-empty-02, max-one, count-i2j-empty-01, max-rec, count-rec,
product-min-nlzprovedall subs proved min-del-nlz, product-min-not-ls-zero,
divide-list-at-valueprovedall subs proved max-rec, max-one, min-rec, min-one,
coprimes-no-dupsprovedall subs proved filterFun-no-dups-01, coprimes-def,
min-del-nlzprovedall subs proved min-del-nlz-01, min-empty, min-rec,
max-recprovedall subs proved max-in-not-ls, max-in-01, max-def,
filterFun-no-dups-01provedall subs proved count-i2j-no-dups, filterFun-no-dups,
nodups-interval-sizeprovedall subs proved max-in-not-ls, max-in-01,
euler-phi-primeprovedall subs proved count-i2j-length, coprimes-prime, euler-phi-def,
coprimes-orderedprovedall subs proved count-i2j-ordered, filterFun-ordered, coprimes-def,
coprimes-minprovedall subs proved count-i2j-min, filterFun-min, count-i2j-in, filterFun-in, min-empty, min-in, min-def, coprimes-def,
min-del-nlz-01provedall subs proved min-one, min-rec, min-empty,
max-in-not-lsprovedall subs proved max-is-max, max-empty, max-in-01, max-def,
count-i2j-no-dupsprovedall subs proved count-empty, count-i2j-in, counti2j-empty, counti2j-rec,
coprimes-primeprovedall subs proved count-i2j-in, filterFun-all, filterFun-base, counti2j-empty, filterFun-one, filterFun-append, counti2j-rec, coprimes-def,
count-i2j-orderedprovedall subs proved count-i2j-empty-02, count-i2j-in, counti2j-empty, count-rec,
filterFun-minprovedall subs proved min-one, min-rec, filterFun-keep, filterFun-remove, filterFun-base,
count-i2j-minprovedall subs proved count-i2j-empty-02, min-one, count-i2j-empty-01, min-rec, count-rec,
sum-countfun-not-lsprovedall subs proved countFun-in, countFun-in-01, sum-in-not-ls, sum-one, sum-app, countFun-last,
sum-countFun-subprovedall subs proved countFun-base-03, sum-one, sum-app, sum-empty, countFun-base, countFun-last,
sum-constant-countFunprovedall subs proved countFun-base-02, countFun-base-03, sum-empty, countFun-base, sum-one, sum-app, countFun-last,
product-equal-01provedall subs proved product-perm-equal,
product-del1-01provedall subs proved product-del1,
min-in-nlsprovedall subs proved min-one, min-rec,
min-in-nleprovedall subs proved min-one, min-rec,
countFun-atprovedall subs proved countFun-base-03, countFun-base-02, countFun-length, countFun-last,
coprimes-oneprovedall subs proved filterFun-one, count-one, coprimes-def,
all_prime_divisors-rec-01provedall subs proved all_prime_divisors-rec-02,
sum-in-not-lsprovedall subs proved sum-not-ls-zero, sum-one, sum-app,
countFun-in-01provedall subs proved countFun-in,
product-min-not-ls-zeroprovedall subs proved min-in-not-ls, product-negative,
product-perm-equalprovedall subs proved product-del1-02, product-one, product-app, prod-empty,
product-del1provedall subs proved product-del1-02,
max-is-maxprovedall subs proved max-in-01, max-def,
count-i2j-lengthprovedall subs proved count-i2j-empty-02, count-rec,
countFun-lastprovedall subs proved countFun-base-01, countFun-one, countFun-rec, countFun-base,
min-recprovedall subs proved min-in-not-ls, min-in, min-def,
max-oneprovedall subs proved max-in-01,
count-i2j-inprovedall subs proved count-empty, counti2j-empty, counti2j-rec,
count-oneprovedall subs proved count-empty, counti2j-rec,
all_prime_divisors-rec-02provedall subs proved all_prime_divisors-in-01, all_prime_divisors-prime, all_prime_divisors-div,
sum-positiveprovedall subs proved sum-not-ls-zero,
sum-equalprovedall subs proved sum-rec-01, sum-one, sum-app,
sum-all-indices-leprovedall subs proved sum-rec-01, sum-rec, sum-empty,
product-divideprovedall subs proved product-del1-02, product-one, product-app, prod-empty,
primes-product-not-negprovedall subs proved primes-not-neg, product-negative,
primes-max-evenprovedall subs proved max-in-01, primes-def,
countFun-last-01provedall subs proved countFun-one, countFun-rec, countFun-base,
coprimes-coprimesprovedall subs proved filterFun-in, coprimes-def,
all_prime_divisors-product-delprovedall subs proved all_prime_divisors-in-01, product-prime-divides,
all_prime_divisors-orderedprovedall subs proved all_prime_divisors-last, all_prime_divisors-in, all_prime_divisors-prime, all_prime_divisors-base, all_prime_divisors-rec,
sum-not-ls-zeroprovedall subs proved sum-one, sum-app, sum-empty,
sum-rec-01provedall subs proved sum-one, sum-app,
product-del1-02provedall subs proved product-one, product-app, prod-empty,
product-negativeprovedall subs proved product-one, product-app, prod-empty,
primes-recprovedall subs proved primes-in, primes-def,
min-in-not-lsprovedall subs proved min-empty, min-in, min-def,
max-in-01provedall subs proved max-in, max-empty,
filterFun-no-dupsprovedall subs proved filterFun-not-in, filterFun-remove, filterFun-keep, filterFun-base,
countFun-oneprovedall subs proved countFun-base-01, countFun-rec,
countFun-inprovedall subs proved countFun-base-01, countFun-rec, countFun-base,
countFun-lengthprovedall subs proved countFun-base-01, countFun-rec,
count-i2j-empty-01provedall subs proved count-i2j-empty-02,
count-recprovedall subs proved count-i2j-empty-02, counti2j-empty, counti2j-rec,
count-emptyprovedall subs proved count-i2j-empty-02, counti2j-empty,
filterFun-orderedprovedall subs proved filterFun-not-in, filterFun-keep, filterFun-remove, filterFun-base,
filterFun-inprovedall subs proved filterFun-not-in, filterFun-keep, filterFun-remove, filterFun-base,
all_prime_divisors-divprovedall subs proved all_prime_divisors-in-01, all_prime_divisors-base, all_prime_divisors-prime, all_prime_divisors-rec,
product-prime-dividesprovedall subs proved product-one, product-app, prod-empty,
all_prime_divisors-inprovedall subs proved all_prime_divisors-in-01,
product-zeroprovedall subs proved product-one, product-app, prod-empty,
product-positiveprovedall subs proved product-one, product-app, prod-empty,
product-multprovedall subs proved product-app,
product-lastprovedall subs proved product-one, product-app,
countFun-multprovedall subs proved sum-empty, countFun-base-01, sum-rec, countFun-rec, countFun-base,
countFun-distprovedall subs proved sum-empty, countFun-base-01, sum-rec, countFun-rec, countFun-base,
all_prime_divisors-productprovedall subs proved product-app, prod-empty, all_prime_divisors-base, product-one, all_prime_divisors-prime, all_prime_divisors-rec,
sum-appprovedall subs proved sum-rec, sum-empty,
sum-oneprovedall subs proved sum-empty, sum-rec,
primes-inprovedall subs proved primes-def,
primes-not-negprovedall subs proved primes-def,
max-inprovedall subs proved max-def,
filterFun-not-inprovedall subs proved filterFun-keep, filterFun-remove, filterFun-base,
countFun-base-01provedall subs proved countFun-base,
countFun-base-02provedall subs proved countFun-base,
countFun-base-03provedall subs proved countFun-base,
min-oneprovedall subs proved min-def,
count-i2j-empty-02provedall subs proved counti2j-rec, counti2j-empty,
filterFun-appendprovedall subs proved filterFun-keep, filterFun-remove, filterFun-base,
filterFun-allprovedall subs proved filterFun-keep, filterFun-remove, filterFun-base,
filterFun-oneprovedall subs proved filterFun-remove, filterFun-base, filterFun-keep,
min-inprovedall subs proved min-def, min-empty,
product-oneprovedall subs proved prod-empty, prod-rec,
product-appprovedall subs proved prod-rec, prod-empty,
all_prime_divisors-lastprovedall subs proved all_prime_divisors-base, all_prime_divisors-rec,
all_prime_divisors-in-01provedall subs proved all_prime_divisors-prime, all_prime_divisors-base, all_prime_divisors-rec,
sum-all-elems-leprovedall subs proved sum-rec, sum-empty,
primes-perm-02provedall subs proved primes-def,
primes-perm-01provedall subs proved primes-def,
primes-permprovedall subs proved primes-def,
primes-oneprovedall subs proved primes-def,
map-lengthprovedall subs proved mapFun-rec, mapFun-base,
map-inprovedall subs proved mapFun-rec, mapFun-base,
map-atprovedall subs proved mapFun-rec,
coprimes-emptyprovedall subs proved filterFun-base, counti2j-empty, coprimes-def,
prod-recaxiom
primes-defaxiom
mapFun-baseaxiom
mapFun-recaxiom
filterFun-removeaxiom
filterFun-keepaxiom
euler-phi-defaxiom
countFun-recaxiom
sum-recaxiom
sum-emptyaxiom
countFun-baseaxiom
counti2j-recaxiom
min-defaxiom
min-emptyaxiom
max-emptyaxiom
max-defaxiom
counti2j-emptyaxiom
filterFun-baseaxiom
coprimes-defaxiom
prod-emptyaxiom
all_prime_divisors-recaxiom
all_prime_divisors-primeaxiom
all_prime_divisors-baseaxiom