/usr/share/acl2-3.1/books/arithmetic-2/floor-mod/floor-mod-helper.lisp /usr/share/acl2-3.1/books/arithmetic-2/floor-mod/floor-mod.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/cancel-terms-helper.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/cancel-terms-meta.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/collect-terms-meta.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/common-meta.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/expt-helper.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/expt.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/integerp-meta.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/integerp.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/mini-theories.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/non-linear.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/numerator-and-denominator.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/post.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/pre.lisp /usr/share/acl2-3.1/books/arithmetic-2/meta/top.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/basic-arithmetic-helper.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/basic-arithmetic.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/expt-helper.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/expt.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/inequalities.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/mini-theories.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/numerator-and-denominator-helper.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/numerator-and-denominator.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/prefer-times.lisp /usr/share/acl2-3.1/books/arithmetic-2/pass1/top.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/arithmetic-theory.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/banner.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/basic-helper.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/basic.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/building-blocks.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/collect.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/common.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/default-hint.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/integerp-meta.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/integerp.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/mini-theories-helper.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/mini-theories.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/normalize.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/numerator-and-denominator.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/simplify-helper.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/simplify.lisp /usr/share/acl2-3.1/books/arithmetic-3/bind-free/top.lisp /usr/share/acl2-3.1/books/arithmetic-3/extra/ext.lisp /usr/share/acl2-3.1/books/arithmetic-3/extra/top-ext.lisp /usr/share/acl2-3.1/books/arithmetic-3/floor-mod/floor-mod.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/basic-arithmetic.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/expt-helper.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/expt.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/inequalities.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/mini-theories.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/non-linear.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/num-and-denom-helper.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/numerator-and-denominator.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/prefer-times.lisp /usr/share/acl2-3.1/books/arithmetic-3/pass1/top.lisp /usr/share/acl2-3.1/books/arithmetic/abs.lisp /usr/share/acl2-3.1/books/arithmetic/binomial.lisp /usr/share/acl2-3.1/books/arithmetic/equalities.acl2 /usr/share/acl2-3.1/books/arithmetic/equalities.lisp /usr/share/acl2-3.1/books/arithmetic/factorial.lisp /usr/share/acl2-3.1/books/arithmetic/idiv.lisp /usr/share/acl2-3.1/books/arithmetic/inequalities.lisp /usr/share/acl2-3.1/books/arithmetic/mod-gcd.lisp /usr/share/acl2-3.1/books/arithmetic/natp-posp.lisp /usr/share/acl2-3.1/books/arithmetic/rational-listp.lisp /usr/share/acl2-3.1/books/arithmetic/rationals.lisp /usr/share/acl2-3.1/books/arithmetic/sumlist.lisp /usr/share/acl2-3.1/books/arithmetic/top-with-meta.lisp /usr/share/acl2-3.1/books/arithmetic/top.lisp /usr/share/acl2-3.1/books/bdd/alu-proofs.lisp /usr/share/acl2-3.1/books/bdd/alu.lisp /usr/share/acl2-3.1/books/bdd/bdd-primitives.lisp /usr/share/acl2-3.1/books/bdd/benchmarks.acl2 /usr/share/acl2-3.1/books/bdd/benchmarks.lisp /usr/share/acl2-3.1/books/bdd/bit-vector-reader.lsp /usr/share/acl2-3.1/books/bdd/bool-ops.lisp /usr/share/acl2-3.1/books/bdd/cbf.lisp /usr/share/acl2-3.1/books/bdd/hamming.lisp /usr/share/acl2-3.1/books/bdd/pg-theory.lisp /usr/share/acl2-3.1/books/certify-numbers.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/apply-total-order.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/fairenv.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/final-theorems.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/initial-state.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/inv-persists.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/inv-sufficient.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/labels.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/lexicographic-pos.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/lexicographic.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/measures.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/pos-temp.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/programs.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/properties-of-sets.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/properties.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/records.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/stutter1-match.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/stutter2.lisp /usr/share/acl2-3.1/books/concurrent-programs/bakery/variables.lisp /usr/share/acl2-3.1/books/concurrent-programs/german-protocol/german.lisp /usr/share/acl2-3.1/books/cowles/acl2-agp.acl2 /usr/share/acl2-3.1/books/cowles/acl2-agp.lisp /usr/share/acl2-3.1/books/cowles/acl2-asg.acl2 /usr/share/acl2-3.1/books/cowles/acl2-asg.lisp /usr/share/acl2-3.1/books/cowles/acl2-crg.acl2 /usr/share/acl2-3.1/books/cowles/acl2-crg.lisp /usr/share/acl2-3.1/books/data-structures/alist-defthms.lisp /usr/share/acl2-3.1/books/data-structures/alist-defuns.lisp /usr/share/acl2-3.1/books/data-structures/alist-theory.lisp /usr/share/acl2-3.1/books/data-structures/array1.lisp /usr/share/acl2-3.1/books/data-structures/defalist.acl2 /usr/share/acl2-3.1/books/data-structures/defalist.lisp /usr/share/acl2-3.1/books/data-structures/define-structures-package.lisp /usr/share/acl2-3.1/books/data-structures/define-u-package.lisp /usr/share/acl2-3.1/books/data-structures/deflist.acl2 /usr/share/acl2-3.1/books/data-structures/deflist.lisp /usr/share/acl2-3.1/books/data-structures/list-defthms.lisp /usr/share/acl2-3.1/books/data-structures/list-defuns.lisp /usr/share/acl2-3.1/books/data-structures/list-theory.lisp /usr/share/acl2-3.1/books/data-structures/memories/cert.acl2 /usr/share/acl2-3.1/books/data-structures/memories/log2.lisp /usr/share/acl2-3.1/books/data-structures/memories/memory-impl.lisp /usr/share/acl2-3.1/books/data-structures/memories/memory.lisp /usr/share/acl2-3.1/books/data-structures/memories/memtree.lisp /usr/share/acl2-3.1/books/data-structures/memories/private.lisp /usr/share/acl2-3.1/books/data-structures/memories/timetest.lisp /usr/share/acl2-3.1/books/data-structures/number-list-defthms.lisp /usr/share/acl2-3.1/books/data-structures/number-list-defuns.lisp /usr/share/acl2-3.1/books/data-structures/number-list-theory.lisp /usr/share/acl2-3.1/books/data-structures/set-defthms.lisp /usr/share/acl2-3.1/books/data-structures/set-defuns.lisp /usr/share/acl2-3.1/books/data-structures/set-theory.lisp /usr/share/acl2-3.1/books/data-structures/structures.acl2 /usr/share/acl2-3.1/books/data-structures/structures.lisp /usr/share/acl2-3.1/books/data-structures/utilities.acl2 /usr/share/acl2-3.1/books/data-structures/utilities.lisp /usr/share/acl2-3.1/books/deduction/passmore/bewijs.lisp /usr/share/acl2-3.1/books/deduction/passmore/general.lisp /usr/share/acl2-3.1/books/deduction/passmore/paramod.lisp /usr/share/acl2-3.1/books/deduction/passmore/prover.lisp /usr/share/acl2-3.1/books/deduction/passmore/resolution.lisp /usr/share/acl2-3.1/books/deduction/passmore/unification.lisp /usr/share/acl2-3.1/books/deduction/passmore/weighting.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/basic.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/dag-unification-l.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/dag-unification-rules.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/dag-unification-st.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/dags.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/list-unification-rules.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/matching.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/subsumption-subst.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/subsumption.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/terms-as-dag.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/terms-dag-stobj.lisp /usr/share/acl2-3.1/books/defexec/dag-unification/terms.lisp /usr/share/acl2-3.1/books/defexec/defpun-exec/defpun-exec.lisp /usr/share/acl2-3.1/books/defexec/find-path/fpst.lisp /usr/share/acl2-3.1/books/defexec/find-path/graph/find-path1.lisp /usr/share/acl2-3.1/books/defexec/find-path/graph/find-path2.lisp /usr/share/acl2-3.1/books/defexec/find-path/graph/find-path3.lisp /usr/share/acl2-3.1/books/defexec/find-path/graph/helpers.lisp /usr/share/acl2-3.1/books/defexec/find-path/graph/linear-find-path.lisp /usr/share/acl2-3.1/books/defexec/find-path/graph/solutions.lisp /usr/share/acl2-3.1/books/defexec/find-path/run-fpst.lisp /usr/share/acl2-3.1/books/defexec/ordinals/supporting-ordinals.lisp /usr/share/acl2-3.1/books/defexec/other-apps/misc/memos.lisp /usr/share/acl2-3.1/books/defexec/other-apps/misc/stobjsim.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/extraction.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/final-theorem.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/first-last.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/intermediate-program.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/intermediate-to-spec.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/load-extract.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/merge-intermediate.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/nth-update-nth.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/permutations.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/programs.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/sort-qs-properties.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/spec-properties.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/split-qs-properties.lisp /usr/share/acl2-3.1/books/defexec/other-apps/qsort/total-order.lisp /usr/share/acl2-3.1/books/defexec/other-apps/records/inline.lisp /usr/share/acl2-3.1/books/defexec/other-apps/records/records.lisp /usr/share/acl2-3.1/books/defexec/other-apps/records/recordsim.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/cert.acl2 /usr/share/acl2-3.1/books/finite-set-theory/osets/computed-hints.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/fast.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/instance.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/map.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/membership.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/outer.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/primitives.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/quantify.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/set-order.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/sets.lisp /usr/share/acl2-3.1/books/finite-set-theory/osets/sort.lisp /usr/share/acl2-3.1/books/finite-set-theory/set-theory.acl2 /usr/share/acl2-3.1/books/finite-set-theory/set-theory.lisp /usr/share/acl2-3.1/books/finite-set-theory/total-ordering.lisp /usr/share/acl2-3.1/books/ihs/@logops.lisp /usr/share/acl2-3.1/books/ihs/ihs-definitions.lisp /usr/share/acl2-3.1/books/ihs/ihs-init.acl2 /usr/share/acl2-3.1/books/ihs/ihs-init.lisp /usr/share/acl2-3.1/books/ihs/ihs-lemmas.lisp /usr/share/acl2-3.1/books/ihs/ihs-theories.lisp /usr/share/acl2-3.1/books/ihs/logops-definitions.lisp /usr/share/acl2-3.1/books/ihs/logops-lemmas.lisp /usr/share/acl2-3.1/books/ihs/math-lemmas.lisp /usr/share/acl2-3.1/books/ihs/quotient-remainder-lemmas.lisp /usr/share/acl2-3.1/books/make-event/assert-check-include-1.acl2 /usr/share/acl2-3.1/books/make-event/assert-check-include-1.lisp /usr/share/acl2-3.1/books/make-event/assert-check-include.lisp /usr/share/acl2-3.1/books/make-event/assert-check.lisp /usr/share/acl2-3.1/books/make-event/assert-include.acl2 /usr/share/acl2-3.1/books/make-event/assert-include.lisp /usr/share/acl2-3.1/books/make-event/assert.lisp /usr/share/acl2-3.1/books/make-event/basic-check.lisp /usr/share/acl2-3.1/books/make-event/basic-pkg-check.acl2 /usr/share/acl2-3.1/books/make-event/basic-pkg-check.lisp /usr/share/acl2-3.1/books/make-event/basic-pkg.acl2 /usr/share/acl2-3.1/books/make-event/basic-pkg.lisp /usr/share/acl2-3.1/books/make-event/basic.lisp /usr/share/acl2-3.1/books/make-event/defconst-fast-examples.lisp /usr/share/acl2-3.1/books/make-event/defconst-fast.lisp /usr/share/acl2-3.1/books/make-event/dotimes.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms.acl2 /usr/share/acl2-3.1/books/make-event/embedded-defaxioms.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/bar.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/baruser.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-a1.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-a21.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-b1.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-b2.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-b3.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-c1.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-c2.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-d.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-e.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/foo-f.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/local-defaxiom-1.lisp /usr/share/acl2-3.1/books/make-event/embedded-defaxioms/local-defaxiom-2.lisp /usr/share/acl2-3.1/books/make-event/eval-check-tests.lisp /usr/share/acl2-3.1/books/make-event/eval-check.lisp /usr/share/acl2-3.1/books/make-event/eval-tests.lisp /usr/share/acl2-3.1/books/make-event/eval.lisp /usr/share/acl2-3.1/books/make-event/gen-defthm-check.lisp /usr/share/acl2-3.1/books/make-event/gen-defthm.lisp /usr/share/acl2-3.1/books/make-event/gen-defun-check.lisp /usr/share/acl2-3.1/books/make-event/gen-defun.lisp /usr/share/acl2-3.1/books/make-event/local-requires-skip-check-include.lisp /usr/share/acl2-3.1/books/make-event/local-requires-skip-check.lisp /usr/share/acl2-3.1/books/make-event/logical-tangent.lisp /usr/share/acl2-3.1/books/make-event/macros-include.lisp /usr/share/acl2-3.1/books/make-event/macros-skip-proofs-include.acl2 /usr/share/acl2-3.1/books/make-event/macros-skip-proofs-include.lisp /usr/share/acl2-3.1/books/make-event/macros-skip-proofs.acl2 /usr/share/acl2-3.1/books/make-event/macros-skip-proofs.lisp /usr/share/acl2-3.1/books/make-event/macros.lisp /usr/share/acl2-3.1/books/make-event/nested-check.lisp /usr/share/acl2-3.1/books/make-event/nested.lisp /usr/share/acl2-3.1/books/make-event/portcullis-expansion-include.acl2 /usr/share/acl2-3.1/books/make-event/portcullis-expansion-include.lisp /usr/share/acl2-3.1/books/make-event/portcullis-expansion.acl2 /usr/share/acl2-3.1/books/make-event/portcullis-expansion.lisp /usr/share/acl2-3.1/books/make-event/proof-by-arith.lisp /usr/share/acl2-3.1/books/make-event/read-from-file.lisp /usr/share/acl2-3.1/books/make-event/stobj-test.lisp /usr/share/acl2-3.1/books/make-event/test-case-check.lisp /usr/share/acl2-3.1/books/make-event/test-case.lisp /usr/share/acl2-3.1/books/meta/meta-plus-equal.lisp /usr/share/acl2-3.1/books/meta/meta-plus-lessp.lisp /usr/share/acl2-3.1/books/meta/meta-times-equal.lisp /usr/share/acl2-3.1/books/meta/meta.lisp /usr/share/acl2-3.1/books/meta/pseudo-termp-lemmas.lisp /usr/share/acl2-3.1/books/meta/term-defuns.lisp /usr/share/acl2-3.1/books/meta/term-lemmas.lisp /usr/share/acl2-3.1/books/misc/bash.lisp /usr/share/acl2-3.1/books/misc/computed-hint.lisp /usr/share/acl2-3.1/books/misc/csort.lisp /usr/share/acl2-3.1/books/misc/defmac.lisp /usr/share/acl2-3.1/books/misc/defpun.lisp /usr/share/acl2-3.1/books/misc/dft-ex.acl2 /usr/share/acl2-3.1/books/misc/dft-ex.lisp /usr/share/acl2-3.1/books/misc/dft.lisp /usr/share/acl2-3.1/books/misc/dump-events.lisp /usr/share/acl2-3.1/books/misc/expander.lisp /usr/share/acl2-3.1/books/misc/fibonacci.lisp /usr/share/acl2-3.1/books/misc/file-io.lisp /usr/share/acl2-3.1/books/misc/find-lemmas.lisp /usr/share/acl2-3.1/books/misc/grcd.lisp /usr/share/acl2-3.1/books/misc/hacker.lisp /usr/share/acl2-3.1/books/misc/hanoi.acl2 /usr/share/acl2-3.1/books/misc/hanoi.lisp /usr/share/acl2-3.1/books/misc/how-to-prove-thms.lisp /usr/share/acl2-3.1/books/misc/int-division.lisp /usr/share/acl2-3.1/books/misc/meta-lemmas.lisp /usr/share/acl2-3.1/books/misc/mult.lisp /usr/share/acl2-3.1/books/misc/priorities.lisp /usr/share/acl2-3.1/books/misc/problem13.lisp /usr/share/acl2-3.1/books/misc/process-book-readme.lisp /usr/share/acl2-3.1/books/misc/radix.acl2 /usr/share/acl2-3.1/books/misc/radix.lisp /usr/share/acl2-3.1/books/misc/records.lisp /usr/share/acl2-3.1/books/misc/records0.lisp /usr/share/acl2-3.1/books/misc/rtl-untranslate.lisp /usr/share/acl2-3.1/books/misc/simplify-defuns.lisp /usr/share/acl2-3.1/books/misc/sin-cos.lisp /usr/share/acl2-3.1/books/misc/sort-symbols.lisp /usr/share/acl2-3.1/books/misc/sticky-disable.lisp /usr/share/acl2-3.1/books/misc/symbol-btree.lisp /usr/share/acl2-3.1/books/misc/total-order.lisp /usr/share/acl2-3.1/books/misc/transfinite.lisp /usr/share/acl2-3.1/books/misc/untranslate-patterns.lisp /usr/share/acl2-3.1/books/ordinals/e0-ordinal.lisp /usr/share/acl2-3.1/books/ordinals/lexicographic-ordering.lisp /usr/share/acl2-3.1/books/ordinals/limits.lisp /usr/share/acl2-3.1/books/ordinals/ordinal-addition.lisp /usr/share/acl2-3.1/books/ordinals/ordinal-basic-thms.lisp /usr/share/acl2-3.1/books/ordinals/ordinal-counter-examples.lisp /usr/share/acl2-3.1/books/ordinals/ordinal-definitions.lisp /usr/share/acl2-3.1/books/ordinals/ordinal-exponentiation.lisp /usr/share/acl2-3.1/books/ordinals/ordinal-isomorphism.lisp /usr/share/acl2-3.1/books/ordinals/ordinal-multiplication.lisp /usr/share/acl2-3.1/books/ordinals/ordinal-total-order.lisp /usr/share/acl2-3.1/books/ordinals/ordinals-without-arithmetic.lisp /usr/share/acl2-3.1/books/ordinals/ordinals.lisp /usr/share/acl2-3.1/books/ordinals/proof-of-well-foundedness.acl2 /usr/share/acl2-3.1/books/ordinals/proof-of-well-foundedness.lisp /usr/share/acl2-3.1/books/ordinals/top-with-meta.lisp /usr/share/acl2-3.1/books/powerlists/algebra.acl2 /usr/share/acl2-3.1/books/powerlists/algebra.lisp /usr/share/acl2-3.1/books/powerlists/batcher-sort.acl2 /usr/share/acl2-3.1/books/powerlists/batcher-sort.lisp /usr/share/acl2-3.1/books/powerlists/bitonic-sort.acl2 /usr/share/acl2-3.1/books/powerlists/bitonic-sort.lisp /usr/share/acl2-3.1/books/powerlists/cla-adder.acl2 /usr/share/acl2-3.1/books/powerlists/cla-adder.lisp /usr/share/acl2-3.1/books/powerlists/defpkg.lisp /usr/share/acl2-3.1/books/powerlists/gray-code.acl2 /usr/share/acl2-3.1/books/powerlists/gray-code.lisp /usr/share/acl2-3.1/books/powerlists/merge-sort.acl2 /usr/share/acl2-3.1/books/powerlists/merge-sort.lisp /usr/share/acl2-3.1/books/powerlists/prefix-sum.acl2 /usr/share/acl2-3.1/books/powerlists/prefix-sum.lisp /usr/share/acl2-3.1/books/powerlists/simple.acl2 /usr/share/acl2-3.1/books/powerlists/simple.lisp /usr/share/acl2-3.1/books/powerlists/sort.acl2 /usr/share/acl2-3.1/books/powerlists/sort.lisp /usr/share/acl2-3.1/books/proofstyles/c2i/c2i-partial.lisp /usr/share/acl2-3.1/books/proofstyles/c2i/c2i-total.lisp /usr/share/acl2-3.1/books/proofstyles/c2i/clock-to-inv.lisp /usr/share/acl2-3.1/books/proofstyles/compose/compose-c-c-partial.lisp /usr/share/acl2-3.1/books/proofstyles/compose/compose-c-c-total.lisp /usr/share/acl2-3.1/books/proofstyles/i2c/i2c-partial.lisp /usr/share/acl2-3.1/books/proofstyles/i2c/i2c-total.lisp /usr/share/acl2-3.1/books/proofstyles/i2c/inv-to-clock.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib1/basic.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib1/bits.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib1/brat.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib1/float.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib1/reps.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib1/round.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib1/top.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib3/basic.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib3/bits.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib3/brat.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib3/fadd.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib3/float.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib3/reps.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib3/round.lisp /usr/share/acl2-3.1/books/rtl/rel1/lib3/top.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/add.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/away.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/basic.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/divsqrt.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/fadd/add3.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/fadd/lop1.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/fadd/lop2.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/fadd/lop3.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/fadd/stick.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/fadd/top.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/float.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/floor.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/fp.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/logdefs.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/loglemmas.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/logxor-def.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/logxor-lemmas.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/merge.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/near.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/odd.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/proofs.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/reps.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/rewrite-theory.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/rnd.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/sticky.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/trunc.lisp /usr/share/acl2-3.1/books/rtl/rel1/support/x-2xx.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/arith.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/arith2.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/basic.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/cg.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/common-factor-defuns.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/common-factor.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/complex-rationalp.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/denominator.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/even-odd.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/even-odd2-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/even-odd2.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/expo-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/expo.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/expt-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/expt.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/extra-rules.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/fl-expt.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/fl-hacks.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/fl-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/fl.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/floor-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/floor.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/fp.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/fp2.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/ground-zero.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/hacks.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/induct.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/integerp.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/inverted-factor.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/mod-expt.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/mod-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/mod.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/negative-syntaxp.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/nniq.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/numerator.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/power2p.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/predicate.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/product-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/product.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/rationalp.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/top.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/unary-divide.lisp /usr/share/acl2-3.1/books/rtl/rel4/arithmetic/x-2xx.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/arith.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/basic.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/bits.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/bvecp-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/bvecp-raw-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/clocks.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/fadd.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/float.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/openers.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/package-defs.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/reps.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/rom-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/round.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/rtl.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/rtlarr.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/simple-loop-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/simplify-model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/top.lisp /usr/share/acl2-3.1/books/rtl/rel4/lib/util.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/add3-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/add3.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/all-ones.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/ash.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/away-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/away.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/badguys.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bias-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bias.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bitn-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bitn.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bits-extra.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bits-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bits-trunc-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bits-trunc.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bits.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bvecp-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bvecp-lemmas.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bvecp-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/bvecp.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/cat-def.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/cat-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/cat.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/clocks.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/decode-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/decode.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/drnd.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/encode.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/ereps-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/ereps.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/fadd.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/fast-and.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/float.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/ground-zero.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/guards.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/ireps.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/land-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/land.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lextra-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lextra.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lior-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lior.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lnot-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lnot.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/log-equal.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/log-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/log.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logand-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logand.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logeqv.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logior-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logior.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logior1-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logior1.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lognot.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logorc1.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/logxor.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lop1-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lop1.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lop2-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lop2.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lop3-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lop3.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lxor-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/lxor.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/merge.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/merge2.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/mod4.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/mulcat-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/mulcat.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/near+-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/near+.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/near-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/near.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/ocat.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/oddr-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/oddr.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/openers.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/package-defs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/rewrite-theory.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/rnd.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/rom-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/rtl.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/rtlarr.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/setbitn-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/setbitn.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/setbits-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/setbits.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/sgn.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/shft.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/simple-loop-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/simplify-model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/stick-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/stick.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/sticky-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/sticky.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/sumbits.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/top.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/top1.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/trunc-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/trunc.lisp /usr/share/acl2-3.1/books/rtl/rel4/support/util.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/away.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/bias.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/bitn.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/bits-trunc.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/bits.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/brat.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/bvecp.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/cat.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/decode.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/ereps.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/land.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/lextra.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/lior.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/lnot.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/logior1.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/lxor.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/mulcat.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/near.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/setbitn.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/setbits.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/stick.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/sumbits.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/top.lisp /usr/share/acl2-3.1/books/rtl/rel4/user/trunc.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/arith.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/arith2.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/basic.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/cg.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/common-factor-defuns.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/common-factor.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/complex-rationalp.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/denominator.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/even-odd.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/even-odd2-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/even-odd2.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/expo-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/expo.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/expt-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/expt.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/extra-rules.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/fl-expt.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/fl-hacks.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/fl-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/fl.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/floor-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/floor.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/fp.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/fp2.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/ground-zero.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/hacks.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/induct.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/integerp.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/inverted-factor.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/mod-expt.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/mod-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/mod.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/negative-syntaxp.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/nniq.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/numerator.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/power2p.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/predicate.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/product-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/product.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/rationalp.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/top.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/unary-divide.lisp /usr/share/acl2-3.1/books/rtl/rel5/arithmetic/x-2xx.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/add.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/arith.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/basic.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/bits.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/bvecp-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/bvecp-raw-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/clocks.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/float.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/log.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/openers.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/package-defs.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/reps.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/rom-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/round.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/rtl.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/rtlarr.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/simple-loop-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/simplify-model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/top.lisp /usr/share/acl2-3.1/books/rtl/rel5/lib/util.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/add3-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/add3.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/all-ones.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/ash.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/away-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/away.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/badguys.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bias-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bias.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bitn-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bitn.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bits-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bits-trunc-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bits-trunc.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bits.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bvecp-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bvecp-lemmas.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bvecp-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/bvecp.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/cat-def.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/cat-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/cat.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/clocks.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/decode-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/decode.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/drnd.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/encode.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/ereps-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/ereps.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/fadd-extra.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/fadd-extra0.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/fadd.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/fast-and.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/float-extra.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/float.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/ground-zero.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/guards.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/ireps.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/land.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/land0-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/land0.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lextra-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lextra.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lextra0.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lior.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lior0-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lior0.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lnot-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lnot.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/log-equal.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/log-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/log.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logand-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logand.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logeqv.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logior-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logior.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logior1-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logior1.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lognot.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logorc1.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/logxor.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lop1-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lop1.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lop2-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lop2.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lop3-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lop3.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lxor.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lxor0-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/lxor0.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/merge.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/merge2.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/mod4.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/mulcat-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/mulcat.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/near+-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/near+.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/near-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/near.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/ocat.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/oddr-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/oddr.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/openers.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/package-defs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/rewrite-theory.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/rnd.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/rom-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/round-extra.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/rtl.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/rtlarr.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/setbitn-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/setbitn.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/setbits-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/setbits.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/sgn.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/shft.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/simple-loop-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/simplify-model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/stick-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/stick.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/sticky-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/sticky.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/sumbits.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/top.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/top1.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/trunc-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/trunc.lisp /usr/share/acl2-3.1/books/rtl/rel5/support/util.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/away.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/bias.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/bitn.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/bits-trunc.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/bits.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/brat.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/bvecp.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/cat.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/decode.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/ereps.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/land.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/lextra.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/lior.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/lnot.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/logior1.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/lxor.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/mulcat.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/near.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/setbitn.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/setbits.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/stick.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/sumbits.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/top.lisp /usr/share/acl2-3.1/books/rtl/rel5/user/trunc.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/arith.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/arith2.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/basic.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/cg.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/common-factor-defuns.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/common-factor.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/complex-rationalp.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/denominator.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/even-odd.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/even-odd2-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/even-odd2.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/expo-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/expo.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/expt-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/expt.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/extra-rules.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/fl-expt.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/fl-hacks.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/fl-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/fl.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/floor-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/floor.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/fp.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/fp2.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/ground-zero.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/hacks.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/induct.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/integerp.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/inverted-factor.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/mod-expt.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/mod-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/mod.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/negative-syntaxp.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/nniq.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/numerator.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/power2p.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/predicate.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/product-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/product.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/rationalp.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/top.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/unary-divide.lisp /usr/share/acl2-3.1/books/rtl/rel6/arithmetic/x-2xx.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/add.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/arith.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/basic.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/bits.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/bvecp-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/bvecp-raw-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/clocks.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/float.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/log.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/mult.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/openers.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/package-defs.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/reps.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/rom-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/round.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/rtl.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/rtlarr.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/simple-loop-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/simplify-model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/top.lisp /usr/share/acl2-3.1/books/rtl/rel6/lib/util.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1.delta1/float-extra2.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1.delta1/float.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1.delta1/mult-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1.delta1/mult.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1.delta1/round-extra2.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1.delta1/round.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/add.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/arith.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/basic.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/bits.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/bvecp-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/bvecp-raw-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/clocks.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/float.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/log.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/mult.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/openers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/package-defs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/reps.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/rom-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/round.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/rtl.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/rtlarr.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/simple-loop-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/simplify-model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/top.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/lib1/util.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/add3-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/add3.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/all-ones.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/arith-support-mult.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/ash.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/away-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/away.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/badguys.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bias-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bias.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bitn-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bitn.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bits-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bits-trunc-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bits-trunc.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bits.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bvecp-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bvecp-lemmas.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bvecp-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/bvecp.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/cat-def.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/cat-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/cat.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/clocks.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/decode-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/decode.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/drnd-original.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/drnd.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/encode.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/ereps-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/ereps.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/fadd-extra.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/fadd-extra0.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/fadd.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/fast-and.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/float-extra.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/float.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/ground-zero.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/guards.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/ireps.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/land.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/land0-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/land0.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lextra-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lextra.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lextra0.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lior.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lior0-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lior0.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lnot-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lnot.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/log-equal.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/log-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/log.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logand-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logand.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logeqv.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logior-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logior.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logior1-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logior1.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lognot.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logorc1.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/logxor.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lop1-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lop1.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lop2-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lop2.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lop3-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lop3.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lxor.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lxor0-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/lxor0.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/merge.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/merge2.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/mod4.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/mulcat-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/mulcat.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/near+-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/near+.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/near-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/near.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/ocat.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/oddr-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/oddr.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/openers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/package-defs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/rewrite-theory.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/rnd.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/rom-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/round-extra.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/round-extra2.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/rtl.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/rtlarr.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/setbitn-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/setbitn.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/setbits-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/setbits.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/sgn.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/shft.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/simple-loop-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/simplify-model-helpers.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/stick-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/stick.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/sticky-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/sticky.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/sumbits.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/top.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/top1.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/trunc-proofs.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/trunc.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/support/util.lisp /usr/share/acl2-3.1/books/rtl/rel6/support/top/top.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/away.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/bias.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/bitn.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/bits-trunc.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/bits.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/brat.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/bvecp.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/cat.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/decode.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/ereps.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/land.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/lextra.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/lior.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/lnot.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/logior1.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/lxor.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/mulcat.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/near.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/setbitn.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/setbits.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/stick.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/sumbits.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/top.lisp /usr/share/acl2-3.1/books/rtl/rel6/user/trunc.lisp /usr/share/acl2-3.1/books/symbolic/generic/assertions.lisp /usr/share/acl2-3.1/books/symbolic/generic/defsimulate.lisp /usr/share/acl2-3.1/books/symbolic/generic/factorial-jvm-correct.acl2 /usr/share/acl2-3.1/books/symbolic/generic/factorial-jvm-correct.lisp /usr/share/acl2-3.1/books/symbolic/generic/measures.lisp /usr/share/acl2-3.1/books/symbolic/generic/partial-correctness.lisp /usr/share/acl2-3.1/books/symbolic/generic/tiny-fib-correct.lisp /usr/share/acl2-3.1/books/symbolic/generic/total-correctness.lisp /usr/share/acl2-3.1/books/symbolic/m5/demo.acl2 /usr/share/acl2-3.1/books/symbolic/m5/demo.lisp /usr/share/acl2-3.1/books/symbolic/m5/m5.acl2 /usr/share/acl2-3.1/books/symbolic/m5/m5.lisp /usr/share/acl2-3.1/books/symbolic/m5/utilities.acl2 /usr/share/acl2-3.1/books/symbolic/m5/utilities.lisp /usr/share/acl2-3.1/books/symbolic/tiny-fib/defstobj+.lisp /usr/share/acl2-3.1/books/symbolic/tiny-fib/fib-def.lisp /usr/share/acl2-3.1/books/symbolic/tiny-fib/tiny-rewrites.lisp /usr/share/acl2-3.1/books/symbolic/tiny-fib/tiny.lisp /usr/share/acl2-3.1/books/symbolic/tiny-triangle/tiny-triangle-correct.lisp /usr/share/acl2-3.1/books/symbolic/tiny-triangle/triangle-def.lisp /usr/share/acl2-3.1/books/textbook/chap10/ac-example.lisp /usr/share/acl2-3.1/books/textbook/chap10/adder.lisp /usr/share/acl2-3.1/books/textbook/chap10/compiler.acl2 /usr/share/acl2-3.1/books/textbook/chap10/compiler.lisp /usr/share/acl2-3.1/books/textbook/chap10/fact.lisp /usr/share/acl2-3.1/books/textbook/chap10/insertion-sort.lisp /usr/share/acl2-3.1/books/textbook/chap10/tree.lisp /usr/share/acl2-3.1/books/textbook/chap11/compress.lisp /usr/share/acl2-3.1/books/textbook/chap11/encap.lisp /usr/share/acl2-3.1/books/textbook/chap11/finite-sets.lisp /usr/share/acl2-3.1/books/textbook/chap11/how-many-soln1.lisp /usr/share/acl2-3.1/books/textbook/chap11/how-many-soln2.lisp /usr/share/acl2-3.1/books/textbook/chap11/mergesort.lisp /usr/share/acl2-3.1/books/textbook/chap11/perm-append.lisp /usr/share/acl2-3.1/books/textbook/chap11/perm.lisp /usr/share/acl2-3.1/books/textbook/chap11/qsort.lisp /usr/share/acl2-3.1/books/textbook/chap11/starters.lisp /usr/share/acl2-3.1/books/textbook/chap11/summations-book.lisp /usr/share/acl2-3.1/books/textbook/chap11/summations.lisp /usr/share/acl2-3.1/books/textbook/chap11/tautology.lisp /usr/share/acl2-3.1/books/textbook/chap11/xtr.lisp /usr/share/acl2-3.1/books/textbook/chap11/xtr2.lisp /usr/share/acl2-3.1/books/textbook/chap3/programs.lisp /usr/share/acl2-3.1/books/textbook/chap4/solutions-logic-mode.lisp /usr/share/acl2-3.1/books/textbook/chap4/solutions-program-mode.lisp /usr/share/acl2-3.1/books/textbook/chap5/solutions.lisp /usr/share/acl2-3.1/books/textbook/chap6/selected-solutions.lisp /usr/share/acl2-3.1/books/unicode/app.lisp /usr/share/acl2-3.1/books/unicode/append.lisp /usr/share/acl2-3.1/books/unicode/base10-digit-charp.lisp /usr/share/acl2-3.1/books/unicode/close-input-channel.lisp /usr/share/acl2-3.1/books/unicode/coerce.lisp /usr/share/acl2-3.1/books/unicode/combine.lisp /usr/share/acl2-3.1/books/unicode/consless-listp.lisp /usr/share/acl2-3.1/books/unicode/explode-atom.lisp /usr/share/acl2-3.1/books/unicode/explode-nonnegative-integer.lisp /usr/share/acl2-3.1/books/unicode/file-measure.lisp /usr/share/acl2-3.1/books/unicode/flatten.lisp /usr/share/acl2-3.1/books/unicode/intern-in-package-of-symbol.lisp /usr/share/acl2-3.1/books/unicode/list-fix.lisp /usr/share/acl2-3.1/books/unicode/nat-listp.lisp /usr/share/acl2-3.1/books/unicode/nthcdr-bytes.lisp /usr/share/acl2-3.1/books/unicode/nthcdr.lisp /usr/share/acl2-3.1/books/unicode/open-input-channel.lisp /usr/share/acl2-3.1/books/unicode/open-input-channels.lisp /usr/share/acl2-3.1/books/unicode/partition.lisp /usr/share/acl2-3.1/books/unicode/peek-char.lisp /usr/share/acl2-3.1/books/unicode/pos-listp.lisp /usr/share/acl2-3.1/books/unicode/read-byte.lisp /usr/share/acl2-3.1/books/unicode/read-char.lisp /usr/share/acl2-3.1/books/unicode/read-file-bytes.lisp /usr/share/acl2-3.1/books/unicode/read-file-characters.lisp /usr/share/acl2-3.1/books/unicode/read-ints.lisp /usr/share/acl2-3.1/books/unicode/read-object.lisp /usr/share/acl2-3.1/books/unicode/read-utf8.lisp /usr/share/acl2-3.1/books/unicode/repeat.lisp /usr/share/acl2-3.1/books/unicode/revappend.lisp /usr/share/acl2-3.1/books/unicode/reverse.lisp /usr/share/acl2-3.1/books/unicode/sign-byte.lisp /usr/share/acl2-3.1/books/unicode/signed-byte-listp.lisp /usr/share/acl2-3.1/books/unicode/string-append.lisp /usr/share/acl2-3.1/books/unicode/sum-list.lisp /usr/share/acl2-3.1/books/unicode/take-bytes.lisp /usr/share/acl2-3.1/books/unicode/take.lisp /usr/share/acl2-3.1/books/unicode/test-performance/tests.lisp /usr/share/acl2-3.1/books/unicode/test-performance/timing.lisp /usr/share/acl2-3.1/books/unicode/test-performance/unicode.lisp /usr/share/acl2-3.1/books/unicode/uchar.lisp /usr/share/acl2-3.1/books/unicode/unsigned-byte-listp.lisp /usr/share/acl2-3.1/books/unicode/update-state.lisp /usr/share/acl2-3.1/books/unicode/utf8-decode-string.lisp /usr/share/acl2-3.1/books/unicode/utf8-decode.lisp /usr/share/acl2-3.1/books/unicode/utf8-encode.lisp /usr/share/acl2-3.1/books/unicode/utf8-table35.lisp /usr/share/acl2-3.1/books/unicode/utf8-table36.lisp /usr/share/acl2-3.1/books/unicode/utf8.lisp /usr/share/acl2-3.1/books/unicode/z-listp.lisp /usr/share/doc/acl2-books-source/changelog.Debian.gz /usr/share/doc/acl2-books-source/copyright