[acl2/acl2] a22a29: [PFCS] Add a theorem.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: a22a2985553f82e416f6e404c5fc290ec7d40bbf
https://github.com/acl2/acl2/commit/a22a2985553f82e416f6e404c5fc290ec7d40bbf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)

Changed paths:
M books/projects/pfcs/abstract-syntax-trees.lisp

Log Message:
-----------
[PFCS] Add a theorem.


Commit: c7cd4cc7281983057c3cb206a26e6909e57495d2
https://github.com/acl2/acl2/commit/c7cd4cc7281983057c3cb206a26e6909e57495d2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)

Changed paths:
M books/acl2s/cgen/callback.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/step.lisp
A books/kestrel/arm/top.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/c/atc/expression-generation.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/function-tables.lisp
M books/kestrel/c/atc/generation-contexts.lisp
M books/kestrel/c/atc/generation.lisp
M books/kestrel/c/atc/limits.lisp
M books/kestrel/c/atc/pretty-printing-options.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/term-checkers-atc.lisp
M books/kestrel/c/atc/theorem-generation.lisp
M books/kestrel/c/package.lsp
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/u...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
A books/kestrel/c/syntax/tests/conditional.c
A books/kestrel/c/syntax/tests/gincluder1.c
A books/kestrel/c/syntax/tests/gincluder1.h
A books/kestrel/c/syntax/tests/gincluder2.c
A books/kestrel/c/syntax/tests/gincluder2.h
A books/kestrel/c/syntax/tests/gincludermod1.c
A books/kestrel/c/syntax/tests/gincludermod2.c
A books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/types.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/types.lisp
A books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
A books/kestrel/c/transformation/command-line/tests/input-files/file9.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
M books/kestrel/c/transformation/tests/add-section-attr/test3.c
M books/kestrel/c/transformation/tests/split-all-gso/extern-struct.c
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-all-gso/static-struct1.c
M books/kestrel/c/transformation/tests/split-all-gso/static-struct2.c
M books/kestrel/c/transformation/tests/split-gso/extern-struct.c
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
A books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/mach-o...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ex...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ma...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/pe-t...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/t...@useless-runes.lsp
A books/kestrel/executable-parsers/elf-tools.lisp
A books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/parse-elf-file.lisp
A books/kestrel/executable-parsers/parse-executable.lisp
A books/kestrel/executable-parsers/parse-mach-o-file.lisp
A books/kestrel/executable-parsers/parse-pe-file.lisp
A books/kestrel/executable-parsers/parsed-executable-tools.lisp
A books/kestrel/executable-parsers/parser-utils.lisp
A books/kestrel/executable-parsers/pe-tools.lisp
A books/kestrel/executable-parsers/top.lisp
M books/kestrel/json-parser/parsed-json.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/top.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/utilities/run-json-command.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
R books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/t...@useless-runes.lsp
R books/kestrel/x86/parsers/elf-tools.lisp
R books/kestrel/x86/parsers/mach-o-tools.lisp
R books/kestrel/x86/parsers/parse-elf-file.lisp
R books/kestrel/x86/parsers/parse-executable.lisp
R books/kestrel/x86/parsers/parse-mach-o-file.lisp
R books/kestrel/x86/parsers/parse-pe-file.lisp
R books/kestrel/x86/parsers/parsed-executable-tools.lisp
R books/kestrel/x86/parsers/parser-utils.lisp
R books/kestrel/x86/parsers/pe-tools.lisp
R books/kestrel/x86/parsers/top.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.lisp
R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-alt.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval_poly.defhol
M books/projects/hol-in-acl2/examples/eval_polyScript.sml

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/de23e2d6a421...c7cd4cc72819

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel