/usr/share/acl2-2.9/books/arithmetic-2/floor-mod/floor-mod-helper.lisp /usr/share/acl2-2.9/books/arithmetic-2/floor-mod/floor-mod.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/cancel-terms-helper.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/cancel-terms-meta.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/collect-terms-meta.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/common-meta.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/expt-helper.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/expt.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/integerp-meta.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/integerp.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/mini-theories.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/non-linear.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/numerator-and-denominator.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/post.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/pre.lisp /usr/share/acl2-2.9/books/arithmetic-2/meta/top.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/basic-arithmetic-helper.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/basic-arithmetic.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/expt-helper.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/expt.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/inequalities.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/mini-theories.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/numerator-and-denominator-helper.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/numerator-and-denominator.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/prefer-times.lisp /usr/share/acl2-2.9/books/arithmetic-2/pass1/top.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/arithmetic-theory.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/basic-helper.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/basic.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/building-blocks.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/collect.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/common.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/default-hint.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/integerp-meta.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/integerp.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/mini-theories-helper.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/mini-theories.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/normalize.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/numerator-and-denominator.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/simplify-helper.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/simplify.lisp /usr/share/acl2-2.9/books/arithmetic-3/bind-free/top.lisp /usr/share/acl2-2.9/books/arithmetic-3/floor-mod/floor-mod.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/basic-arithmetic.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/expt-helper.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/expt.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/inequalities.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/mini-theories.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/non-linear.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/num-and-denom-helper.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/numerator-and-denominator.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/prefer-times.lisp /usr/share/acl2-2.9/books/arithmetic-3/pass1/top.lisp /usr/share/acl2-2.9/books/arithmetic/abs.lisp /usr/share/acl2-2.9/books/arithmetic/binomial.lisp /usr/share/acl2-2.9/books/arithmetic/equalities.acl2 /usr/share/acl2-2.9/books/arithmetic/equalities.lisp /usr/share/acl2-2.9/books/arithmetic/factorial.lisp /usr/share/acl2-2.9/books/arithmetic/idiv.lisp /usr/share/acl2-2.9/books/arithmetic/inequalities.lisp /usr/share/acl2-2.9/books/arithmetic/mod-gcd.lisp /usr/share/acl2-2.9/books/arithmetic/natp-posp.lisp /usr/share/acl2-2.9/books/arithmetic/rational-listp.lisp /usr/share/acl2-2.9/books/arithmetic/rationals.lisp /usr/share/acl2-2.9/books/arithmetic/sumlist.lisp /usr/share/acl2-2.9/books/arithmetic/top-with-meta.lisp /usr/share/acl2-2.9/books/arithmetic/top.lisp /usr/share/acl2-2.9/books/bdd/alu-proofs.lisp /usr/share/acl2-2.9/books/bdd/alu.lisp /usr/share/acl2-2.9/books/bdd/bdd-primitives.lisp /usr/share/acl2-2.9/books/bdd/benchmarks.acl2 /usr/share/acl2-2.9/books/bdd/benchmarks.lisp /usr/share/acl2-2.9/books/bdd/bit-vector-reader.lsp /usr/share/acl2-2.9/books/bdd/bool-ops.lisp /usr/share/acl2-2.9/books/bdd/cbf.lisp /usr/share/acl2-2.9/books/bdd/hamming.lisp /usr/share/acl2-2.9/books/bdd/pg-theory.lisp /usr/share/acl2-2.9/books/certify-numbers.lisp /usr/share/acl2-2.9/books/cowles/acl2-agp.acl2 /usr/share/acl2-2.9/books/cowles/acl2-agp.lisp /usr/share/acl2-2.9/books/cowles/acl2-asg.acl2 /usr/share/acl2-2.9/books/cowles/acl2-asg.lisp /usr/share/acl2-2.9/books/cowles/acl2-crg.acl2 /usr/share/acl2-2.9/books/cowles/acl2-crg.lisp /usr/share/acl2-2.9/books/data-structures/alist-defthms.lisp /usr/share/acl2-2.9/books/data-structures/alist-defuns.lisp /usr/share/acl2-2.9/books/data-structures/alist-theory.lisp /usr/share/acl2-2.9/books/data-structures/array1.lisp /usr/share/acl2-2.9/books/data-structures/defalist.acl2 /usr/share/acl2-2.9/books/data-structures/defalist.lisp /usr/share/acl2-2.9/books/data-structures/define-structures-package.lisp /usr/share/acl2-2.9/books/data-structures/define-u-package.lisp /usr/share/acl2-2.9/books/data-structures/deflist.acl2 /usr/share/acl2-2.9/books/data-structures/deflist.lisp /usr/share/acl2-2.9/books/data-structures/list-defthms.lisp /usr/share/acl2-2.9/books/data-structures/list-defuns.lisp /usr/share/acl2-2.9/books/data-structures/list-theory.lisp /usr/share/acl2-2.9/books/data-structures/number-list-defthms.lisp /usr/share/acl2-2.9/books/data-structures/number-list-defuns.lisp /usr/share/acl2-2.9/books/data-structures/number-list-theory.lisp /usr/share/acl2-2.9/books/data-structures/set-defthms.lisp /usr/share/acl2-2.9/books/data-structures/set-defuns.lisp /usr/share/acl2-2.9/books/data-structures/set-theory.lisp /usr/share/acl2-2.9/books/data-structures/structures.acl2 /usr/share/acl2-2.9/books/data-structures/structures.lisp /usr/share/acl2-2.9/books/data-structures/utilities.acl2 /usr/share/acl2-2.9/books/data-structures/utilities.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/cert.acl2 /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/fast.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/membership.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/outer.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/package.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/primitives.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/set-order.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/sets.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/sort.lisp /usr/share/acl2-2.9/books/finite-set-theory/osets-0.81/typed.lisp /usr/share/acl2-2.9/books/finite-set-theory/set-theory.acl2 /usr/share/acl2-2.9/books/finite-set-theory/set-theory.lisp /usr/share/acl2-2.9/books/finite-set-theory/total-ordering.lisp /usr/share/acl2-2.9/books/ihs/@logops.lisp /usr/share/acl2-2.9/books/ihs/ihs-definitions.lisp /usr/share/acl2-2.9/books/ihs/ihs-init.acl2 /usr/share/acl2-2.9/books/ihs/ihs-init.lisp /usr/share/acl2-2.9/books/ihs/ihs-lemmas.lisp /usr/share/acl2-2.9/books/ihs/ihs-theories.lisp /usr/share/acl2-2.9/books/ihs/logops-definitions.lisp /usr/share/acl2-2.9/books/ihs/logops-lemmas.lisp /usr/share/acl2-2.9/books/ihs/math-lemmas.lisp /usr/share/acl2-2.9/books/ihs/quotient-remainder-lemmas.lisp /usr/share/acl2-2.9/books/meta/meta-plus-equal.lisp /usr/share/acl2-2.9/books/meta/meta-plus-lessp.lisp /usr/share/acl2-2.9/books/meta/meta-times-equal.lisp /usr/share/acl2-2.9/books/meta/meta.lisp /usr/share/acl2-2.9/books/meta/pseudo-termp-lemmas.lisp /usr/share/acl2-2.9/books/meta/term-defuns.lisp /usr/share/acl2-2.9/books/meta/term-lemmas.lisp /usr/share/acl2-2.9/books/misc/computed-hint.lisp /usr/share/acl2-2.9/books/misc/csort.lisp /usr/share/acl2-2.9/books/misc/defpun.lisp /usr/share/acl2-2.9/books/misc/dft-ex.acl2 /usr/share/acl2-2.9/books/misc/dft-ex.lisp /usr/share/acl2-2.9/books/misc/dft.lisp /usr/share/acl2-2.9/books/misc/dump-events.lisp /usr/share/acl2-2.9/books/misc/expander.lisp /usr/share/acl2-2.9/books/misc/fibonacci.lisp /usr/share/acl2-2.9/books/misc/file-io.lisp /usr/share/acl2-2.9/books/misc/grcd.lisp /usr/share/acl2-2.9/books/misc/int-division.lisp /usr/share/acl2-2.9/books/misc/meta-lemmas.lisp /usr/share/acl2-2.9/books/misc/mult.lisp /usr/share/acl2-2.9/books/misc/priorities.lisp /usr/share/acl2-2.9/books/misc/problem13.lisp /usr/share/acl2-2.9/books/misc/records.lisp /usr/share/acl2-2.9/books/misc/records0.lisp /usr/share/acl2-2.9/books/misc/rtl-untranslate.lisp /usr/share/acl2-2.9/books/misc/simplify-defuns.lisp /usr/share/acl2-2.9/books/misc/sin-cos.lisp /usr/share/acl2-2.9/books/misc/symbol-btree.lisp /usr/share/acl2-2.9/books/misc/total-order.lisp /usr/share/acl2-2.9/books/ordinals/e0-ordinal.lisp /usr/share/acl2-2.9/books/ordinals/lexicographic-ordering.lisp /usr/share/acl2-2.9/books/ordinals/limits.lisp /usr/share/acl2-2.9/books/ordinals/ordinal-addition.lisp /usr/share/acl2-2.9/books/ordinals/ordinal-basic-thms.lisp /usr/share/acl2-2.9/books/ordinals/ordinal-counter-examples.lisp /usr/share/acl2-2.9/books/ordinals/ordinal-definitions.lisp /usr/share/acl2-2.9/books/ordinals/ordinal-exponentiation.lisp /usr/share/acl2-2.9/books/ordinals/ordinal-isomorphism.lisp /usr/share/acl2-2.9/books/ordinals/ordinal-multiplication.lisp /usr/share/acl2-2.9/books/ordinals/ordinal-total-order.lisp /usr/share/acl2-2.9/books/ordinals/ordinals-without-arithmetic.lisp /usr/share/acl2-2.9/books/ordinals/ordinals.lisp /usr/share/acl2-2.9/books/ordinals/proof-of-well-foundedness.acl2 /usr/share/acl2-2.9/books/ordinals/proof-of-well-foundedness.lisp /usr/share/acl2-2.9/books/ordinals/top-with-meta.lisp /usr/share/acl2-2.9/books/powerlists/algebra.acl2 /usr/share/acl2-2.9/books/powerlists/algebra.lisp /usr/share/acl2-2.9/books/powerlists/batcher-sort.acl2 /usr/share/acl2-2.9/books/powerlists/batcher-sort.lisp /usr/share/acl2-2.9/books/powerlists/bitonic-sort.acl2 /usr/share/acl2-2.9/books/powerlists/bitonic-sort.lisp /usr/share/acl2-2.9/books/powerlists/cla-adder.acl2 /usr/share/acl2-2.9/books/powerlists/cla-adder.lisp /usr/share/acl2-2.9/books/powerlists/defpkg.lisp /usr/share/acl2-2.9/books/powerlists/gray-code.acl2 /usr/share/acl2-2.9/books/powerlists/gray-code.lisp /usr/share/acl2-2.9/books/powerlists/merge-sort.acl2 /usr/share/acl2-2.9/books/powerlists/merge-sort.lisp /usr/share/acl2-2.9/books/powerlists/prefix-sum.acl2 /usr/share/acl2-2.9/books/powerlists/prefix-sum.lisp /usr/share/acl2-2.9/books/powerlists/simple.acl2 /usr/share/acl2-2.9/books/powerlists/simple.lisp /usr/share/acl2-2.9/books/powerlists/sort.acl2 /usr/share/acl2-2.9/books/powerlists/sort.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib1/basic.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib1/bits.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib1/brat.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib1/float.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib1/reps.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib1/round.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib1/top.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib3/basic.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib3/bits.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib3/brat.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib3/fadd.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib3/float.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib3/reps.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib3/round.lisp /usr/share/acl2-2.9/books/rtl/rel1/lib3/top.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/add.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/away.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/basic.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/divsqrt.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/fadd/add3.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/fadd/lop1.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/fadd/lop2.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/fadd/lop3.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/fadd/stick.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/fadd/top.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/float.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/floor.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/fp.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/logdefs.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/loglemmas.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/logxor-def.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/logxor-lemmas.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/merge.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/near.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/odd.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/proofs.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/reps.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/rewrite-theory.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/rnd.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/sticky.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/trunc.lisp /usr/share/acl2-2.9/books/rtl/rel1/support/x-2xx.lisp /usr/share/acl2-2.9/books/rtl/rel2/lib/basic.lisp /usr/share/acl2-2.9/books/rtl/rel2/lib/bits.lisp /usr/share/acl2-2.9/books/rtl/rel2/lib/brat.lisp /usr/share/acl2-2.9/books/rtl/rel2/lib/fadd.lisp /usr/share/acl2-2.9/books/rtl/rel2/lib/float.lisp /usr/share/acl2-2.9/books/rtl/rel2/lib/reps.lisp /usr/share/acl2-2.9/books/rtl/rel2/lib/round.lisp /usr/share/acl2-2.9/books/rtl/rel2/lib/top.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/add.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/add3.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/away.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/basic.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/bits-trunc.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/bits.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/drnd.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/float.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/floor.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/fp.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/irepsproofs.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/log.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/lop1.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/lop2.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/lop3.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/merge.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/merge4.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/near+.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/near.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/odd.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/rem.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/repsproofs.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/rewrite-theory.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/rnd.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/setbits.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/stick.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/sticky.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/top.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/trunc.lisp /usr/share/acl2-2.9/books/rtl/rel2/support/x-2xx.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/basic.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/bits.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/brat.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/fadd.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/float.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/reps.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/round.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/top.lisp /usr/share/acl2-2.9/books/rtl/rel3/lib/top2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/add.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/add3.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/arith.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/arith2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/ash.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/away.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/basic.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bitn-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bitn.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bits-trunc.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bits.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bits2-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bits2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bvecp-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bvecp-lemmas.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/bvecp.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/cat.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/comp1.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/complex-rationalp.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/decode.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/denominator.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/drnd.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/encode.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/even-odd.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/expo.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/expo2-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/expo2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/expt.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/expt0.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/expt2-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/expt2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/fl-expt.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/fl2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/float.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/floor.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/flooreric-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/flooreric.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/fp.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/fp2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/frac-coeff.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/ground-zero.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/induct.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/integerp.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/irepsproofs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/log.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/logand-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/logand.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/lognot.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/logs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/lop1.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/lop2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/lop3.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/merge.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/mod-expt.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/mod.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/mod2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/model-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/mulcat.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/near+.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/near.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/negative-syntaxp.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/nniq.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/numerator.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/odd.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/power2p.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/predicate.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/product.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/rationalp.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/rem.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/repsproofs.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/rewrite-theory.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/rnd.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/rom-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/rtl.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/rtlarr.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/setbitn.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/setbits.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/setbits2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/sgn.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/shft.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/stick.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/stick2.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/sticky.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/top.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/trunc.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/type.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/unary-divide.lisp /usr/share/acl2-2.9/books/rtl/rel3/support/x-2xx.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/arith.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/arith2.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/basic.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/cg.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/common-factor-defuns.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/common-factor.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/complex-rationalp.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/denominator.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/even-odd.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/even-odd2-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/even-odd2.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/expo-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/expo.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/expt-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/expt.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/extra-rules.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/fl-expt.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/fl-hacks.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/fl-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/fl.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/floor-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/floor.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/fp.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/fp2.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/ground-zero.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/hacks.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/induct.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/integerp.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/inverted-factor.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/mod-expt.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/mod-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/mod.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/negative-syntaxp.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/nniq.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/numerator.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/power2p.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/predicate.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/product-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/product.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/rationalp.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/top.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/unary-divide.lisp /usr/share/acl2-2.9/books/rtl/rel4/arithmetic/x-2xx.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/arith.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/basic.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/bits.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/brat.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/bvecp-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/bvecp-raw-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/fadd.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/float.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/reps.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/rom-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/round.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/rtl.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/rtlarr.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/simple-loop-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/simplify-model-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/top.lisp /usr/share/acl2-2.9/books/rtl/rel4/lib/util.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/add3-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/add3.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/all-ones.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/ash.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/away-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/away.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/badguys.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bias-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bias.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bitn-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bitn.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bits-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bits-trunc-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bits-trunc.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bits.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bvecp-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bvecp-lemmas.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bvecp-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/bvecp.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/cat-def.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/cat-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/cat.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/decode-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/decode.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/drnd.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/encode.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/ereps-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/ereps.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/fast-and.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/float.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/ground-zero.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/ireps.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/land-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/land.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lextra-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lextra.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lior-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lior.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lnot-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lnot.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/log-equal.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/log-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/log.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logand-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logand.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logeqv.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logior-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logior.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logior1-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logior1.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lognot.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logorc1.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/logxor.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lop1-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lop1.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lop2-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lop2.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lop3-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lop3.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lxor-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/lxor.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/merge.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/merge2.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/mod4.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/model-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/mulcat-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/mulcat.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/near+-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/near+.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/near-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/near.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/ocat.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/oddr-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/oddr.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/rewrite-theory.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/rnd.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/rom-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/rtl.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/rtlarr.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/setbitn-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/setbitn.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/setbits-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/setbits.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/sgn.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/shft.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/simple-loop-helpers.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/stick-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/stick.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/sticky-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/sticky.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/sumbits.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/top.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/trunc-proofs.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/trunc.lisp /usr/share/acl2-2.9/books/rtl/rel4/support/util.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/away.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/bias.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/bitn.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/bits-trunc.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/bits.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/bvecp.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/cat.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/clocks.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/decode.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/ereps.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/land.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/lextra.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/lior.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/lnot.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/logior1.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/lxor.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/mulcat.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/near.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/openers.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/package-defs.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/setbitn.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/setbits.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/stick.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/sumbits.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/top.lisp /usr/share/acl2-2.9/books/rtl/rel4/user/trunc.lisp /usr/share/acl2-2.9/books/textbook/chap10/ac-example.lisp /usr/share/acl2-2.9/books/textbook/chap10/adder.lisp /usr/share/acl2-2.9/books/textbook/chap10/compiler.acl2 /usr/share/acl2-2.9/books/textbook/chap10/compiler.lisp /usr/share/acl2-2.9/books/textbook/chap10/fact.lisp /usr/share/acl2-2.9/books/textbook/chap10/insertion-sort.lisp /usr/share/acl2-2.9/books/textbook/chap10/tree.lisp /usr/share/acl2-2.9/books/textbook/chap11/compress.lisp /usr/share/acl2-2.9/books/textbook/chap11/encap.lisp /usr/share/acl2-2.9/books/textbook/chap11/finite-sets.lisp /usr/share/acl2-2.9/books/textbook/chap11/how-many-soln1.lisp /usr/share/acl2-2.9/books/textbook/chap11/how-many-soln2.lisp /usr/share/acl2-2.9/books/textbook/chap11/mergesort.lisp /usr/share/acl2-2.9/books/textbook/chap11/perm-append.lisp /usr/share/acl2-2.9/books/textbook/chap11/perm.lisp /usr/share/acl2-2.9/books/textbook/chap11/qsort.lisp /usr/share/acl2-2.9/books/textbook/chap11/starters.lisp /usr/share/acl2-2.9/books/textbook/chap11/summations-book.lisp /usr/share/acl2-2.9/books/textbook/chap11/summations.lisp /usr/share/acl2-2.9/books/textbook/chap11/tautology.lisp /usr/share/acl2-2.9/books/textbook/chap11/xtr.lisp /usr/share/acl2-2.9/books/textbook/chap11/xtr2.lisp /usr/share/acl2-2.9/books/textbook/chap3/programs.lisp /usr/share/acl2-2.9/books/textbook/chap4/solutions-logic-mode.lisp /usr/share/acl2-2.9/books/textbook/chap4/solutions-program-mode.lisp /usr/share/acl2-2.9/books/textbook/chap5/solutions.lisp /usr/share/acl2-2.9/books/textbook/chap6/selected-solutions.lisp /usr/share/doc/acl2-books-source/changelog.Debian.gz /usr/share/doc/acl2-books-source/copyright