acl2miricl

LOGIC & THEOREM PROVING

Programs, with proofs.

An ACL2 session in your browser.

ACL2 transcript0 inputs
Start with an expression or a conjecture.Try (+ 1 2) or choose an example.

Starting ACL2…

    Ctrl / ⌘ + Enter to evaluate
    Loading assets…
    Supported math books

    Math book sources up to 2 MB (2,000,000 bytes) per file, with required shared Lisp utilities. Books needing oversized or unavailable dependencies are excluded. Sources download separately on first access. Compilation happens in your session.

    459 selected math books · 3.56 MiB source download. Full file manifest · Download source artifact

    arithmetic (16)
    • arithmetic/abs 2,229 bytes
    • arithmetic/binomial 13,197 bytes
    • arithmetic/equalities 27,182 bytes
    • arithmetic/factorial 1,195 bytes
    • arithmetic/idiv 4,854 bytes
    • arithmetic/inequalities 17,786 bytes
    • arithmetic/mod-gcd 27,838 bytes
    • arithmetic/nat-listp 3,341 bytes
    • arithmetic/natp-posp 5,550 bytes
    • arithmetic/rational-listp 1,220 bytes
    • arithmetic/rationals 8,738 bytes
    • arithmetic/real-listp 693 bytes
    • arithmetic/realp 1,163 bytes
    • arithmetic/sumlist 1,100 bytes
    • arithmetic/top-with-meta 470 bytes
    • arithmetic/top 3,412 bytes
    arithmetic-2 (26)
    • arithmetic-2/floor-mod/floor-mod-helper 17,687 bytes
    • arithmetic-2/floor-mod/floor-mod 17,298 bytes
    • arithmetic-2/meta/cancel-terms-helper 10,323 bytes
    • arithmetic-2/meta/cancel-terms-meta 18,521 bytes
    • arithmetic-2/meta/collect-terms-meta 5,630 bytes
    • arithmetic-2/meta/common-meta 25,608 bytes
    • arithmetic-2/meta/expt-helper 3,099 bytes
    • arithmetic-2/meta/expt 11,612 bytes
    • arithmetic-2/meta/integerp-meta 21,120 bytes
    • arithmetic-2/meta/integerp 3,400 bytes
    • arithmetic-2/meta/mini-theories 1,998 bytes
    • arithmetic-2/meta/non-linear 13,432 bytes
    • arithmetic-2/meta/numerator-and-denominator 2,494 bytes
    • arithmetic-2/meta/post 4,854 bytes
    • arithmetic-2/meta/pre 2,120 bytes
    • arithmetic-2/meta/top 6,201 bytes
    • arithmetic-2/pass1/basic-arithmetic-helper 3,334 bytes
    • arithmetic-2/pass1/basic-arithmetic 5,339 bytes
    • arithmetic-2/pass1/expt-helper 2,472 bytes
    • arithmetic-2/pass1/expt 5,549 bytes
    • arithmetic-2/pass1/inequalities 4,467 bytes
    • arithmetic-2/pass1/mini-theories 2,217 bytes
    • arithmetic-2/pass1/numerator-and-denominator-helper 19,523 bytes
    • arithmetic-2/pass1/numerator-and-denominator 2,892 bytes
    • arithmetic-2/pass1/prefer-times 4,498 bytes
    • arithmetic-2/pass1/top 1,097 bytes
    arithmetic-3 (35)
    • arithmetic-3/bind-free/arithmetic-theory 22,385 bytes
    • arithmetic-3/bind-free/banner 404 bytes
    • arithmetic-3/bind-free/basic-helper 5,647 bytes
    • arithmetic-3/bind-free/basic 24,117 bytes
    • arithmetic-3/bind-free/building-blocks 6,117 bytes
    • arithmetic-3/bind-free/collect 15,400 bytes
    • arithmetic-3/bind-free/common 13,411 bytes
    • arithmetic-3/bind-free/default-hint 1,970 bytes
    • arithmetic-3/bind-free/integerp-meta 25,736 bytes
    • arithmetic-3/bind-free/integerp 35,386 bytes
    • arithmetic-3/bind-free/mini-theories-helper 4,685 bytes
    • arithmetic-3/bind-free/mini-theories 4,493 bytes
    • arithmetic-3/bind-free/normalize 24,628 bytes
    • arithmetic-3/bind-free/numerator-and-denominator 2,285 bytes
    • arithmetic-3/bind-free/remove-weak-inequalities 3,284 bytes
    • arithmetic-3/bind-free/simplify-helper 10,533 bytes
    • arithmetic-3/bind-free/simplify 36,624 bytes
    • arithmetic-3/bind-free/top 13,060 bytes
    • arithmetic-3/extra/ext-compat 8,578 bytes
    • arithmetic-3/extra/ext 18,504 bytes
    • arithmetic-3/extra/top-ext 550 bytes
    • arithmetic-3/floor-mod/floor-mod 39,558 bytes
    • arithmetic-3/floor-mod/mod-expt-fast 5,804 bytes
    • arithmetic-3/pass1/basic-arithmetic-helper 3,407 bytes
    • arithmetic-3/pass1/basic-arithmetic 6,495 bytes
    • arithmetic-3/pass1/expt-helper 2,561 bytes
    • arithmetic-3/pass1/expt 5,728 bytes
    • arithmetic-3/pass1/inequalities 3,735 bytes
    • arithmetic-3/pass1/mini-theories 2,218 bytes
    • arithmetic-3/pass1/non-linear 6,390 bytes
    • arithmetic-3/pass1/num-and-denom-helper 19,613 bytes
    • arithmetic-3/pass1/numerator-and-denominator 2,917 bytes
    • arithmetic-3/pass1/prefer-times 3,345 bytes
    • arithmetic-3/pass1/top 457 bytes
    • arithmetic-3/top 275 bytes
    arithmetic-5 (56)
    • arithmetic-5/lib/basic-ops/arithmetic-theory 29,723 bytes
    • arithmetic-5/lib/basic-ops/banner 1,359 bytes
    • arithmetic-5/lib/basic-ops/basic 5,493 bytes
    • arithmetic-5/lib/basic-ops/building-blocks-helper 3,785 bytes
    • arithmetic-5/lib/basic-ops/building-blocks 44,281 bytes
    • arithmetic-5/lib/basic-ops/collect 23,554 bytes
    • arithmetic-5/lib/basic-ops/common 48,271 bytes
    • arithmetic-5/lib/basic-ops/default-hint 15,052 bytes
    • arithmetic-5/lib/basic-ops/distributivity 1,384 bytes
    • arithmetic-5/lib/basic-ops/dynamic-e-d 4,255 bytes
    • arithmetic-5/lib/basic-ops/elim-hint 22,332 bytes
    • arithmetic-5/lib/basic-ops/expt-helper 16,548 bytes
    • arithmetic-5/lib/basic-ops/expt 32,045 bytes
    • arithmetic-5/lib/basic-ops/forcing-types 3,541 bytes
    • arithmetic-5/lib/basic-ops/fuse-power-of-2 19,190 bytes
    • arithmetic-5/lib/basic-ops/if-normalization 2,533 bytes
    • arithmetic-5/lib/basic-ops/integerp-helper 4,211 bytes
    • arithmetic-5/lib/basic-ops/integerp-meta 32,653 bytes
    • arithmetic-5/lib/basic-ops/integerp 167,864 bytes
    • arithmetic-5/lib/basic-ops/mini-theories 2,352 bytes
    • arithmetic-5/lib/basic-ops/natp-posp 4,860 bytes
    • arithmetic-5/lib/basic-ops/normalize 25,252 bytes
    • arithmetic-5/lib/basic-ops/numerator-and-denominator 6,040 bytes
    • arithmetic-5/lib/basic-ops/remove-weak-inequalities 3,661 bytes
    • arithmetic-5/lib/basic-ops/simple-equalities-and-inequalities-helper 2,998 bytes
    • arithmetic-5/lib/basic-ops/simple-equalities-and-inequalities 44,536 bytes
    • arithmetic-5/lib/basic-ops/simplify-helper 14,519 bytes
    • arithmetic-5/lib/basic-ops/simplify 30,283 bytes
    • arithmetic-5/lib/basic-ops/top 14,663 bytes
    • arithmetic-5/lib/basic-ops/types-helper 1,923 bytes
    • arithmetic-5/lib/basic-ops/types 3,498 bytes
    • arithmetic-5/lib/basic-ops/we-are-here 525 bytes
    • arithmetic-5/lib/floor-mod/floor-mod-basic-helper 16,506 bytes
    • arithmetic-5/lib/floor-mod/floor-mod-basic 33,425 bytes
    • arithmetic-5/lib/floor-mod/floor-mod-helper 15,197 bytes
    • arithmetic-5/lib/floor-mod/floor-mod 69,750 bytes
    • arithmetic-5/lib/floor-mod/forcing-types 3,286 bytes
    • arithmetic-5/lib/floor-mod/if-normalization 1,635 bytes
    • arithmetic-5/lib/floor-mod/logand-helper 3,495 bytes
    • arithmetic-5/lib/floor-mod/logand 57,468 bytes
    • arithmetic-5/lib/floor-mod/mod-expt-fast 2,448 bytes
    • arithmetic-5/lib/floor-mod/more-floor-mod 26,623 bytes
    • arithmetic-5/lib/floor-mod/top 720 bytes
    • arithmetic-5/lib/floor-mod/truncate-rem 2,787 bytes
    • arithmetic-5/support/basic-arithmetic-helper 3,600 bytes
    • arithmetic-5/support/basic-arithmetic 6,533 bytes
    • arithmetic-5/support/expt-helper 2,609 bytes
    • arithmetic-5/support/expt 5,983 bytes
    • arithmetic-5/support/inequalities 3,873 bytes
    • arithmetic-5/support/mini-theories 2,256 bytes
    • arithmetic-5/support/non-linear 6,443 bytes
    • arithmetic-5/support/num-and-denom-helper 19,799 bytes
    • arithmetic-5/support/numerator-and-denominator 3,892 bytes
    • arithmetic-5/support/prefer-times 3,463 bytes
    • arithmetic-5/support/top 495 bytes
    • arithmetic-5/top 17,583 bytes
    cowles (4)
    • cowles/acl2-agp 8,795 bytes
    • cowles/acl2-asg 8,013 bytes
    • cowles/acl2-crg 8,283 bytes
    • cowles/portcullis 162 bytes
    finite-set-theory (2)
    • finite-set-theory/set-theory 103,710 bytes
    • finite-set-theory/total-ordering 8,680 bytes
    ihs (11)
    • ihs/@logops 39,103 bytes
    • ihs/basic-definitions 34,311 bytes
    • ihs/ihs-definitions 1,493 bytes
    • ihs/ihs-doc-topic 1,329 bytes
    • ihs/ihs-init 18,535 bytes
    • ihs/ihs-lemmas 2,730 bytes
    • ihs/ihs-theories 4,825 bytes
    • ihs/logops-definitions 54,035 bytes
    • ihs/logops-lemmas 81,128 bytes
    • ihs/math-lemmas 12,499 bytes
    • ihs/quotient-remainder-lemmas 76,314 bytes
    ordinals (17)
    • ordinals/e0-ordinal 12,851 bytes
    • ordinals/lexicographic-book 5,977 bytes
    • ordinals/lexicographic-ordering-without-arithmetic 211 bytes
    • ordinals/lexicographic-ordering 242 bytes
    • ordinals/limits 1,746 bytes
    • ordinals/ordinal-addition 13,112 bytes
    • ordinals/ordinal-basic-thms 10,202 bytes
    • ordinals/ordinal-counter-examples 3,725 bytes
    • ordinals/ordinal-definitions 8,996 bytes
    • ordinals/ordinal-exponentiation 30,914 bytes
    • ordinals/ordinal-isomorphism 18,411 bytes
    • ordinals/ordinal-multiplication 15,484 bytes
    • ordinals/ordinal-total-order 5,819 bytes
    • ordinals/ordinals-without-arithmetic 80 bytes
    • ordinals/ordinals 111 bytes
    • ordinals/proof-of-well-foundedness 4,487 bytes
    • ordinals/top-with-meta 154 bytes
    powerlists (9)
    • powerlists/algebra 43,818 bytes
    • powerlists/batcher-sort 35,719 bytes
    • powerlists/bitonic-sort 4,732 bytes
    • powerlists/cla-adder 12,341 bytes
    • powerlists/gray-code 8,380 bytes
    • powerlists/merge-sort 8,665 bytes
    • powerlists/prefix-sum 27,858 bytes
    • powerlists/simple 7,383 bytes
    • powerlists/sort 6,881 bytes
    kestrel/algebra (2)
    • kestrel/algebra/groups-encap-test 1,799 bytes
    • kestrel/algebra/groups-encap 2,930 bytes
    kestrel/arithmetic-light (60)
    • kestrel/arithmetic-light/abs 1,396 bytes
    • kestrel/arithmetic-light/ash 10,614 bytes
    • kestrel/arithmetic-light/cancel-addends-tests 2,185 bytes
    • kestrel/arithmetic-light/cancel-addends 4,396 bytes
    • kestrel/arithmetic-light/ceiling-of-lg-def 700 bytes
    • kestrel/arithmetic-light/ceiling-of-lg 7,511 bytes
    • kestrel/arithmetic-light/ceiling 11,477 bytes
    • kestrel/arithmetic-light/compat 926 bytes
    • kestrel/arithmetic-light/complex 579 bytes
    • kestrel/arithmetic-light/denominator 2,135 bytes
    • kestrel/arithmetic-light/divide 14,921 bytes
    • kestrel/arithmetic-light/doc 547 bytes
    • kestrel/arithmetic-light/even-and-odd 5,695 bytes
    • kestrel/arithmetic-light/evenp 1,759 bytes
    • kestrel/arithmetic-light/expt 33,792 bytes
    • kestrel/arithmetic-light/expt2 11,986 bytes
    • kestrel/arithmetic-light/fix 1,277 bytes
    • kestrel/arithmetic-light/floor-and-expt 3,530 bytes
    • kestrel/arithmetic-light/floor-mod-expt 3,470 bytes
    • kestrel/arithmetic-light/floor 54,732 bytes
    • kestrel/arithmetic-light/floor2 16,737 bytes
    • kestrel/arithmetic-light/ifix 1,365 bytes
    • kestrel/arithmetic-light/imagpart 2,788 bytes
    • kestrel/arithmetic-light/integer-length 14,088 bytes
    • kestrel/arithmetic-light/integer-length2 637 bytes
    • kestrel/arithmetic-light/integerp 4,722 bytes
    • kestrel/arithmetic-light/less-than-or-equal 638 bytes
    • kestrel/arithmetic-light/less-than 1,446 bytes
    • kestrel/arithmetic-light/lg-def 669 bytes
    • kestrel/arithmetic-light/lg 3,547 bytes
    • kestrel/arithmetic-light/limit-expt 2,150 bytes
    • kestrel/arithmetic-light/log2-def 1,426 bytes
    • kestrel/arithmetic-light/log2 12,062 bytes
    • kestrel/arithmetic-light/max 4,545 bytes
    • kestrel/arithmetic-light/min 2,834 bytes
    • kestrel/arithmetic-light/minus 2,597 bytes
    • kestrel/arithmetic-light/mod-and-expt 7,620 bytes
    • kestrel/arithmetic-light/mod-expt-fast-unguarded 1,006 bytes
    • kestrel/arithmetic-light/mod-expt-fast 1,349 bytes
    • kestrel/arithmetic-light/mod 31,087 bytes
    • kestrel/arithmetic-light/mod2 9,144 bytes
    • kestrel/arithmetic-light/natp 1,964 bytes
    • kestrel/arithmetic-light/nonnegative-integer-quotient 9,667 bytes
    • kestrel/arithmetic-light/numerator-and-denominator 4,199 bytes
    • kestrel/arithmetic-light/numerator 2,198 bytes
    • kestrel/arithmetic-light/plus-and-minus 1,053 bytes
    • kestrel/arithmetic-light/plus-and-times 519 bytes
    • kestrel/arithmetic-light/plus-times-and-divide 1,530 bytes
    • kestrel/arithmetic-light/plus 10,577 bytes
    • kestrel/arithmetic-light/power-of-2p-def 584 bytes
    • kestrel/arithmetic-light/power-of-2p 5,388 bytes
    • kestrel/arithmetic-light/realpart 2,766 bytes
    • kestrel/arithmetic-light/rem 3,796 bytes
    • kestrel/arithmetic-light/times-and-divide 4,433 bytes
    • kestrel/arithmetic-light/times 24,337 bytes
    • kestrel/arithmetic-light/top 2,151 bytes
    • kestrel/arithmetic-light/truncate 10,778 bytes
    • kestrel/arithmetic-light/types 2,574 bytes
    • kestrel/arithmetic-light/unguarded-built-ins 6,369 bytes
    • kestrel/arithmetic-light/unguarded-primitives 4,180 bytes
    kestrel/number-theory (16)
    • kestrel/number-theory/defprime-tests 3,722 bytes
    • kestrel/number-theory/defprime 12,292 bytes
    • kestrel/number-theory/divides 809 bytes
    • kestrel/number-theory/euler2-support 2,027 bytes
    • kestrel/number-theory/mod-expt-fast 1,403 bytes
    • kestrel/number-theory/mod 2,999 bytes
    • kestrel/number-theory/portcullis 353 bytes
    • kestrel/number-theory/prime-fix 804 bytes
    • kestrel/number-theory/prime 690 bytes
    • kestrel/number-theory/primep-def-doc 758 bytes
    • kestrel/number-theory/primep-def 714 bytes
    • kestrel/number-theory/primes 2,700 bytes
    • kestrel/number-theory/quadratic-residue 4,629 bytes
    • kestrel/number-theory/tonelli-shanks-proof 54,179 bytes
    • kestrel/number-theory/tonelli-shanks 24,418 bytes
    • kestrel/number-theory/top 733 bytes
    kestrel/prime-fields (35)
    • kestrel/prime-fields/add 5,680 bytes
    • kestrel/prime-fields/bind-free-common 1,766 bytes
    • kestrel/prime-fields/bind-free-rules 413 bytes
    • kestrel/prime-fields/bind-free-tests 1,515 bytes
    • kestrel/prime-fields/bitp-idioms 4,157 bytes
    • kestrel/prime-fields/bv-rules-axe 3,964 bytes
    • kestrel/prime-fields/bv-rules 57,253 bytes
    • kestrel/prime-fields/div 1,846 bytes
    • kestrel/prime-fields/doc 2,629 bytes
    • kestrel/prime-fields/equal-of-add-cancel-bind-free 4,204 bytes
    • kestrel/prime-fields/equal-of-add-cancel 3,082 bytes
    • kestrel/prime-fields/equal-of-add-move-negs-bind-free 8,968 bytes
    • kestrel/prime-fields/equal-of-add-move-negs 3,520 bytes
    • kestrel/prime-fields/equal-of-add-rules 416 bytes
    • kestrel/prime-fields/fe-listp-fast 2,465 bytes
    • kestrel/prime-fields/fe-listp 1,805 bytes
    • kestrel/prime-fields/fep-fix 887 bytes
    • kestrel/prime-fields/fep 2,664 bytes
    • kestrel/prime-fields/inv 5,377 bytes
    • kestrel/prime-fields/minus1 1,598 bytes
    • kestrel/prime-fields/mul 8,216 bytes
    • kestrel/prime-fields/neg 3,406 bytes
    • kestrel/prime-fields/portcullis 363 bytes
    • kestrel/prime-fields/pow 6,875 bytes
    • kestrel/prime-fields/prime-fields-alt 15,932 bytes
    • kestrel/prime-fields/prime-fields-rules-axe 2,891 bytes
    • kestrel/prime-fields/prime-fields-rules 32,285 bytes
    • kestrel/prime-fields/prime-fields 1,081 bytes
    • kestrel/prime-fields/printing 6,741 bytes
    • kestrel/prime-fields/rule-lists 1,290 bytes
    • kestrel/prime-fields/rules2 6,580 bytes
    • kestrel/prime-fields/sub 3,353 bytes
    • kestrel/prime-fields/support 454 bytes
    • kestrel/prime-fields/top 1,019 bytes
    • kestrel/prime-fields/unguarded-defuns 4,274 bytes
    kestrel/sets (1)
    • kestrel/sets/sets 14,204 bytes
    projects/cholesky (4)
    • projects/cholesky/mlayers 3,086 bytes
    • projects/cholesky/mout 10,210 bytes
    • projects/cholesky/msplice 6,539 bytes
    • projects/cholesky/msym 2,697 bytes
    projects/fields (8)
    • projects/fields/embeddings 59,476 bytes
    • projects/fields/extensions 121,701 bytes
    • projects/fields/galois 111,374 bytes
    • projects/fields/polynomials 26,243 bytes
    • projects/fields/support/embeddings 431,039 bytes
    • projects/fields/support/extensions 289,043 bytes
    • projects/fields/support/galois 317,560 bytes
    • projects/fields/vectors 31,869 bytes
    projects/gaussian-elim-solvers (1)
    • projects/gaussian-elim-solvers/df-solver-v9 78,293 bytes
    projects/groups (30)
    • projects/groups/abelian 29,058 bytes
    • projects/groups/actions 32,692 bytes
    • projects/groups/cauchy 15,245 bytes
    • projects/groups/groups 43,749 bytes
    • projects/groups/lists 16,389 bytes
    • projects/groups/maps 20,263 bytes
    • projects/groups/products 14,197 bytes
    • projects/groups/quotients 17,568 bytes
    • projects/groups/simple 15,058 bytes
    • projects/groups/support/a5 61,736 bytes
    • projects/groups/support/abelian 153,970 bytes
    • projects/groups/support/actions 92,558 bytes
    • projects/groups/support/alt 34,661 bytes
    • projects/groups/support/alt5 14,246 bytes
    • projects/groups/support/dihedral 3,120 bytes
    • projects/groups/support/groups 115,294 bytes
    • projects/groups/support/lists 16,676 bytes
    • projects/groups/support/maps 48,113 bytes
    • projects/groups/support/maxine/dihedral 31,308 bytes
    • projects/groups/support/perms 23,246 bytes
    • projects/groups/support/permute 27,171 bytes
    • projects/groups/support/products 69,466 bytes
    • projects/groups/support/simple 73,656 bytes
    • projects/groups/support/support/groups 137,540 bytes
    • projects/groups/support/sylow 28,146 bytes
    • projects/groups/support/sym 13,936 bytes
    • projects/groups/support/totient 21,695 bytes
    • projects/groups/support/transpositions 10,847 bytes
    • projects/groups/sylow 8,805 bytes
    • projects/groups/symmetric 27,676 bytes
    projects/linear (17)
    • projects/linear/fdet 39,813 bytes
    • projects/linear/field 13,714 bytes
    • projects/linear/fmat 18,904 bytes
    • projects/linear/rdet 41,035 bytes
    • projects/linear/reduction 45,863 bytes
    • projects/linear/ring 13,866 bytes
    • projects/linear/rmat 21,326 bytes
    • projects/linear/support/cramer 11,379 bytes
    • projects/linear/support/fdet 182,017 bytes
    • projects/linear/support/field 20,736 bytes
    • projects/linear/support/fmat 55,080 bytes
    • projects/linear/support/rdet 182,007 bytes
    • projects/linear/support/reduction 232,838 bytes
    • projects/linear/support/ring 18,784 bytes
    • projects/linear/support/rmat 55,089 bytes
    • projects/linear/support/vectors 231,073 bytes
    • projects/linear/vectors 61,030 bytes
    projects/numbers (47)
    • projects/numbers/ballot 8,979 bytes
    • projects/numbers/binomial 824 bytes
    • projects/numbers/birthday 6,544 bytes
    • projects/numbers/derangements 8,644 bytes
    • projects/numbers/div3 1,448 bytes
    • projects/numbers/divisors 13,992 bytes
    • projects/numbers/eisenstein 10,034 bytes
    • projects/numbers/euclid 16,203 bytes
    • projects/numbers/euler 10,100 bytes
    • projects/numbers/fermat 4,928 bytes
    • projects/numbers/gauss 5,111 bytes
    • projects/numbers/girard 7,106 bytes
    • projects/numbers/harmonic 2,544 bytes
    • projects/numbers/konigsberg 3,746 bytes
    • projects/numbers/mersenne 4,525 bytes
    • projects/numbers/partitions 24,345 bytes
    • projects/numbers/portcullis 356 bytes
    • projects/numbers/pratt 9,433 bytes
    • projects/numbers/subseq 8,022 bytes
    • projects/numbers/subsets 6,360 bytes
    • projects/numbers/sum4squares 11,690 bytes
    • projects/numbers/support/ballot 19,633 bytes
    • projects/numbers/support/binomial 1,204 bytes
    • projects/numbers/support/birthday 13,337 bytes
    • projects/numbers/support/crt 11,960 bytes
    • projects/numbers/support/derangements 36,870 bytes
    • projects/numbers/support/divisors 37,202 bytes
    • projects/numbers/support/eisenstein 16,048 bytes
    • projects/numbers/support/euclid 22,003 bytes
    • projects/numbers/support/euler 19,051 bytes
    • projects/numbers/support/fermat 7,967 bytes
    • projects/numbers/support/fta 11,413 bytes
    • projects/numbers/support/gauss 9,208 bytes
    • projects/numbers/support/girard 21,076 bytes
    • projects/numbers/support/mersenne 8,141 bytes
    • projects/numbers/support/partitions 59,341 bytes
    • projects/numbers/support/pratt 36,356 bytes
    • projects/numbers/support/subseq 20,916 bytes
    • projects/numbers/support/subsets 21,223 bytes
    • projects/numbers/support/sum4squares 40,769 bytes
    • projects/numbers/support/sylvester 24,407 bytes
    • projects/numbers/support/triples 13,933 bytes
    • projects/numbers/support/z2q 7,069 bytes
    • projects/numbers/sylvester 13,717 bytes
    • projects/numbers/triangular 1,490 bytes
    • projects/numbers/triples 4,415 bytes
    • projects/numbers/z2q 5,480 bytes
    projects/schroeder-bernstein (6)
    • projects/schroeder-bernstein/chains 21,864 bytes
    • projects/schroeder-bernstein/definverse 5,742 bytes
    • projects/schroeder-bernstein/portcullis 213 bytes
    • projects/schroeder-bernstein/schroeder-bernstein 2,986 bytes
    • projects/schroeder-bernstein/setup 2,051 bytes
    • projects/schroeder-bernstein/witness 6,974 bytes
    projects/set-theory (56)
    • projects/set-theory/algebra/groups 1,415 bytes
    • projects/set-theory/algebra/integer-group 1,104 bytes
    • projects/set-theory/base 87,967 bytes
    • projects/set-theory/bijection 19,396 bytes
    • projects/set-theory/cantor 2,934 bytes
    • projects/set-theory/defthmz-plus 2,559 bytes
    • projects/set-theory/doc 48,191 bytes
    • projects/set-theory/finite/base 461 bytes
    • projects/set-theory/finite/finite-bang 14,512 bytes
    • projects/set-theory/finite/finite-domain 5,950 bytes
    • projects/set-theory/finite/finite-image 752 bytes
    • projects/set-theory/finite/finite-inverse 1,994 bytes
    • projects/set-theory/finite/finite-restrict 976 bytes
    • projects/set-theory/finite/finite-union2 8,792 bytes
    • projects/set-theory/finite/top 371 bytes
    • projects/set-theory/finseqs 7,111 bytes
    • projects/set-theory/foldr 6,336 bytes
    • projects/set-theory/fun-space 3,568 bytes
    • projects/set-theory/identity 1,539 bytes
    • projects/set-theory/image-plus 610 bytes
    • projects/set-theory/induction-support 5,307 bytes
    • projects/set-theory/induction 5,526 bytes
    • projects/set-theory/injective-funp 1,374 bytes
    • projects/set-theory/intersection 4,457 bytes
    • projects/set-theory/inverse 6,033 bytes
    • projects/set-theory/iterate 1,290 bytes
    • projects/set-theory/ordinals 14,347 bytes
    • projects/set-theory/phoenix 2,822 bytes
    • projects/set-theory/portcullis 224 bytes
    • projects/set-theory/prove-acl2p 9,569 bytes
    • projects/set-theory/reals/dedekind 3,310 bytes
    • projects/set-theory/reals/negative 13,823 bytes
    • projects/set-theory/reals/sum 9,633 bytes
    • projects/set-theory/restrict 4,856 bytes
    • projects/set-theory/schroeder-bernstein-1 3,681 bytes
    • projects/set-theory/schroeder-bernstein-support 47,127 bytes
    • projects/set-theory/schroeder-bernstein 1,511 bytes
    • projects/set-theory/set-algebra 14,137 bytes
    • projects/set-theory/skolem 3,274 bytes
    • projects/set-theory/swap 4,724 bytes
    • projects/set-theory/tc 8,906 bytes
    • projects/set-theory/top 1,142 bytes
    • projects/set-theory/topology/closed-subspace-is-compact 19,581 bytes
    • projects/set-theory/topology/compact-is-normal 27,355 bytes
    • projects/set-theory/topology/compact-is-regular 32,123 bytes
    • projects/set-theory/topology/compact 597 bytes
    • projects/set-theory/topology/finite-intersection-closure 7,776 bytes
    • projects/set-theory/topology/normal 1,535 bytes
    • projects/set-theory/topology/prelims 1,250 bytes
    • projects/set-theory/topology/subspace 15,456 bytes
    • projects/set-theory/utilities/change-pkg 4,195 bytes
    • projects/set-theory/utilities/defthme 6,086 bytes
    • projects/set-theory/utilities/remove-hypz 703 bytes
    • projects/set-theory/zfns 2,926 bytes
    • projects/set-theory/zify-motivation 1,954 bytes
    • projects/set-theory/zify 24,193 bytes

    Restart for a fresh logical world, then certify, compile, and include the factorial book.

    (certify-book "books/arithmetic/factorial" 0 t)
(include-book "arithmetic/factorial" :dir :system :load-compiled-file :comp)
(factorial 10) ; 3628800

    Generated certificates and compiled files last for this worker session. Restart discards them. Books with dependencies require those books to be certified first.