Search-engine friendly clone of the
ACL2 documentation
.
Top
ACL2 Index
!_
!_-fn
!call-gate-descriptor-attributesbits->dpl
!call-gate-descriptor-attributesbits->p
!call-gate-descriptor-attributesbits->s
!call-gate-descriptor-attributesbits->type
!call-gate-descriptor-attributesbits->unknownbits
!call-gate-descriptorbits->all-zeroes?
!call-gate-descriptorbits->dpl
!call-gate-descriptorbits->offset15-0
!call-gate-descriptorbits->offset31-16
!call-gate-descriptorbits->offset63-32
!call-gate-descriptorbits->p
!call-gate-descriptorbits->res1
!call-gate-descriptorbits->res2
!call-gate-descriptorbits->res3
!call-gate-descriptorbits->s
!call-gate-descriptorbits->selector
!call-gate-descriptorbits->type
!code-segment-descriptor-attributesbits->a
!code-segment-descriptor-attributesbits->avl
!code-segment-descriptor-attributesbits->c
!code-segment-descriptor-attributesbits->d
!code-segment-descriptor-attributesbits->dpl
!code-segment-descriptor-attributesbits->g
!code-segment-descriptor-attributesbits->l
!code-segment-descriptor-attributesbits->msb-of-type
!code-segment-descriptor-attributesbits->p
!code-segment-descriptor-attributesbits->r
!code-segment-descriptor-attributesbits->s
!code-segment-descriptor-attributesbits->unknownbits
!code-segment-descriptorbits->a
!code-segment-descriptorbits->avl
!code-segment-descriptorbits->base15-0
!code-segment-descriptorbits->base23-16
!code-segment-descriptorbits->base31-24
!code-segment-descriptorbits->c
!code-segment-descriptorbits->d
!code-segment-descriptorbits->dpl
!code-segment-descriptorbits->g
!code-segment-descriptorbits->l
!code-segment-descriptorbits->limit15-0
!code-segment-descriptorbits->limit19-16
!code-segment-descriptorbits->msb-of-type
!code-segment-descriptorbits->p
!code-segment-descriptorbits->r
!code-segment-descriptorbits->s
!cr0bits->am
!cr0bits->cd
!cr0bits->em
!cr0bits->et
!cr0bits->mp
!cr0bits->ne
!cr0bits->nw
!cr0bits->pe
!cr0bits->pg
!cr0bits->res1
!cr0bits->res2
!cr0bits->res3
!cr0bits->ts
!cr0bits->wp
!cr3bits->pcd
!cr3bits->pdb
!cr3bits->pwt
!cr3bits->res1
!cr3bits->res2
!cr3bits->res3
!cr4bits->de
!cr4bits->fsgsbase
!cr4bits->la57
!cr4bits->mce
!cr4bits->osfxsr
!cr4bits->osxmmexcpt
!cr4bits->osxsave
!cr4bits->pae
!cr4bits->pce
!cr4bits->pcide
!cr4bits->pge
!cr4bits->pse
!cr4bits->pvi
!cr4bits->res1
!cr4bits->res2
!cr4bits->smap
!cr4bits->smep
!cr4bits->smxe
!cr4bits->tsd
!cr4bits->umip
!cr4bits->vme
!cr4bits->vmxe
!cr8bits->cr8-trpl
!ctri-from-alist
!cutinfo->score
!cutinfo->size
!cutinfo->truth
!cutinfo->valid
!data-segment-descriptor-attributesbits->a
!data-segment-descriptor-attributesbits->avl
!data-segment-descriptor-attributesbits->d/b
!data-segment-descriptor-attributesbits->dpl
!data-segment-descriptor-attributesbits->e
!data-segment-descriptor-attributesbits->g
!data-segment-descriptor-attributesbits->l
!data-segment-descriptor-attributesbits->msb-of-type
!data-segment-descriptor-attributesbits->p
!data-segment-descriptor-attributesbits->s
!data-segment-descriptor-attributesbits->unknownbits
!data-segment-descriptor-attributesbits->w
!data-segment-descriptorbits->a
!data-segment-descriptorbits->avl
!data-segment-descriptorbits->base15-0
!data-segment-descriptorbits->base23-16
!data-segment-descriptorbits->base31-24
!data-segment-descriptorbits->d/b
!data-segment-descriptorbits->dpl
!data-segment-descriptorbits->e
!data-segment-descriptorbits->g
!data-segment-descriptorbits->l
!data-segment-descriptorbits->limit15-0
!data-segment-descriptorbits->limit19-16
!data-segment-descriptorbits->msb-of-type
!data-segment-descriptorbits->p
!data-segment-descriptorbits->s
!data-segment-descriptorbits->w
!elf32_sym->info
!elf32_sym->name
!elf32_sym->other
!elf32_sym->shndx
!elf32_sym->size
!elf32_sym->value
!elf64_sym->info
!elf64_sym->name
!elf64_sym->other
!elf64_sym->shndx
!elf64_sym->size
!elf64_sym->value
!evex-byte1->b
!evex-byte1->mm
!evex-byte1->r
!evex-byte1->r-prime
!evex-byte1->res
!evex-byte1->x
!evex-byte2->pp
!evex-byte2->res
!evex-byte2->vvvv
!evex-byte2->w
!evex-byte3->aaa
!evex-byte3->b
!evex-byte3->v-prime
!evex-byte3->vl/rc
!evex-byte3->z
!evex-prefixes->byte0
!evex-prefixes->byte1
!evex-prefixes->byte2
!evex-prefixes->byte3
!fgl-function-mode->dont-concrete-exec
!fgl-function-mode->dont-expand-def
!fgl-function-mode->dont-primitive-exec
!fgl-function-mode->dont-rewrite
!fgl-function-mode->dont-rewrite-under-if-test
!fgl-function-mode->split-ifs
!fp-statusbits->b
!fp-statusbits->c0
!fp-statusbits->c1
!fp-statusbits->c2
!fp-statusbits->c3
!fp-statusbits->de
!fp-statusbits->es
!fp-statusbits->ie
!fp-statusbits->oe
!fp-statusbits->pe
!fp-statusbits->sf
!fp-statusbits->top
!fp-statusbits->ue
!fp-statusbits->ze
!gatesimp->hashp
!gatesimp->level
!gatesimp->xor-mode
!gdtr/idtrbits->base-addr
!gdtr/idtrbits->limit
!hidden-segment-registerbits->attr
!hidden-segment-registerbits->base-addr
!hidden-segment-registerbits->limit
!ia32_eferbits->lma
!ia32_eferbits->lme
!ia32_eferbits->nxe
!ia32_eferbits->res1
!ia32_eferbits->res2
!ia32_eferbits->sce
!ia32e-page-tablesbits->a
!ia32e-page-tablesbits->d
!ia32e-page-tablesbits->p
!ia32e-page-tablesbits->pcd
!ia32e-page-tablesbits->ps
!ia32e-page-tablesbits->pwt
!ia32e-page-tablesbits->r/w
!ia32e-page-tablesbits->reference-addr
!ia32e-page-tablesbits->res1
!ia32e-page-tablesbits->res2
!ia32e-page-tablesbits->u/s
!ia32e-page-tablesbits->xd
!ia32e-pde-2mb-pagebits->a
!ia32e-pde-2mb-pagebits->d
!ia32e-pde-2mb-pagebits->g
!ia32e-pde-2mb-pagebits->p
!ia32e-pde-2mb-pagebits->page
!ia32e-pde-2mb-pagebits->pat
!ia32e-pde-2mb-pagebits->pcd
!ia32e-pde-2mb-pagebits->ps
!ia32e-pde-2mb-pagebits->pwt
!ia32e-pde-2mb-pagebits->r/w
!ia32e-pde-2mb-pagebits->res1
!ia32e-pde-2mb-pagebits->res2
!ia32e-pde-2mb-pagebits->res3
!ia32e-pde-2mb-pagebits->u/s
!ia32e-pde-2mb-pagebits->xd
!ia32e-pde-pg-tablebits->a
!ia32e-pde-pg-tablebits->p
!ia32e-pde-pg-tablebits->pcd
!ia32e-pde-pg-tablebits->ps
!ia32e-pde-pg-tablebits->pt
!ia32e-pde-pg-tablebits->pwt
!ia32e-pde-pg-tablebits->r/w
!ia32e-pde-pg-tablebits->res1
!ia32e-pde-pg-tablebits->res2
!ia32e-pde-pg-tablebits->res3
!ia32e-pde-pg-tablebits->u/s
!ia32e-pde-pg-tablebits->xd
!ia32e-pdpte-1gb-pagebits->a
!ia32e-pdpte-1gb-pagebits->d
!ia32e-pdpte-1gb-pagebits->g
!ia32e-pdpte-1gb-pagebits->p
!ia32e-pdpte-1gb-pagebits->page
!ia32e-pdpte-1gb-pagebits->pat
!ia32e-pdpte-1gb-pagebits->pcd
!ia32e-pdpte-1gb-pagebits->ps
!ia32e-pdpte-1gb-pagebits->pwt
!ia32e-pdpte-1gb-pagebits->r/w
!ia32e-pdpte-1gb-pagebits->res1
!ia32e-pdpte-1gb-pagebits->res2
!ia32e-pdpte-1gb-pagebits->res3
!ia32e-pdpte-1gb-pagebits->u/s
!ia32e-pdpte-1gb-pagebits->xd
!ia32e-pdpte-pg-dirbits->a
!ia32e-pdpte-pg-dirbits->p
!ia32e-pdpte-pg-dirbits->pcd
!ia32e-pdpte-pg-dirbits->pd
!ia32e-pdpte-pg-dirbits->ps
!ia32e-pdpte-pg-dirbits->pwt
!ia32e-pdpte-pg-dirbits->r/w
!ia32e-pdpte-pg-dirbits->res1
!ia32e-pdpte-pg-dirbits->res2
!ia32e-pdpte-pg-dirbits->res3
!ia32e-pdpte-pg-dirbits->u/s
!ia32e-pdpte-pg-dirbits->xd
!ia32e-pml4ebits->a
!ia32e-pml4ebits->p
!ia32e-pml4ebits->pcd
!ia32e-pml4ebits->pdpt
!ia32e-pml4ebits->ps
!ia32e-pml4ebits->pwt
!ia32e-pml4ebits->r/w
!ia32e-pml4ebits->res1
!ia32e-pml4ebits->res2
!ia32e-pml4ebits->res3
!ia32e-pml4ebits->u/s
!ia32e-pml4ebits->xd
!ia32e-pte-4k-pagebits->a
!ia32e-pte-4k-pagebits->d
!ia32e-pte-4k-pagebits->g
!ia32e-pte-4k-pagebits->p
!ia32e-pte-4k-pagebits->page
!ia32e-pte-4k-pagebits->pat
!ia32e-pte-4k-pagebits->pcd
!ia32e-pte-4k-pagebits->pwt
!ia32e-pte-4k-pagebits->r/w
!ia32e-pte-4k-pagebits->res1
!ia32e-pte-4k-pagebits->res2
!ia32e-pte-4k-pagebits->u/s
!ia32e-pte-4k-pagebits->xd
!interp-flags->branch-on-ifs
!interp-flags->intro-bvars
!interp-flags->intro-synvars
!interp-flags->make-ites
!interp-flags->simplify-logic
!interp-flags->trace-rewrites
!interrupt/trap-gate-descriptor-attributesbits->dpl
!interrupt/trap-gate-descriptor-attributesbits->ist
!interrupt/trap-gate-descriptor-attributesbits->p
!interrupt/trap-gate-descriptor-attributesbits->s
!interrupt/trap-gate-descriptor-attributesbits->type
!interrupt/trap-gate-descriptor-attributesbits->unknownbits
!interrupt/trap-gate-descriptorbits->all-zeros?
!interrupt/trap-gate-descriptorbits->dpl
!interrupt/trap-gate-descriptorbits->ist
!interrupt/trap-gate-descriptorbits->offset15-0
!interrupt/trap-gate-descriptorbits->offset31-16
!interrupt/trap-gate-descriptorbits->offset63-32
!interrupt/trap-gate-descriptorbits->p
!interrupt/trap-gate-descriptorbits->res1
!interrupt/trap-gate-descriptorbits->res2
!interrupt/trap-gate-descriptorbits->res3
!interrupt/trap-gate-descriptorbits->s
!interrupt/trap-gate-descriptorbits->selector
!interrupt/trap-gate-descriptorbits->type
!log-file-name
!mmx
!modr/m->mod
!modr/m->r/m
!modr/m->reg
!msri-from-alist
!mxcsrbits->daz
!mxcsrbits->de
!mxcsrbits->dm
!mxcsrbits->fz
!mxcsrbits->ie
!mxcsrbits->im
!mxcsrbits->oe
!mxcsrbits->om
!mxcsrbits->pe
!mxcsrbits->pm
!mxcsrbits->rc
!mxcsrbits->reserved
!mxcsrbits->ue
!mxcsrbits->um
!mxcsrbits->ze
!mxcsrbits->zm
!npn4->negate
!npn4->perm
!npn4->polarity
!npn4->truth-idx
!prefixes->adr
!prefixes->lck
!prefixes->num
!prefixes->nxt
!prefixes->opr
!prefixes->rep
!prefixes->seg
!rflagsbits->ac
!rflagsbits->af
!rflagsbits->cf
!rflagsbits->df
!rflagsbits->id
!rflagsbits->intf
!rflagsbits->iopl
!rflagsbits->nt
!rflagsbits->of
!rflagsbits->pf
!rflagsbits->res1
!rflagsbits->res2
!rflagsbits->res3
!rflagsbits->res4
!rflagsbits->res5
!rflagsbits->rf
!rflagsbits->sf
!rflagsbits->tf
!rflagsbits->vif
!rflagsbits->vip
!rflagsbits->vm
!rflagsbits->zf
!rgfi-from-alist
!rgfi-size
!seg-hidden-attri-from-alist
!seg-hidden-basei-from-alist
!seg-hidden-limiti-from-alist
!seg-visiblei-from-alist
!segment-selectorbits->index
!segment-selectorbits->rpl
!segment-selectorbits->ti
!sib->base
!sib->index
!sib->scale
!simpcode->choice
!simpcode->identity
!simpcode->neg
!simpcode->xor
!system-segment-descriptor-attributesbits->avl
!system-segment-descriptor-attributesbits->dpl
!system-segment-descriptor-attributesbits->g
!system-segment-descriptor-attributesbits->p
!system-segment-descriptor-attributesbits->s
!system-segment-descriptor-attributesbits->type
!system-segment-descriptor-attributesbits->unknownbits
!system-segment-descriptorbits->all-zeroes?
!system-segment-descriptorbits->avl
!system-segment-descriptorbits->base15-0
!system-segment-descriptorbits->base23-16
!system-segment-descriptorbits->base31-24
!system-segment-descriptorbits->base63-32
!system-segment-descriptorbits->dpl
!system-segment-descriptorbits->g
!system-segment-descriptorbits->limit15-0
!system-segment-descriptorbits->limit19-16
!system-segment-descriptorbits->p
!system-segment-descriptorbits->res1
!system-segment-descriptorbits->res2
!system-segment-descriptorbits->res3
!system-segment-descriptorbits->s
!system-segment-descriptorbits->type
!vex-prefixes->byte0
!vex-prefixes->byte1
!vex-prefixes->byte2
!vex2-byte1->l
!vex2-byte1->pp
!vex2-byte1->r
!vex2-byte1->vvvv
!vex3-byte1->b
!vex3-byte1->m-mmmm
!vex3-byte1->r
!vex3-byte1->x
!vex3-byte2->l
!vex3-byte2->pp
!vex3-byte2->vvvv
!vex3-byte2->w
!xcr0bits->avx-state
!xcr0bits->bndcsr-state
!xcr0bits->bndreg-state
!xcr0bits->fpu/mmx-state
!xcr0bits->hi16_zmm-state
!xcr0bits->opmask-state
!xcr0bits->pkru-state
!xcr0bits->res1
!xcr0bits->res2
!xcr0bits->sse-state
!xcr0bits->zmm_hi256-state
!xmmi-size
!zmmi-size
%b-
%b.
%b.-fn
%d-
%d.
%d.-fn
%x-
%x.
%x.-fn
&&
&allow-other-keys
&body
&key
&optional
&rest
&whole
>
>=
<
<>
<<
<=
(= 0 (ash 1 x))
*
*-listp
*60-bit-mask*
*ACL2-exports*
*ACL2-system-exports*
*_
*account-index*
*aij-class-names*
*aij-natives*
*aij-package*
*aij-symbol-constants*
*all-grammar-rules*
*all-grammar-rules*-tree-operations
*all-http-grammar-rules*
*all-http-grammar-rules*-tree-operations
*all-http-message-grammar-rules*
*all-uri-grammar-rules*
*all-uri-grammar-rules*-tree-operations
*alpha*
*alternation*
*atc-adjust-type-rules*
*atc-all-rules*
*atc-allowed-options*
*atc-allowed-pretty-printing-options*
*atc-apconvert-rules*
*atc-array-length-rules*
*atc-array-length-write-rules*
*atc-array-read-return-rewrite-rules*
*atc-array-read-rules*
*atc-array-read-type-prescription-rules*
*atc-array-write-return-rewrite-rules*
*atc-array-write-type-prescription-rules*
*atc-boolean-from-integer-return-rules*
*atc-boolean-from-sint*
*atc-boolean-from-type-fns*
*atc-compound-recognizer-rules*
*atc-compustate-frames-number-rules*
*atc-computation-state-return-rules*
*atc-convert-integer-value-rules*
*atc-create-var-rules*
*atc-distributivity-over-if-rewrite-rules*
*atc-exec-arrsub-rules*
*atc-exec-binary-strict-pure-rules*
*atc-exec-block-item-list-rules*
*atc-exec-block-item-rules*
*atc-exec-cast-rules*
*atc-exec-const-rules*
*atc-exec-expr-asg-arrsub-rules*
*atc-exec-expr-asg-ident-rules*
*atc-exec-expr-asg-indir-rules*
*atc-exec-expr-asg-rules*
*atc-exec-expr-call-or-asg-rules*
*atc-exec-expr-call-or-pure-rules*
*atc-exec-expr-call-rules*
*atc-exec-expr-pure-list-rules*
*atc-exec-expr-pure-rules*
*atc-exec-fun-rules*
*atc-exec-ident-rules*
*atc-exec-indir-rules*
*atc-exec-initer-rules*
*atc-exec-stmt-rules*
*atc-exec-unary-nonpointer-rules*
*atc-exit-scope-rules*
*atc-flexible-array-member-rules*
*atc-identifier-rules*
*atc-init-scope-rules*
*atc-init-value-to-value-rules*
*atc-integer-const-rules*
*atc-integer-constructors-return-rules*
*atc-integer-conv-rules*
*atc-integer-convs-return-rewrite-rules*
*atc-integer-convs-type-prescription-rules*
*atc-integer-fix-rules*
*atc-integer-ifix-rules*
*atc-integer-ops-1-return-rewrite-rules*
*atc-integer-ops-1-type-prescription-rules*
*atc-integer-ops-2-return-rewrite-rules*
*atc-integer-ops-2-type-prescription-rules*
*atc-integer-size-rules*
*atc-limit-rules*
*atc-lognot-sint-rules*
*atc-misc-rewrite-rules*
*atc-not-error-rules*
*atc-object-designator-rules*
*atc-op-type-fns*
*atc-op-type1-type2-fns*
*atc-other-executable-counterpart-rules*
*atc-pointed-integer-rules*
*atc-pointed-integers-type-prescription-rules*
*atc-pop-frame-rules*
*atc-promote-value-rules*
*atc-push-frame-rules*
*atc-read-object-rules*
*atc-read-static-var-rules*
*atc-read-var-rules*
*atc-sint-from-boolean*
*atc-sint-get-rules*
*atc-static-variable-pointer-rules*
*atc-symbolic-computation-state-rules*
*atc-table*
*atc-test-value-rules*
*atc-tyname-to-type-rules*
*atc-type-base-const-fns*
*atc-type-kind-rules*
*atc-type-of-value-option-rules*
*atc-type-of-value-rules*
*atc-type-prescription-rules*
*atc-type1-from-type2-fns*
*atc-uaconvert-values-rules*
*atc-update-object-rules*
*atc-update-static-var-rules*
*atc-update-var-rules*
*atc-value-array->elemtype-rules*
*atc-value-fix-rules*
*atc-value-integer->get-rules*
*atc-value-kind-rules*
*atc-value-listp-rules*
*atc-value-optionp-rules*
*atc-value-result-fix-rules*
*atc-valuep-rules*
*atc-var-autop-rules*
*atc-wrapper-rules*
*atc-write-object-rules*
*atc-write-static-var-rules*
*atc-write-var-rules*
*atj-allowed-options*
*atj-default-java-class*
*atj-disallowed-class-names*
*atj-disallowed-jvar-names*
*atj-disallowed-method-names*
*atj-function-type-info-table-name*
*atj-gen-cond-exprs*
*atj-gen-pkg-name-alist*
*atj-init-indices*
*atj-java-lang-class-names*
*atj-jprim-binop-fns*
*atj-jprim-constr-fns*
*atj-jprim-conv-fns*
*atj-jprim-deconstr-fns*
*atj-jprim-fns*
*atj-jprim-unop-fns*
*atj-jprimarr-conv-fromlist-fns*
*atj-jprimarr-conv-tolist-fns*
*atj-jprimarr-fns*
*atj-jprimarr-length-fns*
*atj-jprimarr-new-init-fns*
*atj-jprimarr-new-len-fns*
*atj-jprimarr-read-fns*
*atj-jprimarr-write-fns*
*atj-mv-factory-method-name*
*atj-mv-singleton-field-name*
*atj-predefined-method-names*
*atj-primarray-write-method-names*
*b64-chars-from-vals-array*
*b64-vals-from-codes-array*
*base58-characters*
*base58-zero*
*bech32-char-vals*
*bech32m-const*
*bin-val*
*bip32-version-priv-main*
*bip32-version-priv-test*
*bip32-version-pub-main*
*bip32-version-pub-test*
*bip39-english-words*
*bip44-purpose*
*bit*
*boolean-literals*
*builtin-function-names*
*c-nl*
*c-wsp*
*case-insensitive-string*
*case-sensitive-string*
*char*
*char-val*
*coin-type-index*
*command-name-init-from-entropy*
*command-name-init-from-mnemonic*
*command-name-next-key*
*command-name-sign*
*comment*
*common-lisp-symbols-from-main-lisp-package*
*concatenation*
*concrete-syntax-rules*
*concrete-syntax-rules-parsed*
*concrete-syntax-rules-parsed-and-abstracted*
*core-rules*
*core-rules-parsed*
*core-rules-parsed-and-abstracted*
*cr*
*crlf*
*ctl*
*ctype-code-map*
*dec-val*
*defarbrec-table-name*
*default-config*
*default-numbered-name-index-end*
*default-numbered-name-index-start*
*default-numbered-name-index-wildcard*
*default-paired-name-separator*
*defaults-table-name*
*defbyte-table-name*
*defdefparse-allowed-options*
*defdigits-table-name*
*defgrammar-allowed-options*
*defined-as*
*definterface-hash-table-name*
*definterface-hmac-table-name*
*defmapping-table-name*
*defobject-table*
*defparse-yul-group-table*
*defparse-yul-option-table*
*defparse-yul-repetition-table*
*defstruct-table*
*deftreeops-allowed-options*
*demo-usage*
*demo2-opts-usage*
*digit*
*double-quote-tree-list*
*double-quoted-content-rulenames*
*dquote*
*element*
*elements*
*empty-lt*
*esim-and*
*esim-buf*
*esim-bufif0*
*esim-bufif1*
*esim-ceq*
*esim-cmos*
*esim-del*
*esim-f*
*esim-fsmreg*
*esim-id*
*esim-latch*
*esim-nand*
*esim-nmos*
*esim-nor*
*esim-not*
*esim-notif0*
*esim-notif1*
*esim-or*
*esim-pmos*
*esim-primitives*
*esim-safe-mux*
*esim-t*
*esim-tri*
*esim-unsafe-mux*
*esim-x*
*esim-xnor*
*esim-xor*
*esim-z*
*esim-zif*
*external-chain-index*
*fake-modelement*
*file-types*
*grammar*
*grammar*
*grammar*
*grammar*
*grammar*-tree-operations
*grammar*-tree-operations
*grammar*-tree-operations
*grammar-new*
*grammar-new*-tree-operations
*grammar-old*
*grammar-parser-error-msg*
*grammar-rules*
*group*
*hex-val*
*hexdig*
*htab*
*http-grammar-rules*
*imap-grammar-rules*
*imap-grammar-rules*-tree-operations
*imf-grammar-rules*
*imf-grammar-rules*-tree-operations
*jkeywords*
*jubjub-l*
*key-path-prefix*
*keywords*
*l-merkle-sapling*
*lexical-grammar*
*lf*
*list-leafterm-92*
*list-leafterm-u*
*list-leafterm-x*
*logops-functions*
*lwsp*
*newline*
*nls*
*nls*
*nonchar-integer-fixtypes*
*nonchar-integer-types*
*not-toohard-ops*
*null-literal*
*num-val*
*octet*
*option*
*pdf-grammar-rules*
*pdf-grammar-rules*-tree-operations
*pedersen-c*
*prose-val*
*purpose-index*
*quoted-string*
*repeat*
*repetition*
*restricted-jkeywords*
*rule*
*rule_alpha*
*rule_alternation*
*rule_bin-val*
*rule_bit*
*rule_c-nl*
*rule_c-wsp*
*rule_case-insensitive-string*
*rule_case-sensitive-string*
*rule_char*
*rule_char-val*
*rule_comment*
*rule_concatenation*
*rule_cr*
*rule_crlf*
*rule_ctl*
*rule_dec-val*
*rule_defined-as*
*rule_digit*
*rule_dquote*
*rule_element*
*rule_elements*
*rule_group*
*rule_hex-val*
*rule_hexdig*
*rule_htab*
*rule_lf*
*rule_lwsp*
*rule_num-val*
*rule_octet*
*rule_option*
*rule_prose-val*
*rule_quoted-string*
*rule_repeat*
*rule_repetition*
*rule_rule*
*rule_rulelist*
*rule_rulename*
*rule_sp*
*rule_vchar*
*rule_wsp*
*rulelist*
*rulename*
*sbitset-block-size*
*schemalg-schemas*
*sexpr-rewrites*
*single-quote-tree-list*
*single-quoted-content-rulenames*
*smt-architecture*
*smt-basics*
*smt-functions*
*smt-types*
*smt-uninterpreted-types*
*smtp-grammar-rules*
*smtp-grammar-rules*-tree-operations
*solve-call-ACL2-rewriter*
*solve-call-axe-rewriter*
*sp*
*standard-ci*
*standard-co*
*standard-oi*
*stat-filepath*
*stv2c-opts-usage*
*stype-ctype-map*
*svex-op-table*
*syntactic-grammar*
*toohard-ops*
*typo-numbers*
*typo-numbers*
*typo-special-substrings-chars*
*typo-special-substrings-chars*
*uncommitted-sapling*
*untranslate-specifier-keywords*
*uri-grammar-rules*
*url-encode-array*
*urs*
*vchar*
*vl-1-bit-adder-core*
*vl-1-bit-adder-core-support*
*vl-1-bit-and*
*vl-1-bit-approx-mux*
*vl-1-bit-assign*
*vl-1-bit-buf*
*vl-1-bit-bufif0*
*vl-1-bit-bufif1*
*vl-1-bit-ceq*
*vl-1-bit-cmos*
*vl-1-bit-delay-1*
*vl-1-bit-div-rem*
*vl-1-bit-dynamic-bitselect*
*vl-1-bit-f*
*vl-1-bit-ground*
*vl-1-bit-latch*
*vl-1-bit-mult*
*vl-1-bit-mux*
*vl-1-bit-nand*
*vl-1-bit-nmos*
*vl-1-bit-nor*
*vl-1-bit-not*
*vl-1-bit-notif0*
*vl-1-bit-notif1*
*vl-1-bit-or*
*vl-1-bit-pmos*
*vl-1-bit-power*
*vl-1-bit-pulldown*
*vl-1-bit-pullup*
*vl-1-bit-rcmos*
*vl-1-bit-rnmos*
*vl-1-bit-rpmos*
*vl-1-bit-rtran*
*vl-1-bit-rtranif0*
*vl-1-bit-rtranif1*
*vl-1-bit-signed-gte*
*vl-1-bit-t*
*vl-1-bit-tran*
*vl-1-bit-tranif0*
*vl-1-bit-tranif1*
*vl-1-bit-x*
*vl-1-bit-xnor*
*vl-1-bit-xor*
*vl-1-bit-z*
*vl-1-bit-zmux*
*vl-2-bit-dynamic-bitselect*
*vl-2005-keyword-table*
*vl-2005-keyword-table*
*vl-2005-keyword-table-strict*
*vl-2005-keyword-table-strict*
*vl-2005-keywords*
*vl-2005-keywords*
*vl-2005-lexstate*
*vl-2005-lexstate*
*vl-2005-plain-nonkeywords*
*vl-2005-plain-nonkeywords*
*vl-2005-strict-lexstate*
*vl-2005-strict-lexstate*
*vl-2012-keyword-table*
*vl-2012-keyword-table*
*vl-2012-keyword-table-strict*
*vl-2012-keyword-table-strict*
*vl-2012-keywords*
*vl-2012-keywords*
*vl-2012-lexstate*
*vl-2012-lexstate*
*vl-2012-plain-nonkeywords*
*vl-2012-plain-nonkeywords*
*vl-2012-strict-lexstate*
*vl-2012-strict-lexstate*
*vl-assignment-operators*
*vl-binary-ops*
*vl-charge-strengths-alist*
*vl-charge-strengths-alist*
*vl-charge-strengths-keywords*
*vl-charge-strengths-keywords*
*vl-core-data-type-table*
*vl-core-data-type-table*
*vl-current-syntax-version*
*vl-current-syntax-version*
*vl-default-expr*
*vl-default-token*
*vl-default-token*
*vl-directions-kwd-alist*
*vl-directions-kwd-alist*
*vl-directions-kwds*
*vl-directions-kwds*
*vl-ds0-alist*
*vl-ds0-alist*
*vl-ds0-keywords*
*vl-ds0-keywords*
*vl-ds0/1-keywords*
*vl-ds0/1-keywords*
*vl-ds1-alist*
*vl-ds1-alist*
*vl-ds1-keywords*
*vl-ds1-keywords*
*vl-empty-lucidval*
*vl-empty-lucidval*
*vl-end-of-sequence-$*
*vl-extra-keywords*
*vl-extra-keywords*
*vl-fake-elem-for-vl-consteval*
*vl-fakeloc*
*vl-fakeloc*
*vl-gather-help*
*vl-gather-opts-usage*
*vl-gather-opts-usage*
*vl-html-&*
*vl-html->*
*vl-html-<*
*vl-html- *
*vl-html-"*
*vl-html-newline*
*vl-incexpr-1*
*vl-json-opts-usage*
*vl-json-opts-usage*
*vl-json-readme*
*vl-lint-help*
*vl-lint-help*
*vl-lintconfig-usage*
*vl-lintconfig-usage*
*vl-model-opts-usage*
*vl-odd-binops-table*
*vl-odd-binops-table*
*vl-ops-table*
*vl-plain-old-integer-type*
*vl-plain-old-integer-type*
*vl-plain-old-logic-type*
*vl-plain-old-real-type*
*vl-plain-old-real-type*
*vl-plain-old-realtime-type*
*vl-plain-old-realtime-type*
*vl-plain-old-reg-type*
*vl-plain-old-reg-type*
*vl-plain-old-time-type*
*vl-plain-old-time-type*
*vl-plain-old-wire-type*
*vl-plaintoken-fal*
*vl-plaintoken-fal*
*vl-plaintoken-types*
*vl-plaintoken-types*
*vl-pp-opts-usage*
*vl-preprocess-clock*
*vl-preprocess-clock*
*vl-scopes->classes*
*vl-scopes->defs*
*vl-scopes->defs*
*vl-scopes->items*
*vl-scopes->items*
*vl-scopes->pkgs*
*vl-scopes->pkgs*
*vl-scopes->portdecls*
*vl-scopes->portdecls*
*vl-server-help*
*vl-server-opts-usage*
*vl-server-opts-usage*
*vl-shell-help*
*vl-strength0-alist*
*vl-strength0-alist*
*vl-strength1-alist*
*vl-strength1-alist*
*vl-tmp-wire-atts*
*vl-trivially-true-property-expr*
*vl-unary-ops*
*vl-url-encode-array*
*vl-very-simple-type-table*
*vl-very-simple-type-table*
*vl-very-simple-type-tokens*
*vl-very-simple-type-tokens*
*vl-x-wire-expr*
*vl-z-wire-expr*
*vl-zip-help*
*vl-zip-opts-usage*
*vls-root*
*wsp*
*yul-keywords*
*yul-symbols*
+
-
/
/=
/_
/_-fn
0f-38-three-byte-opcodes-map
0f-3a-three-byte-opcodes-map
1*_
1+
1-
1. An Example GL Proof
100-theorems
10bits
10bits-fix
10bits-p
11bits
11bits-fix
11bits-p
12bits
12bits-fix
12bits-p
13bits
13bits-fix
13bits-p
16bits
16bits-fix
16bits-p
17bits
17bits-fix
17bits-p
19bits
19bits-fix
19bits-p
2. Symbolic Objects
22bits
22bits-fix
22bits-p
24bits
24bits-fix
24bits-p
2bits
2bits-fix
2bits-p
2vec
2vec->val
2vec-p
2vecnatx
2vecnatx-equiv
2vecnatx-fix
2vecnatx-p
2vecnatx-p!
2vecx
2vecx-equiv
2vecx-fix
2vecx-p
2vexc-p!
3. Computing with Symbolic Objects
31bits
31bits-fix
31bits-p
32-bit-compute-mandatory-prefix-for-0f-38-three-byte-opcode
32-bit-compute-mandatory-prefix-for-0f-3a-three-byte-opcode
32-bit-compute-mandatory-prefix-for-two-byte-opcode
32-bit-mode-0f-38-three-byte-opcode-modr/m-p
32-bit-mode-0f-3a-three-byte-opcode-modr/m-p
32-bit-mode-one-byte-opcode-modr/m-p
32-bit-mode-two-byte-opcode-modr/m-p
32bits
32bits-fix
32bits-p
3bits
3bits-fix
3bits-p
3col4vecline
3col4vecline->label
3col4vecline->val
3col4vecline->val2
3col4vecline-equiv
3col4vecline-fix
3col4vecline-p
3col4vecs
3col4vecs-equiv
3col4vecs-fix
3col4vecs-p
3col4vecs-p-basics
3v-syntax-sexprp
3vec
3vec-==
3vec-?
3vec-?*
3vec-bit?
3vec-bitand
3vec-bitnot
3vec-bitor
3vec-bitxor
3vec-equiv
3vec-fix
3vec-fix-fast
3vec-operations
3vec-p
3vec-p!
3vec-reduction-and
3vec-reduction-or
4. Proving Theorems by Symbolic Execution
40bits
40bits-fix
40bits-p
4bits
4bits-fix
4bits-p
4v
4v->4vec-bit
4v->faig-const
4v-<=
4v-alist->faig-const-alist
4v-alist-<=
4v-alist-extract
4v-alists-agree
4v-alists-disagree-witness
4v-and
4v-and-faig-operations-commute
4v-and-list
4v-cdr-consp-equiv
4v-cdr-equiv
4v-env-equiv
4v-equiv
4v-fix
4v-iff
4v-ite
4v-ite*
4v-list->faig-const-list
4v-list-<=
4v-lookup
4v-monotonicity
4v-not
4v-not-list
4v-nsexpr-alist-p
4v-nsexpr-p
4v-nsexpr-p-4v-sexpr-compose
4v-nsexpr-p-4v-sexpr-restrict
4v-nsexpr-vars
4v-nsexpr-vars-nonsparse
4v-nsexpr-vars-sparse
4v-onehot-filter
4v-onehot-list-p
4v-onehot-rw-sexpr
4v-onehot-rw-sexpr-alist
4v-onehot-rw-sexpr-alist-aux
4v-onehot-sexpr-list-prime
4v-onehot-sexpr-prime
4v-operations
4v-or
4v-pullup
4v-res
4v-sexpr-<=
4v-sexpr-alist-<=
4v-sexpr-alist-<=-alt
4v-sexpr-alist-equiv
4v-sexpr-alist-equiv-alt
4v-sexpr-alist-extract
4v-sexpr-alist-pair-equiv
4v-sexpr-compose
4v-sexpr-compose-alist
4v-sexpr-compose-nofal
4v-sexpr-compose-with-rw
4v-sexpr-equiv
4v-sexpr-eval
4v-sexpr-eval-alist
4v-sexpr-eval-alists
4v-sexpr-eval-list
4v-sexpr-eval-list-list
4v-sexpr-ind
4v-sexpr-list-equiv
4v-sexpr-purebool-check
4v-sexpr-purebool-list-check
4v-sexpr-purebool-list-p
4v-sexpr-purebool-list-p-basics
4v-sexpr-purebool-list-p-to-faig-purebool-list-p
4v-sexpr-purebool-p
4v-sexpr-restrict
4v-sexpr-restrict-alist
4v-sexpr-restrict-list
4v-sexpr-restrict-with-rw
4v-sexpr-simp-and-eval
4v-sexpr-to-faig
4v-sexpr-to-faig-alist
4v-sexpr-to-faig-list
4v-sexpr-to-faig-opt
4v-sexpr-to-faig-plain
4v-sexpr-vars
4v-sexpr-vars-1pass
4v-sexpr-vars-1pass-list
4v-sexpr-vars-1pass-list-list
4v-sexpr-vars-alist
4v-sexpr-vars-alists
4v-sexpr-vars-list
4v-sexpr-vars-list-list
4v-sexprs
4v-shannon-expansion
4v-to-characterp
4v-tristate
4v-unfloat
4v-wand
4v-wor
4v-xdet
4v-xor
4v-zif
4vcases
4vec
4vec->a4vec
4vec->lower
4vec->s4vec
4vec->upper
4vec-<
4vec-<<=
4vec-1mask
4vec-1x
4vec-1z
4vec-==
4vec-===
4vec-===*
4vec-?
4vec-?!
4vec-?*
4vec-bit-extract
4vec-bit-index
4vec-bit?
4vec-bit?!
4vec-bitand
4vec-bitmux
4vec-bitnot
4vec-bitor
4vec-bitxor
4vec-boolmaskp
4vec-clog2
4vec-concat
4vec-countones
4vec-equiv
4vec-examples
4vec-fix
4vec-from-bitlist
4vec-idx->4v
4vec-index-p
4vec-lsh
4vec-mask
4vec-mask-to-zero
4vec-mask?
4vec-minus
4vec-monotonicity
4vec-offset
4vec-onehot
4vec-onehot0
4vec-onset
4vec-operations
4vec-override
4vec-p
4vec-p-to-stringp
4vec-p-to-stringp-aux
4vec-parity
4vec-part-install
4vec-part-select
4vec-plus
4vec-pow
4vec-quotient
4vec-reduction-and
4vec-reduction-or
4vec-remainder
4vec-replace-range
4vec-res
4vec-resand
4vec-resor
4vec-rev-blocks
4vec-rsh
4vec-shift-core
4vec-sign-ext
4vec-symwildeq
4vec-times
4vec-to-bitwise-chars
4vec-to-hex-char
4vec-to-hex-chars
4vec-to-svex
4vec-to-svex-lst
4vec-to-xml-chars
4vec-uminus
4vec-wildeq
4vec-wildeq-safe
4vec-x
4vec-xdet
4vec-xfree-p
4vec-xfree-p-basics
4vec-z
4vec-zero-ext
4vecarr
4veclist
4veclist-<<=
4veclist-equiv
4veclist-fix
4veclist-from-bitlist
4veclist-from-bitlist-log-rec
4veclist-mask
4veclist-mask?
4veclist-nth-safe
4veclist-p
4veclist-p-basics
4veclist-p-to-stringp
4veclist-quote
4veclistlist
4veclistlist-equiv
4veclistlist-fix
4veclistlist-p
4veclistlist-p-basics
4vecs-length
4vmask
4vmask-acons
4vmask-alist
4vmask-alist-equiv
4vmask-alist-fix
4vmask-alist-p
4vmask-all-or-none
4vmask-assoc
4vmask-empty
4vmask-equiv
4vmask-fix
4vmask-p
4vmask-subsumes
4vmask-to-a4vec
4vmask-to-a4vec-env
4vmask-to-a4vec-rec
4vmask-to-a4vec-rec-env
4vmask-to-a4vec-varcount
4vmask-union
4vmasklist
4vmasklist-equiv
4vmasklist-fix
4vmasklist-len-fix
4vmasklist-p
4vmasklist-p-basics
4vmasklist-subsumes
4vp
4vs-and
4vs-and-dumb
4vs-and-list
4vs-and-list-dumb
4vs-and-lists
4vs-buf
4vs-constructors
4vs-f
4vs-iff
4vs-iff-lists
4vs-implies
4vs-implies-lists
4vs-ite*-dumb
4vs-ite*-list-dumb
4vs-not
4vs-not-list
4vs-onehot
4vs-or
4vs-or-list
4vs-or-lists
4vs-t
4vs-x
4vs-xor
4vs-xor-lists
4vs-z
4vs-zif-dumb
5. Using def-gl-thm
54bits
54bits-fix
54bits-p
5bits
5bits-fix
5bits-p
6. Writing :g-bindings forms
60-bit-fix
60bits-0-3
60bits-0-59
60bits-0-7
64-bit-compute-mandatory-prefix-for-0f-38-three-byte-opcode
64-bit-compute-mandatory-prefix-for-0f-3a-three-byte-opcode
64-bit-compute-mandatory-prefix-for-two-byte-opcode
64-bit-mode-0f-38-three-byte-opcode-modr/m-p
64-bit-mode-0f-3a-three-byte-opcode-modr/m-p
64-bit-mode-one-byte-opcode-modr/m-p
64-bit-mode-two-byte-opcode-modr/m-p
64-bit-modep
64bits
64bits-fix
64bits-p
6bits
6bits-fix
6bits-p
7. Proving Coverage
7bits
7bits-fix
7bits-p
8. Exercises
8bitbytes-hexchars-conversions
8bitbytes-hexstrings-conversions
8bits
8bits-fix
8bits-p
=
=/_
=/_-fn
=_
=_-fn
?_
?_-fn
@
@$$
@''
@[]
@``
@body
@call
@csee
@csym
@def
@formals
@gdef
@measure
@see
@see?
@srclink
@sym
@tsee
@url
@{}
A
A Flying Tour of ACL2
A Sketch of How the Rewriter Works
A Tiny Warning Sign
A Trivial Proof
A Typical State
A Walking Tour of ACL2
A!
A2vec-p
A3vec-==
A3vec-?
A3vec-?*
A3vec-bit?
A3vec-bitand
A3vec-bitnot
A3vec-bitor
A3vec-bitxor
A3vec-fix
A3vec-reduction-and
A3vec-reduction-or
A4vec
A4vec->aiglist
A4vec->lower
A4vec->upper
A4vec-<
A4vec-0
A4vec-1x
A4vec-===
A4vec-===*
A4vec-===*-aux
A4vec-===*-bit
A4vec-?!
A4vec-bit-extract
A4vec-bit?!
A4vec-clog2
A4vec-concat
A4vec-constantp
A4vec-countones
A4vec-equiv
A4vec-eval
A4vec-fix
A4vec-ite
A4vec-ite-fn
A4vec-lsh
A4vec-mask
A4vec-mask-check
A4vec-minus
A4vec-offset
A4vec-onehot
A4vec-onehot0
A4vec-onset
A4vec-operations
A4vec-override
A4vec-p
A4vec-parity
A4vec-part-install
A4vec-part-select
A4vec-plus
A4vec-pow
A4vec-quotient
A4vec-remainder
A4vec-res
A4vec-resand
A4vec-resor
A4vec-rev-blocks
A4vec-rsh
A4vec-sign-ext
A4vec-symwildeq
A4vec-syntactic-3vec-p
A4vec-syntactic-3vec-p-rec
A4vec-times
A4vec-uminus
A4vec-wildeq
A4vec-wildeq-aux
A4vec-wildeq-bit
A4vec-wildeq-safe
A4vec-wildeq-safe-aux
A4vec-wildeq-safe-bit
A4vec-x
A4vec-xdet
A4vec-zero-ext
A4vec/svex-env-eval
A4veclist
A4veclist->aiglist
A4veclist-equiv
A4veclist-eval
A4veclist-eval-gl
A4veclist-fix
A4veclist-length
A4veclist-nth
A4veclist-p
A4veclist-p-basics
A4veclist/env-list-eval
A4veclist/svex-env-list-eval
A4veclistlist
A4veclistlist-equiv
A4veclistlist-fix
A4veclistlist-p
A4veclistlist-p-basics
ACL2
ACL2 Characters
ACL2 Conses or Ordered Pairs
ACL2 Strings
ACL2 Symbols
ACL2 System Architecture
ACL2 as an Interactive Theorem Prover
ACL2 as an Interactive Theorem Prover (cont)
ACL2 is an Untyped Language
ACL2-as-standalone-program
ACL2-built-ins
ACL2-count
ACL2-customization
ACL2-defaults-table
ACL2-doc
ACL2-doc-summary
ACL2-help
ACL2-number-list
ACL2-number-list-equiv
ACL2-number-list-fix
ACL2-number-listp
ACL2-number-listp-basics
ACL2-numberp
ACL2-numberp-algebra
ACL2-pc::=
ACL2-pc::ACL2-wrap
ACL2-pc::add-abbreviation
ACL2-pc::al
ACL2-pc::apply-linear
ACL2-pc::bash
ACL2-pc::bdd
ACL2-pc::bk
ACL2-pc::bookmark
ACL2-pc::by
ACL2-pc::casesplit
ACL2-pc::cg
ACL2-pc::cg-or-skip
ACL2-pc::change-goal
ACL2-pc::cl-proc
ACL2-pc::claim
ACL2-pc::claim-simple
ACL2-pc::clause-processor
ACL2-pc::comm
ACL2-pc::commands
ACL2-pc::comment
ACL2-pc::contradict
ACL2-pc::contrapose
ACL2-pc::demote
ACL2-pc::dive
ACL2-pc::do-all
ACL2-pc::do-all-no-prompt
ACL2-pc::do-strict
ACL2-pc::doc
ACL2-pc::drop
ACL2-pc::drop-or-skip
ACL2-pc::dv
ACL2-pc::elim
ACL2-pc::equiv
ACL2-pc::ex
ACL2-pc::exit
ACL2-pc::expand
ACL2-pc::fail
ACL2-pc::fancy-use
ACL2-pc::finish
ACL2-pc::forwardchain
ACL2-pc::free
ACL2-pc::geneqv
ACL2-pc::generalize
ACL2-pc::goals
ACL2-pc::help
ACL2-pc::hyps
ACL2-pc::illegal
ACL2-pc::in-theory
ACL2-pc::induct
ACL2-pc::insist-all-proved
ACL2-pc::instantiate
ACL2-pc::lemmas-used
ACL2-pc::lisp
ACL2-pc::negate
ACL2-pc::nil
ACL2-pc::noise
ACL2-pc::noise!
ACL2-pc::nx
ACL2-pc::orelse
ACL2-pc::p
ACL2-pc::p-top
ACL2-pc::pl
ACL2-pc::pot-lst
ACL2-pc::pp
ACL2-pc::pr
ACL2-pc::print
ACL2-pc::print-all-concs
ACL2-pc::print-all-goals
ACL2-pc::print-main
ACL2-pc::pro
ACL2-pc::pro-or-skip
ACL2-pc::promote
ACL2-pc::protect
ACL2-pc::prove
ACL2-pc::prove-guard
ACL2-pc::prove-termination
ACL2-pc::pso
ACL2-pc::pso!
ACL2-pc::psog
ACL2-pc::put
ACL2-pc::quiet
ACL2-pc::quiet!
ACL2-pc::r
ACL2-pc::reduce
ACL2-pc::reduce-by-induction
ACL2-pc::remove-abbreviations
ACL2-pc::repeat
ACL2-pc::repeat-rec
ACL2-pc::repeat-until-done
ACL2-pc::replay
ACL2-pc::restore
ACL2-pc::retain
ACL2-pc::retain-or-skip
ACL2-pc::retrieve
ACL2-pc::rewrite
ACL2-pc::run-instr-on-goal
ACL2-pc::run-instr-on-new-goals
ACL2-pc::runes
ACL2-pc::s
ACL2-pc::s-prop
ACL2-pc::save
ACL2-pc::sequence
ACL2-pc::show-abbreviations
ACL2-pc::show-linears
ACL2-pc::show-rewrites
ACL2-pc::show-type-prescriptions
ACL2-pc::skip
ACL2-pc::sl
ACL2-pc::sls
ACL2-pc::split
ACL2-pc::split-in-theory
ACL2-pc::sr
ACL2-pc::st
ACL2-pc::succeed
ACL2-pc::th
ACL2-pc::then
ACL2-pc::top
ACL2-pc::type-alist
ACL2-pc::undo
ACL2-pc::unsave
ACL2-pc::up
ACL2-pc::use
ACL2-pc::when-not-proved
ACL2-pc::wrap
ACL2-pc::wrap-induct
ACL2-pc::wrap1
ACL2-pc::x
ACL2-pc::x-dumb
ACL2-programming-language
ACL2-sedan
ACL2-system-feature-dependencies
ACL2-tutorial
ACL2-unwind-protect
ACL2-user
ACL2::always-equal
ACL2::counter-example-generation
ACL2::patbind-ret
ACL2::patbind-stobj-get
ACL2::retroactive-add-aignet-preservation-thm
ACL2::retroactive-add-aignet-preservation-thm-local
ACL2::return-last-blockers
ACL2p-key-checkpoints
ACL2s
ACL2s-command-classifications
ACL2s-defaults
ACL2s-faq
ACL2s-implementation-notes
ACL2s-installation
ACL2s-installation-faq
ACL2s-installation-linux
ACL2s-installation-macos
ACL2s-installation-windows
ACL2s-intro
ACL2s-tutorial
ACL2s-user-guide
ACL2s-utilities
ACL2x
ACL2xskip
ARM AArch32 Floating-Point Instructions
Aabf-<-=-ss
Aabf-<-ss
Aabf-*-ss
Aabf-+-ss
Aabf-=-ss
Aabf-abs-s
Aabf-ash-ss
Aabf-car
Aabf-expt-su
Aabf-first/rest/end
Aabf-floor-ss
Aabf-floor-ss-aux
Aabf-integer-length-bound-s
Aabf-integer-length-s
Aabf-integer-length-s1
Aabf-ite-bss-fn
Aabf-ite-bss-fn-aux
Aabf-ite-buu-fn
Aabf-ite-buu-fn-aux
Aabf-logand-ss
Aabf-logapp-nss
Aabf-logapp-nss-aux
Aabf-logapp-russ
Aabf-logbitp-n2v
Aabf-logeqv-ss
Aabf-logext-ns
Aabf-loghead-ns
Aabf-logior-ss
Aabf-lognot-s
Aabf-logtail-ns
Aabf-logxor-ss
Aabf-mod-ss
Aabf-mod-ss-aux
Aabf-rem-ss
Aabf-scons
Aabf-sign-abs-not-s
Aabf-sign-s
Aabf-signext-nss
Aabf-syntactically-false-p
Aabf-syntactically-neg1-p
Aabf-syntactically-signext-p
Aabf-syntactically-true-p
Aabf-syntactically-zero-p
Aabf-truncate-ss
Aabf-ucons
Aabf-unary-minus-s
Abc-comb-simp-config
Abc-comb-simp-config->quiet
Abc-comb-simp-config->script
Abc-comb-simp-config-equiv
Abc-comb-simp-config-fix
Abc-comb-simp-config-p
Abc-comb-simplify
Abc-comb-simplify!
Abc-example-scripts
Abnf
Abnf-tree-list-with-root-p
Abnf-tree-list-with-root-p
Abnf-tree-list-with-root-p-basics
Abnf-tree-list-with-root-p-basics
Abnf-tree-with-root-p
Abnf-tree-with-root-p
Abnf-tree-wrap
Abnf-tree-wrap-fn
Abort!
Abort-rewrite
Abort-soft
About Models
About Types
About the ACL2 Home Page
About the Admission of Recursive Definitions
About the Prompt
About-ACL2
Abs
Abs-diff
Abs-hex-digit
Abs-raw-input-character
Abs-unicode-escape
Abs-unicode-input-character
Abs-unicode-input-character-list
Abstract-*-alpha/digit/dash
Abstract-*-dot-1*bit
Abstract-*-dot-1*digit
Abstract-*-dot-1*hexdig
Abstract-*-grouped-terminal
Abstract-*-rule-/-*cwsp-cnl
Abstract-*bit
Abstract-*digit
Abstract-*digit-star-*digit
Abstract-*hexdig
Abstract-?repeat
Abstract-alpha
Abstract-alpha/digit/dash
Abstract-alt-rest
Abstract-alt-rest-comp
Abstract-alternation
Abstract-bin-val
Abstract-bin-val-rest
Abstract-bin/dec/hex-val
Abstract-bin/dec/hex-val-rest-dot-p
Abstract-bit
Abstract-case-insensitive-string
Abstract-case-sensitive-string
Abstract-char-val
Abstract-conc-rest
Abstract-conc-rest-comp
Abstract-concatenation
Abstract-dec-val
Abstract-dec-val-rest
Abstract-defined-as
Abstract-digit
Abstract-dot/dash-1*bit
Abstract-dot/dash-1*digit
Abstract-dot/dash-1*hexdig
Abstract-element
Abstract-elements
Abstract-fail
Abstract-group/option
Abstract-grouped-terminal
Abstract-grouped-terminals
Abstract-hex-val
Abstract-hex-val-rest
Abstract-hexdig
Abstract-hids
Abstract-num-val
Abstract-prose-val
Abstract-quoted-string
Abstract-repeat
Abstract-repetition
Abstract-rule
Abstract-rule-/-*cwsp-cnl
Abstract-rulelist
Abstract-rulename
Abstract-stobj
Abstract-syntax
Abstract-syntax
Abstract-syntax
Abstract-syntax
Abstract-syntax
Abstract-syntax
Abstract-syntax
Abstract-syntax-induction-schemas
Abstract-syntax-operations
Abstract-syntax-operations
Abstract-syntax-operations
Abstract-terminal
Abstract-terminals
Access
Accessed-bit
Accessing-printed-output
Accessing-printed-output
Accumulated-persistence
Accumulated-persistence-oops
Accumulated-persistence-subtleties
Acknowledgments
Acons
Acre
Acre-internals
Active-or-non-runep
Active-runep
Adc-af-spec16
Adc-af-spec32
Adc-af-spec64
Adc-af-spec8
Add-af-spec16
Add-af-spec32
Add-af-spec64
Add-af-spec8
Add-aignet-preservation-thm
Add-arithmetic-values
Add-binop
Add-const-to-untranslate-preprocess
Add-custom-keyword-hint
Add-default-hints
Add-default-hints!
Add-dive-into-macro
Add-fgl-binder-meta
Add-fgl-branch-merge
Add-fgl-branch-merges
Add-fgl-brewrite
Add-fgl-brewrites
Add-fgl-meta
Add-fgl-primitive
Add-fgl-rewrite
Add-fgl-rewrites
Add-frame
Add-fun-to-fun-renaming
Add-funs
Add-funs-of-dead
Add-funs-to-fun-renaming
Add-funtypes
Add-hypo-cp
Add-include-book-dir
Add-include-book-dir!
Add-integer-values
Add-invisible-fns
Add-io-pair
Add-io-pairs
Add-io-pairs-details
Add-ld-keyword-alias
Add-ld-keyword-alias!
Add-macro-alias
Add-macro-fn
Add-match-free-override
Add-meta-rule
Add-nth-alias
Add-numbered-name-in-use
Add-override-hints
Add-override-hints!
Add-pdp-entry
Add-pml4-entry
Add-resource-directory
Add-rp-rule
Add-sat-lits-preservation-thm
Add-schar-schar
Add-schar-schar-okp
Add-schar-sint
Add-schar-sint-okp
Add-schar-sllong
Add-schar-sllong-okp
Add-schar-slong
Add-schar-slong-okp
Add-schar-sshort
Add-schar-sshort-okp
Add-schar-uchar
Add-schar-uchar-okp
Add-schar-uint
Add-schar-ullong
Add-schar-ulong
Add-schar-ushort
Add-schar-ushort-okp
Add-sint-schar
Add-sint-schar-okp
Add-sint-sint
Add-sint-sint-okp
Add-sint-sllong
Add-sint-sllong-okp
Add-sint-slong
Add-sint-slong-okp
Add-sint-sshort
Add-sint-sshort-okp
Add-sint-uchar
Add-sint-uchar-okp
Add-sint-uint
Add-sint-ullong
Add-sint-ulong
Add-sint-ushort
Add-sint-ushort-okp
Add-sllong-schar
Add-sllong-schar-okp
Add-sllong-sint
Add-sllong-sint-okp
Add-sllong-sllong
Add-sllong-sllong-okp
Add-sllong-slong
Add-sllong-slong-okp
Add-sllong-sshort
Add-sllong-sshort-okp
Add-sllong-uchar
Add-sllong-uchar-okp
Add-sllong-uint
Add-sllong-uint-okp
Add-sllong-ullong
Add-sllong-ulong
Add-sllong-ushort
Add-sllong-ushort-okp
Add-slong-schar
Add-slong-schar-okp
Add-slong-sint
Add-slong-sint-okp
Add-slong-sllong
Add-slong-sllong-okp
Add-slong-slong
Add-slong-slong-okp
Add-slong-sshort
Add-slong-sshort-okp
Add-slong-uchar
Add-slong-uchar-okp
Add-slong-uint
Add-slong-uint-okp
Add-slong-ullong
Add-slong-ulong
Add-slong-ushort
Add-slong-ushort-okp
Add-sshort-schar
Add-sshort-schar-okp
Add-sshort-sint
Add-sshort-sint-okp
Add-sshort-sllong
Add-sshort-sllong-okp
Add-sshort-slong
Add-sshort-slong-okp
Add-sshort-sshort
Add-sshort-sshort-okp
Add-sshort-uchar
Add-sshort-uchar-okp
Add-sshort-uint
Add-sshort-ullong
Add-sshort-ulong
Add-sshort-ushort
Add-sshort-ushort-okp
Add-stobj-preservation-thm
Add-suffix
Add-suffix-lst
Add-suffix-to-fn
Add-suffix-to-fn-lst
Add-suffix-to-fn-or-const
Add-suffix-to-fn-or-const-lst
Add-to-*ip
Add-to-*sp
Add-to-each
Add-to-ruleset
Add-to-set
Add-to-set-eq
Add-to-set-eql
Add-to-set-equal
Add-to-set-equal-theorems
Add-uchar-schar
Add-uchar-schar-okp
Add-uchar-sint
Add-uchar-sint-okp
Add-uchar-sllong
Add-uchar-sllong-okp
Add-uchar-slong
Add-uchar-slong-okp
Add-uchar-sshort
Add-uchar-sshort-okp
Add-uchar-uchar
Add-uchar-uchar-okp
Add-uchar-uint
Add-uchar-ullong
Add-uchar-ulong
Add-uchar-ushort
Add-uchar-ushort-okp
Add-uint-schar
Add-uint-sint
Add-uint-sllong
Add-uint-sllong-okp
Add-uint-slong
Add-uint-slong-okp
Add-uint-sshort
Add-uint-uchar
Add-uint-uint
Add-uint-ullong
Add-uint-ulong
Add-uint-ushort
Add-ullong-schar
Add-ullong-sint
Add-ullong-sllong
Add-ullong-slong
Add-ullong-sshort
Add-ullong-uchar
Add-ullong-uint
Add-ullong-ullong
Add-ullong-ulong
Add-ullong-ushort
Add-ulong-schar
Add-ulong-sint
Add-ulong-sllong
Add-ulong-slong
Add-ulong-sshort
Add-ulong-uchar
Add-ulong-uint
Add-ulong-ullong
Add-ulong-ulong
Add-ulong-ushort
Add-untranslate-pattern
Add-ushort-schar
Add-ushort-schar-okp
Add-ushort-sint
Add-ushort-sint-okp
Add-ushort-sllong
Add-ushort-sllong-okp
Add-ushort-slong
Add-ushort-slong-okp
Add-ushort-sshort
Add-ushort-sshort-okp
Add-ushort-uchar
Add-ushort-uchar-okp
Add-ushort-uint
Add-ushort-ullong
Add-ushort-ulong
Add-ushort-ushort
Add-ushort-ushort-okp
Add-values
Add-var
Add-var
Add-var-to-var-renaming
Add-var-value
Add-var/vars-not-error-when-add-var/vars-to-var-renaming
Add-var/vars-value/values-when-renamevar
Add-vars
Add-vars-to-var-renaming
Add-vars-values
Adding-z-drivers
Addinstnames
Addition
Addnames
Addnames-indices
Addnames-indices->blockstmt-idx
Addnames-indices->gateinst-idx
Addnames-indices->genblk-idx
Addnames-indices->modinst-idx
Addnames-indices-equiv
Addnames-indices-fix
Addnames-indices-p
Addr-range
Addr-scope
Addr-scope-equiv
Addr-scope-fix
Addr-scope-p
Address
Address
Address->index
Address->number
Address->path
Address->scope
Address->svar
Address-aligned-p
Address-alist
Address-alist-equiv
Address-alist-fix
Address-alist-p
Address-equiv
Address-equiv
Address-fix
Address-fix
Address-p
Address-p
Addresses
Addressing-method-code-p
Addresslist
Addresslist-equiv
Addresslist-fix
Addresslist-p
Addresslist-p-basics
Addressp
Adjacent-p
Adjust-ld-history
Adjust-type
Adjust-type-list
Advanced-equivalence-checking-with-fgl
Advanced-features
Adviser
Aes-128-cbc-pkcs7-interface
Aes-128-interface
Aes-192-cbc-pkcs7-interface
Aes-192-interface
Aes-256-cbc-pkcs7-interface
Aes-256-interface
Aeval
Aexp
Aexp-add
Aexp-add->left
Aexp-add->right
Aexp-case
Aexp-const
Aexp-const->value
Aexp-count
Aexp-equiv
Aexp-fix
Aexp-kind
Aexp-mul
Aexp-mul->left
Aexp-mul->right
Aexp-var
Aexp-var->name
Aexpp
Ahref
Aig
Aig-alist-equiv
Aig-alist-lookup
Aig-and
Aig-and-count
Aig-and-dumb
Aig-and-list
Aig-and-list-aux
Aig-and-lists
Aig-and-macro-exec-part
Aig-and-macro-logic-part
Aig-and-main
Aig-and-pass1
Aig-and-pass2
Aig-and-pass2a
Aig-and-pass3
Aig-and-pass4
Aig-and-pass4a
Aig-and-pass5
Aig-and-pass6
Aig-and-pass6a
Aig-andc1
Aig-andc1-lists
Aig-andc2
Aig-andc2-lists
Aig-binary-and
Aig-binary-or
Aig-cases
Aig-collect-andnode-labels
Aig-collect-labels
Aig-compose
Aig-compose-alist
Aig-compose-alist-thms
Aig-compose-alists
Aig-compose-list
Aig-compose-thms
Aig-constructors
Aig-count-andnode-labels
Aig-count-labels
Aig-countones-aux
Aig-env-equiv
Aig-env-lookup
Aig-env-lookup-missing-action
Aig-env-lookup-missing-output
Aig-equiv
Aig-eval
Aig-eval-alist
Aig-eval-alist-thms
Aig-eval-alists
Aig-eval-list
Aig-eval-thms
Aig-force-sign-s
Aig-from-bed
Aig-head-of-concat
Aig-head-tail-concat-aux
Aig-iff
Aig-iff-lists
Aig-implies
Aig-implies-fn
Aig-implies-lists
Aig-iszero-s
Aig-ite
Aig-ite-fn
Aig-label-nodes
Aig-list->s
Aig-list->s-lower-bound
Aig-list->s-upper-bound
Aig-list->u
Aig-list-best
Aig-list-best-aux
Aig-list-best-aux1
Aig-list-label-nodes
Aig-list-list-best
Aig-list-list-best-aux
Aig-list-list-label-nodes
Aig-logcollapse-ns
Aig-mode-or-p-true
Aig-nand
Aig-nand-lists
Aig-negation-p
Aig-nor
Aig-nor-lists
Aig-not
Aig-not-list
Aig-onehot-aux
Aig-or
Aig-or-list
Aig-or-list-aux
Aig-or-lists
Aig-or-macro-exec-part
Aig-or-macro-logic-part
Aig-orc1
Aig-orc1-lists
Aig-orc2
Aig-orc2-lists
Aig-other
Aig-overlap-width-ss
Aig-overlap-width-ss-aux
Aig-parity-s
Aig-partial-eval
Aig-partial-eval-alist
Aig-partial-eval-alist-thms
Aig-partial-eval-list
Aig-partial-eval-thms
Aig-print
Aig-random-sim
Aig-restrict
Aig-restrict-alist
Aig-restrict-alist-thms
Aig-restrict-alists
Aig-restrict-list
Aig-restrict-thms
Aig-rev-blocks-nns
Aig-rev-blocks-nss
Aig-rev-blocks-sss
Aig-right-shift-ss
Aig-sat
Aig-scons-with-hint
Aig-semantics
Aig-sterm-with-hint
Aig-substitution
Aig-symbolic-arithmetic
Aig-translation
Aig-var-fix
Aig-varlist
Aig-varlist-equiv
Aig-varlist-fix
Aig-varlist-p
Aig-varlist-p-basics
Aig-vars
Aig-vars-1pass
Aig-vars-fast
Aig-vars-thms
Aig-vecsim60
Aig-xor
Aig-xor-lists
Aig2c
Aig2c-boolean-sanity-check-p
Aig2c-compile
Aig2c-config
Aig2c-config->op-and
Aig2c-config->op-not
Aig2c-config->prefix
Aig2c-config->type
Aig2c-config-p
Aig2c-epilogue
Aig2c-main
Aig2c-main-list
Aig2c-maketemps
Aig2c-maketemps-list
Aig2c-prologue
Aiger-read
Aiger-write
Aignet
Aignet-abc
Aignet-abc-interface
Aignet-add-and
Aignet-add-in
Aignet-add-out
Aignet-add-reg
Aignet-add-xor
Aignet-balance-build-supergate
Aignet-balance-build-supergate-rec
Aignet-balance-build-superxor
Aignet-balance-build-superxor-rec
Aignet-balance-find-pairing
Aignet-balance-find-pairing-rec
Aignet-balance-find-xor-pairing
Aignet-balance-find-xor-pairing-rec
Aignet-balance-nxsts
Aignet-balance-outs
Aignet-build
Aignet-build-wide-and
Aignet-case
Aignet-clear
Aignet-cnf
Aignet-comb-transforms
Aignet-complete-copy
Aignet-constprop-stats
Aignet-constprop-sweep
Aignet-constprop-sweep-invar
Aignet-construction
Aignet-copy-init
Aignet-eval
Aignet-extension-bind-inverse
Aignet-extension-binding
Aignet-extension-p
Aignet-fanins
Aignet-get-ipasir-ctrex-invals
Aignet-get-ipasir-ctrex-regvals
Aignet-hash-and
Aignet-hash-iff
Aignet-hash-mux
Aignet-hash-or
Aignet-hash-xor
Aignet-id-fix
Aignet-idp
Aignet-impl
Aignet-init
Aignet-ipasir
Aignet-lit->bfr
Aignet-lit->cnf
Aignet-lit->ipasir
Aignet-lit-constprop
Aignet-lit-constprop-init-and-sweep
Aignet-lit-fix
Aignet-lit-ipasir-sat-minimize
Aignet-litp
Aignet-lits-ipasir-sat-check
Aignet-lits-ipasir-sat-minimize
Aignet-m-assumption-n-output-transforms
Aignet-maybe-update-refs
Aignet-n-output-comb-transforms
Aignet-nodes-ok
Aignet-norm
Aignet-norm-p
Aignet-nxsts
Aignet-nxsts-aux
Aignet-outputs
Aignet-outputs-aux
Aignet-read-aiger
Aignet-record-levels
Aignet-rollback
Aignet-run-abc-core
Aignet-run-abc-core-st
Aignet-set-nxst
Aignet-simplify-marked
Aignet-simplify-marked-with-tracking
Aignet-simplify-with-tracking
Aignet-transforms
Aignet-update-node-level
Aignet-vals->in/regvals
Aignet-vals->regvals-after-invals
Aignet-vals-sat-care-masks-lits
Aignet-vals-sat-care-masks-rec
Aignet-vecsim
Aignet-vecsim-top
Aignet-vecsim1
Aignet-write-aiger
Aigs-length
Aigtrans
Aij
Aij-atj-paper
Aij-class-names
Aij-class-types
Aij-nativep
Aij-notions
Al->pat
Algebra
Algebraic Properties
Alias
Alias->name
Alias->val
Alias-alist
Alias-alist-equiv
Alias-alist-fix
Alias-alist-p
Alias-equiv
Alias-fix
Alias-lst
Alias-lst-equiv
Alias-lst-fix
Alias-lst-p
Alias-lst-p-basics
Alias-norm.lisp
Alias-normalization
Alias-p
Aliases-add-pair
Aliases-bound-fix
Aliases-bound-fix-aux
Aliases-boundedp-aux
Aliases-empty
Aliases-finish-canonicalize
Aliases-fix
Aliases-indexed->named
Aliases-indexed->named-aux
Aliases-normorderedp
Aliases-normorderedp-aux
Aliases-put-pairs
Aliases-to-var-decl-map
Aliases-to-var-decl-map-aux
Aliases-vars
Aliases-vars-aux
Align-let-vars-values
Align-let-vars-values-aux
Alignment-checking-enabled-p
Alist-collect-compositions
Alist-equiv
Alist-equiv-bad-guy
Alist-fix
Alist-keys
Alist-keys-subsetp
Alist-map-keys
Alist-map-keys-functions-and-macros
Alist-map-keys-theorems
Alist-map-vals
Alist-map-vals-functions-and-macros
Alist-map-vals-theorems
Alist-to-doublets
Alist-vals
Alist-values-are-sets-p
Alistp
Alists
Alists-agree
All-attachments
All-by-membership
All-calls
All-equalp
All-equalp-of-vl-emodwirelist->basenames
All-fnnames
All-fnnames-lst
All-fnnames1
All-free/bound-vars
All-free/bound-vars-lst
All-have-len
All-have-len
All-head-to-head-competition-loser-p
All-keys
All-lambdas
All-lambdas-lst
All-logic-fns
All-mem-except-paging-structures-equal
All-mem-except-paging-structures-equal-aux
All-nil
All-non-gv-exec-ffn-symbs
All-non-gv-ffn-symbs
All-non-gv-ffn-symbs-lst
All-pkg-names
All-pkg-names-lst
All-program-ffn-symbs
All-program-ffn-symbs-lst
All-program-fns
All-true-listp
All-valid-key-paths-p
All-vars
All-vars-in-untranslated-term
All-vars-open
All-vars-open-lst
All-xlation-governing-entries-paddrs
Allexprs
Allexprs
Allocate-fixnum-range
Allow-real-oracle-eval
Alpha-char-p
Alphanum-<
Alphanum-obj-<
Alphanum-sort
Alphorder
Alt/conc/rep/elem
Alternate-definitions
Alternation
Alternation-called-rules
Alternation-equiv
Alternation-fix
Alternation-in-termset-p
Alternation-in-termset-p-basics
Alternation-rename-rule
Alternation-unambiguousp
Alternation-unambiguousp-of-cons-when-disjointp
Alternation-wfp
Alternationp
Alternationp-basics
Alternative
Alternative->name
Alternative->product
Alternative-equiv
Alternative-fix
Alternative-introduction
Alternative-list
Alternative-list->name-list
Alternative-list-equiv
Alternative-list-fix
Alternative-listp
Alternative-listp-basics
Alternative-spec-listp
Alternative-spec-listp-basics
Alternativep
Alu-test-vector
Always$
Always$+
Always-top
Ambiguity
An Example Common Lisp Function Definition
An Example of ACL2 in Use
Analyzing Common Lisp Models
And
And*
And-node
And-node->fanin0
And-node->fanin1
And4
Annotate
Annotate
Annotated-ACL2-scripts
Ansfl
Ansi-only
Any-inst-needs-modr/m-p
Any-p
Any-present-in
Any-table
Any-table-equiv
Any-table-fix
Any-table-p
Any-trace
Any-trace-equiv
Any-trace-fix
Any-trace-p
Any-trace-p-basics
Anyp
Anyp
Apconvert-expr-value
Apconvert-type
Apconvert-type-list
App-view
App-view-proof-utilities
Append
Append$
Append$+
Append-alist-keys
Append-alist-keys-exec
Append-alist-vals
Append-alist-vals-exec
Append-chars
Append-n
Append-theorems
Append-without-guard
Apply$
Apply$-guard
Apply$-lambda
Apply$-lambda-guard
Apply$-userfn
Apply-comb-transform
Apply-comb-transform!
Apply-comb-transform-default
Apply-comb-transforms
Apply-comb-transforms!
Apply-fn-if-known
Apply-fn-into-ifs
Apply-m-assumption-n-output-output-transform-default
Apply-m-assumption-n-output-transform
Apply-m-assumption-n-output-transform!
Apply-m-assumption-n-output-transforms
Apply-m-assumption-n-output-transforms!
Apply-n-output-comb-transform
Apply-n-output-comb-transform!
Apply-n-output-comb-transform-default
Apply-n-output-comb-transforms
Apply-n-output-comb-transforms!
Apply-term
Apply-term*
Apply-terms-same-args
Apply-unary-to-terms
Apropos
Apt
Architecture-of-the-prover
Archive-matching-topics
Archive-xdoc
Aref1
Aref2
Arglistp
Argresolve
Argresolve
Args
Args-without-defaults
Argument-lst-syntax
Argument-lst-syntax-fix
Argument-lst-syntax-p
Argument-partitioning
Argument-syntax-fix
Argument-syntax-p
Argv
Arith-compare-check
Arith-equivs
Arithmetic
Arithmetic-1
Arithmetic-2
Arithmetic-3
Arithmetic-5
Arithmetic-light
Arithmetic-operations
Arithmetic/nat-listp
Arithmetic/natp-posp
Arithmetic/rational-listp
Arities-okp
Arity
Arity+
Arity-reasoning
Array
Array-fieldinfo
Array-fieldinfo->size-key
Array-fieldinfo->tr-key
Array-fieldinfo-p
Array-operations
Array-tau-rules
Array-type
Array-type-case
Array-type-class
Array-type-class->dimensions
Array-type-class->element
Array-type-count
Array-type-equiv
Array-type-fix
Array-type-kind
Array-type-primitive
Array-type-primitive->dimensions
Array-type-primitive->element
Array-type-variable
Array-type-variable->dimensions
Array-type-variable->element
Array-typep
Array-value-disjoint-rules
Array-value-rules
Array1
Array1-disabled-lemmas
Array1-functions
Array1-lemmas
Array1p
Array2p
Arrays
Arrays-example
Ascii
Ascii-basic-exec-char
Ascii-basic-exec-char-fix
Ascii-basic-exec-charp
Ascii-basic-source-char
Ascii-basic-source-char-fix
Ascii-basic-source-charp
Ascii-fix
Ascii-identifier-ignore-p
Ascii-identifier-part-p
Ascii-identifier-start-p
Ascii-list
Ascii-list-equiv
Ascii-list-fix
Ascii-listp
Ascii-listp-basics
Ascii-to-exec-char-number
Ascii-to-source-char-number
Ascii=>string
Asciip
Aset1
Aset1-trusted
Aset2
Ash
Ash*
Ash-defaults
Ashu
Ashu-basics
Ashu-guard
Assert!
Assert!-stobj
Assert$
Assert*
Assert-equal
Assert-event
Assert-no-special-raw-definition
Assert-program-mode
Assert-sat
Assert-unsat
Assert?
Assertion
Assertion->asg
Assertion->constr
Assertion-equiv
Assertion-fix
Assertion-list
Assertion-list->asg-list
Assertion-list->constr-list
Assertion-list-equiv
Assertion-list-fix
Assertion-list-from
Assertion-listp
Assertion-listp-basics
Assertionp
Assertions
Assign
Assign
Assign->netassigns
Assign1
Assign2
Assign3
Assign4
Assign5
Assign6
Assign7
Assign8
Assign9
Assignment
Assignment-equiv
Assignment-fix
Assignment-list
Assignment-list-equiv
Assignment-list-fix
Assignment-listp
Assignment-listp-basics
Assignment-wfp
Assignmentp
Assigns
Assigns->absindexed
Assigns->netassigns
Assigns->netassigns-aux
Assigns-addr-p
Assigns-check-masks
Assigns-compose
Assigns-equiv
Assigns-fix
Assigns-named->indexed
Assigns-p
Assigns-subst
Assigns-subst-nrev
Assigns-to-overrides
Assigns-to-overrides-nrev
Assigns-vars
Assoc
Assoc-eq
Assoc-equal
Assoc-keyword
Assoc-pat->al
Assoc-string-equal
Assocs
Assume
Assume-true-false-aggressive-p
Atc
Atc-abstract-syntax
Atc-add-var
Atc-adjust-type-rules
Atc-affecting-term-for-let-p
Atc-apconvert-rules
Atc-array-length-rules
Atc-array-length-write-rules
Atc-array-read-rules
Atc-array-write-rules
Atc-arrays
Atc-boolean-equality-rules
Atc-boolean-from-integer-return-rules
Atc-boolean-from-sint
Atc-boolean-fron/to-sint-rules
Atc-boolean-termp
Atc-c-valued-termp
Atc-call-info
Atc-call-info->encapsulate
Atc-call-infop
Atc-check-array-read
Atc-check-array-write
Atc-check-binop
Atc-check-boolean-from-type
Atc-check-cfun-call
Atc-check-condexpr
Atc-check-conv
Atc-check-declar/assign-n
Atc-check-guard-conjunct
Atc-check-iconst
Atc-check-integer-read
Atc-check-integer-write
Atc-check-let
Atc-check-loop-call
Atc-check-mv-let
Atc-check-sint-from-boolean
Atc-check-struct-read-array
Atc-check-struct-read-scalar
Atc-check-struct-write-array
Atc-check-struct-write-scalar
Atc-check-symbol-2part
Atc-check-symbol-3part
Atc-check-symbol-4part
Atc-check-symbol-5part
Atc-check-unop
Atc-check-var
Atc-compustate-frames-number-rules
Atc-compustatep-rules
Atc-computation-state-return-rules
Atc-conditional-expressions
Atc-context
Atc-context->preamble
Atc-context->premises
Atc-context-equiv
Atc-context-extend
Atc-context-fix
Atc-contextp
Atc-contextualize
Atc-contextualize-compustate
Atc-convert-integer-value-rules
Atc-create-var-rules
Atc-def-integer-arrays
Atc-def-integer-arrays-loop
Atc-distributivity-over-if-rewrite-rules
Atc-ensure-formals-not-lost
Atc-enter-scope-rules
Atc-event-and-code-generation
Atc-exec-arrsub-rules
Atc-exec-arrsub-rules-generation
Atc-exec-binary-strict-pure-rules
Atc-exec-binary-strict-pure-rules-generation
Atc-exec-block-item-list-rules
Atc-exec-block-item-rules
Atc-exec-cast-rules
Atc-exec-cast-rules-generation
Atc-exec-const-rules
Atc-exec-expr-asg-arrsub-rules
Atc-exec-expr-asg-arrsub-rules-generation
Atc-exec-expr-asg-ident-rules
Atc-exec-expr-asg-indir-rule-generation
Atc-exec-expr-asg-indir-rules
Atc-exec-expr-asg-rules
Atc-exec-expr-call-or-asg-rules
Atc-exec-expr-call-or-pure-rules
Atc-exec-expr-call-rules
Atc-exec-expr-pure-list-rules
Atc-exec-expr-pure-rules
Atc-exec-fun-rules
Atc-exec-ident-rules
Atc-exec-indir-rules
Atc-exec-indir-rules-generation
Atc-exec-initer-rules
Atc-exec-stmt-rules
Atc-exec-unary-nonpointer-rules
Atc-exec-unary-nonpointer-rules-generation
Atc-exit-scope-rules
Atc-expression-generation
Atc-filter-exec-fun-args
Atc-find-affected
Atc-flexible-array-member-rules
Atc-fn
Atc-fn-info
Atc-fn-info->affect
Atc-fn-info->correct-mod-thm
Atc-fn-info->correct-thm
Atc-fn-info->extobjs
Atc-fn-info->fun-env-thm
Atc-fn-info->guard
Atc-fn-info->in-types
Atc-fn-info->limit
Atc-fn-info->loop?
Atc-fn-info->measure-nat-thm
Atc-fn-info->out-type
Atc-fn-info->result-thm
Atc-fn-info-equiv
Atc-fn-info-fix
Atc-fn-infop
Atc-formal-affectable-listp
Atc-formal-affectable-listp-basics
Atc-formal-affectablep
Atc-function-and-loop-generation
Atc-function-tables
Atc-gen-add-var-formals
Atc-gen-appconds
Atc-gen-block-item-array-asg
Atc-gen-block-item-asg
Atc-gen-block-item-declon
Atc-gen-block-item-integer-asg
Atc-gen-block-item-list-append
Atc-gen-block-item-list-cons
Atc-gen-block-item-list-none
Atc-gen-block-item-list-one
Atc-gen-block-item-stmt
Atc-gen-block-item-struct-array-asg
Atc-gen-block-item-struct-scalar-asg
Atc-gen-block-item-var-asg
Atc-gen-block-item-var-decl
Atc-gen-call-result-and-endstate
Atc-gen-cfun-call-stmt
Atc-gen-cfun-correct-thm
Atc-gen-cfun-final-compustate
Atc-gen-cfun-fun-env-thm
Atc-gen-cfun-fun-env-thm-name
Atc-gen-context-preamble
Atc-gen-context-preamble-aux-aux
Atc-gen-enter-inscope
Atc-gen-everything
Atc-gen-exec-stmt-while-for-loop
Atc-gen-expr
Atc-gen-expr-and
Atc-gen-expr-array-read
Atc-gen-expr-binary
Atc-gen-expr-bool
Atc-gen-expr-bool-correct-thm
Atc-gen-expr-bool-from-type
Atc-gen-expr-cond
Atc-gen-expr-const
Atc-gen-expr-conv
Atc-gen-expr-integer-read
Atc-gen-expr-or
Atc-gen-expr-pure
Atc-gen-expr-pure-correct-thm
Atc-gen-expr-pure-list
Atc-gen-expr-pure/bool
Atc-gen-expr-sint-from-bool
Atc-gen-expr-struct-read-array
Atc-gen-expr-struct-read-scalar
Atc-gen-expr-unary
Atc-gen-expr-var
Atc-gen-ext-declon-lists
Atc-gen-fileset
Atc-gen-fileset-event
Atc-gen-fn-def*
Atc-gen-fn-guard
Atc-gen-fn-result-thm
Atc-gen-formal-thm
Atc-gen-fun-correct-thm
Atc-gen-fun-endstate
Atc-gen-fundef
Atc-gen-if/ifelse-inscope
Atc-gen-if/ifelse-stmt
Atc-gen-init-fun-env-thm
Atc-gen-init-inscope
Atc-gen-init-inscope-auto
Atc-gen-init-inscope-static
Atc-gen-init-scope-thms
Atc-gen-loop
Atc-gen-loop-body-correct-thm
Atc-gen-loop-correct-thm
Atc-gen-loop-final-compustate
Atc-gen-loop-measure-fn
Atc-gen-loop-measure-thm
Atc-gen-loop-stmt
Atc-gen-loop-termination-thm
Atc-gen-loop-test-correct-thm
Atc-gen-loop-tthm-formula
Atc-gen-loop-tthm-formula-lst
Atc-gen-mbt-block-items
Atc-gen-new-inscope
Atc-gen-obj-declon
Atc-gen-object-disjoint-hyps
Atc-gen-omap-update-formals
Atc-gen-outer-bindings-and-hyps
Atc-gen-param-declon-list
Atc-gen-pop-frame-thm
Atc-gen-prog-const
Atc-gen-push-init-thm
Atc-gen-return-stmt
Atc-gen-stmt
Atc-gen-struct-declon-list
Atc-gen-tag-declon
Atc-gen-tag-member-read-all-thms
Atc-gen-tag-member-read-thms
Atc-gen-tag-member-write-all-thms
Atc-gen-tag-member-write-thms
Atc-gen-term-type-formula
Atc-gen-thm-assert-events
Atc-gen-vardecl-inscope
Atc-gen-wf-thm
Atc-generation-contexts
Atc-get-tag-info
Atc-get-var
Atc-get-var-check-innermost
Atc-get-vars
Atc-get-vars-check-innermost
Atc-hide-rules
Atc-identifier-other-rules
Atc-identifier-rules
Atc-if*-rules
Atc-implementation
Atc-init-scope-rules
Atc-init-value-to-value-rules
Atc-input-processing
Atc-integer-const-rules
Atc-integer-constructors-return-rules
Atc-integer-conv-rules
Atc-integer-fix-rules
Atc-integer-ifix-rules
Atc-integer-size-rules
Atc-let-designations
Atc-limit-rules
Atc-lognot-sint-rules
Atc-loop-body-term-subst
Atc-macro-definition
Atc-make-lets-of-uterms
Atc-make-mv-lets-of-uterms
Atc-make-mv-nth-terms
Atc-maybe-call-infop
Atc-misc-rewrite-rules
Atc-not-error-rules
Atc-obj-info
Atc-obj-info->defobject
Atc-obj-info-equiv
Atc-obj-info-fix
Atc-obj-infop
Atc-object-designator-rules
Atc-object-tables
Atc-pointed-integer-rules
Atc-pop-frame-rules
Atc-premise
Atc-premise-case
Atc-premise-compustate
Atc-premise-compustate->term
Atc-premise-compustate->var
Atc-premise-cvalue
Atc-premise-cvalue->term
Atc-premise-cvalue->var
Atc-premise-cvalues
Atc-premise-cvalues->term
Atc-premise-cvalues->vars
Atc-premise-equiv
Atc-premise-fix
Atc-premise-kind
Atc-premise-list
Atc-premise-list-equiv
Atc-premise-list-fix
Atc-premise-listp
Atc-premise-listp-basics
Atc-premise-test
Atc-premise-test->term
Atc-premisep
Atc-pretty-printer
Atc-pretty-printing-options
Atc-process-const-name
Atc-process-const-name-aux
Atc-process-file-name
Atc-process-function
Atc-process-header
Atc-process-inputs
Atc-process-inputs-and-gen-everything
Atc-process-output-dir
Atc-process-pretty-printing
Atc-process-print
Atc-process-proofs
Atc-process-target
Atc-process-target-list
Atc-process-targets
Atc-promote-value-rules
Atc-pure-c-valued-termp
Atc-push-frame-rules
Atc-read-object-rules
Atc-read-static-var-rules
Atc-read-var-rules
Atc-remove-called-fns
Atc-remove-extobj-args
Atc-shallow-embedding
Atc-sint-from-boolean
Atc-sint-from-boolean-rules
Atc-sint-get-rules
Atc-statement-generation
Atc-static-variable-pointer-rules
Atc-stmt-noncval-termp
Atc-string-objinfo-alist
Atc-string-objinfo-alist-equiv
Atc-string-objinfo-alist-fix
Atc-string-objinfo-alist-to-recognizers
Atc-string-objinfo-alistp
Atc-string-taginfo-alist
Atc-string-taginfo-alist-equiv
Atc-string-taginfo-alist-fix
Atc-string-taginfo-alist-to-flexiblep-thms
Atc-string-taginfo-alist-to-member-read-thms
Atc-string-taginfo-alist-to-member-write-thms
Atc-string-taginfo-alist-to-not-error-thms
Atc-string-taginfo-alist-to-pointer-type-to-quoted-thms
Atc-string-taginfo-alist-to-reader-return-thms
Atc-string-taginfo-alist-to-readers
Atc-string-taginfo-alist-to-recognizers
Atc-string-taginfo-alist-to-type-of-value-thms
Atc-string-taginfo-alist-to-type-to-quoted-thms
Atc-string-taginfo-alist-to-value-kind-thms
Atc-string-taginfo-alist-to-valuep-thms
Atc-string-taginfo-alist-to-writer-return-thms
Atc-string-taginfo-alist-to-writers
Atc-string-taginfo-alistp
Atc-symbol-fninfo-alist
Atc-symbol-fninfo-alist-equiv
Atc-symbol-fninfo-alist-fix
Atc-symbol-fninfo-alist-to-correct-thms
Atc-symbol-fninfo-alist-to-fun-env-thms
Atc-symbol-fninfo-alist-to-measure-nat-thms
Atc-symbol-fninfo-alist-to-result-thms
Atc-symbol-fninfo-alistp
Atc-symbol-varinfo-alist
Atc-symbol-varinfo-alist-equiv
Atc-symbol-varinfo-alist-fix
Atc-symbol-varinfo-alist-list
Atc-symbol-varinfo-alist-list-equiv
Atc-symbol-varinfo-alist-list-fix
Atc-symbol-varinfo-alist-list-to-thms
Atc-symbol-varinfo-alist-listp
Atc-symbol-varinfo-alist-listp-basics
Atc-symbol-varinfo-alist-to-thms
Atc-symbol-varinfo-alistp
Atc-symbolic-computation-states
Atc-symbolic-execution-rules
Atc-symbolp-list
Atc-syntaxp-hyp-for-expr-pure
Atc-table
Atc-table-definition
Atc-table-lookup
Atc-table-record-event
Atc-tag-generation
Atc-tag-generation-rules
Atc-tag-info
Atc-tag-info->defstruct
Atc-tag-info->member-read-thms
Atc-tag-info->member-write-thms
Atc-tag-info-equiv
Atc-tag-info-fix
Atc-tag-infop
Atc-tag-tables
Atc-term-recognizers
Atc-test-value-rules
Atc-theorem-generation
Atc-tutorial
Atc-tutorial-approach
Atc-tutorial-assignments
Atc-tutorial-atj-comparison
Atc-tutorial-conditional-expressions
Atc-tutorial-conditional-statements
Atc-tutorial-conditionals-nonconcluding
Atc-tutorial-conditionals-with-mbt
Atc-tutorial-events
Atc-tutorial-identifiers
Atc-tutorial-int-programs
Atc-tutorial-int-representation
Atc-tutorial-local-variables
Atc-tutorial-motivation
Atc-tutorial-multiple-functions
Atc-tutorial-proofs
Atc-tyname-to-type-rules
Atc-type-kind-rules
Atc-type-of-value-option-rules
Atc-type-of-value-rules
Atc-type-to-notflexarrmem-thms
Atc-type-to-pointer-type-to-quoted-thms
Atc-type-to-recognizer
Atc-type-to-type-of-value-thm
Atc-type-to-type-to-quoted-thms
Atc-type-to-value-kind-thm
Atc-type-to-valuep-thm
Atc-typed-formals
Atc-typed-formals-to-extobjs
Atc-types
Atc-uaconvert-values-rules
Atc-uaconvert-values-rules-generation
Atc-update-object-rules
Atc-update-static-var-rules
Atc-update-var-rules
Atc-update-var-term-alist
Atc-uterm-to-components
Atc-value-arithmeticp-rules
Atc-value-array->elements-rules
Atc-value-array->elemtype-rules
Atc-value-fix-rules
Atc-value-integer->get-rules
Atc-value-integerp-rules
Atc-value-kind-rules
Atc-value-listp-rules
Atc-value-optionp-rules
Atc-value-pointer-rules
Atc-value-result-fix-rules
Atc-valuep-rules
Atc-var-assignablep
Atc-var-autop-rules
Atc-var-info
Atc-var-info->externalp
Atc-var-info->thm
Atc-var-info->type
Atc-var-info-equiv
Atc-var-info-fix
Atc-var-info-list
Atc-var-info-list->thm-list
Atc-var-info-list->type-list
Atc-var-info-list-equiv
Atc-var-info-list-fix
Atc-var-info-listp
Atc-var-info-listp-basics
Atc-var-info-option
Atc-var-info-option-case
Atc-var-info-option-equiv
Atc-var-info-option-fix
Atc-var-info-option-list
Atc-var-info-option-list-equiv
Atc-var-info-option-list-fix
Atc-var-info-option-listp
Atc-var-info-option-listp-basics
Atc-var-info-option-none
Atc-var-info-option-some
Atc-var-info-option-some->val
Atc-var-info-optionp
Atc-var-infop
Atc-variable-tables
Atc-vars-assignablep
Atc-wrapper-rules
Atc-write-object-rules
Atc-write-static-var-rules
Atc-write-var-rules
Atj
Atj-adapt-expr-to-type
Atj-adapt-expr-to-types
Atj-adapt-exprs-to-types
Atj-add-qconstant
Atj-add-qconstants-in-term
Atj-add-qconstants-in-terms
Atj-all-mv-output-types
Atj-analyze-arrays-in-args
Atj-analyze-arrays-in-formals+body
Atj-analyze-arrays-in-mv-let
Atj-analyze-arrays-in-term
Atj-atype
Atj-atype-<=
Atj-atype-boolean
Atj-atype-case
Atj-atype-character
Atj-atype-cons
Atj-atype-equiv
Atj-atype-fix
Atj-atype-integer
Atj-atype-kind
Atj-atype-number
Atj-atype-rational
Atj-atype-string
Atj-atype-symbol
Atj-atype-value
Atj-atypep
Atj-cache-const-methods
Atj-char-to-jchars-id
Atj-char-to-jhexcode
Atj-chars-to-jchars-id
Atj-chars-to-jhexcodes
Atj-check-annotated-mv-let-call
Atj-check-foldable-return
Atj-check-liftable-loop-test
Atj-check-marked-annotated-mv-let-call
Atj-check-no-aij-term
Atj-check-no-aij-term-list
Atj-check-no-aij-type
Atj-check-no-aij-type-list
Atj-check-no-aij-type-list-basics
Atj-check-no-aij-types+body
Atj-check-other-function-type
Atj-check-single-return-with-expr
Atj-code-generation
Atj-collect-fns-in-term
Atj-collect-fns-in-terms
Atj-common-code-generation
Atj-convert-expr-from-jprim
Atj-convert-expr-from-jprimarr
Atj-convert-expr-from-jprimarr-method
Atj-convert-expr-from-jprimarr-method-name
Atj-convert-expr-to-jprim
Atj-convert-expr-to-jprimarr
Atj-convert-expr-to-jprimarr-method
Atj-convert-expr-to-jprimarr-method-name
Atj-deep-code-generation
Atj-def-java-primitive-array-model
Atj-elim-tailrec
Atj-elim-tailrec-gen-block
Atj-elim-tailrec-in-jblock
Atj-elim-tailrec-in-jstatem
Atj-elim-tailrec-in-jstatems+jblocks
Atj-elim-tailrec-in-return
Atj-ensure-no-array-write-calls
Atj-fn
Atj-fn-body
Atj-fn-to-method
Atj-fnnative-method-name
Atj-fns-to-methods
Atj-fns-to-translate
Atj-fold-returns
Atj-function-type
Atj-function-type->arrays
Atj-function-type->inputs
Atj-function-type->outputs
Atj-function-type-equiv
Atj-function-type-fix
Atj-function-type-info
Atj-function-type-info->main
Atj-function-type-info->others
Atj-function-type-info->outputs
Atj-function-type-info-default
Atj-function-type-info-equiv
Atj-function-type-info-fix
Atj-function-type-info-p
Atj-function-type-info-table
Atj-function-type-list
Atj-function-type-list->inputs
Atj-function-type-list->outputs
Atj-function-type-list-equiv
Atj-function-type-list-fix
Atj-function-type-listp
Atj-function-type-listp-basics
Atj-function-type-of-min-input-types
Atj-function-type-of-min-input-types-aux
Atj-function-type-p
Atj-gen-char
Atj-gen-deep-build-method
Atj-gen-deep-call-method
Atj-gen-deep-env-class
Atj-gen-deep-env-cunit
Atj-gen-deep-fnapp
Atj-gen-deep-fndef-method
Atj-gen-deep-fndef-method-name
Atj-gen-deep-fndef-methods
Atj-gen-deep-fndefs
Atj-gen-deep-formals
Atj-gen-deep-lambda
Atj-gen-deep-main-class
Atj-gen-deep-main-cunit
Atj-gen-deep-qconst
Atj-gen-deep-term
Atj-gen-deep-term-fns
Atj-gen-deep-terms
Atj-gen-deep-test-code
Atj-gen-deep-var
Atj-gen-env-file
Atj-gen-everything
Atj-gen-init-method
Atj-gen-integer
Atj-gen-jbigint
Atj-gen-jboolean
Atj-gen-jboolean-array
Atj-gen-jbyte
Atj-gen-jbyte-array
Atj-gen-jchar
Atj-gen-jchar-array
Atj-gen-jint
Atj-gen-jint-array
Atj-gen-jlocvar-indexed
Atj-gen-jlong
Atj-gen-jlong-array
Atj-gen-jshort
Atj-gen-jshort-array
Atj-gen-jstring
Atj-gen-list
Atj-gen-list-flat
Atj-gen-main-file
Atj-gen-number
Atj-gen-output-subdir
Atj-gen-paramlist
Atj-gen-pkg-method
Atj-gen-pkg-method-name
Atj-gen-pkg-methods
Atj-gen-pkg-name
Atj-gen-pkgs
Atj-gen-rational
Atj-gen-run-tests
Atj-gen-shallow-all-fn-methods
Atj-gen-shallow-all-jprimarr-conv-methods
Atj-gen-shallow-all-pkg-fields
Atj-gen-shallow-all-pkg-methods
Atj-gen-shallow-all-synonym-methods
Atj-gen-shallow-and-call
Atj-gen-shallow-build-method
Atj-gen-shallow-char
Atj-gen-shallow-char-field
Atj-gen-shallow-char-field-name
Atj-gen-shallow-char-fields
Atj-gen-shallow-cons
Atj-gen-shallow-cons-field
Atj-gen-shallow-cons-field-name
Atj-gen-shallow-cons-fields
Atj-gen-shallow-env-class
Atj-gen-shallow-env-cunit
Atj-gen-shallow-fn-call
Atj-gen-shallow-fn-methods
Atj-gen-shallow-fndef-all-methods
Atj-gen-shallow-fndef-method
Atj-gen-shallow-fndef-methods
Atj-gen-shallow-fnname
Atj-gen-shallow-fnnative-all-methods
Atj-gen-shallow-fnnative-method
Atj-gen-shallow-fnnative-methods
Atj-gen-shallow-if-call
Atj-gen-shallow-integer-id-part
Atj-gen-shallow-jprim-binop-call
Atj-gen-shallow-jprim-constr-call
Atj-gen-shallow-jprim-conv-call
Atj-gen-shallow-jprim-deconstr-call
Atj-gen-shallow-jprim-unop-call
Atj-gen-shallow-jprimarr-conv-fromlist-call
Atj-gen-shallow-jprimarr-conv-tolist-call
Atj-gen-shallow-jprimarr-fromlist-methods
Atj-gen-shallow-jprimarr-length-call
Atj-gen-shallow-jprimarr-new-init-call
Atj-gen-shallow-jprimarr-new-len-call
Atj-gen-shallow-jprimarr-read-call
Atj-gen-shallow-jprimarr-tolist-methods
Atj-gen-shallow-jprimarr-write-call
Atj-gen-shallow-jtype
Atj-gen-shallow-lambda
Atj-gen-shallow-let-bindings
Atj-gen-shallow-main-class
Atj-gen-shallow-main-cunit
Atj-gen-shallow-mv-asgs
Atj-gen-shallow-mv-call
Atj-gen-shallow-mv-class
Atj-gen-shallow-mv-class-name
Atj-gen-shallow-mv-classes
Atj-gen-shallow-mv-classes-guard
Atj-gen-shallow-mv-field-name
Atj-gen-shallow-mv-fields
Atj-gen-shallow-mv-let
Atj-gen-shallow-mv-params
Atj-gen-shallow-not-call
Atj-gen-shallow-number
Atj-gen-shallow-number-field
Atj-gen-shallow-number-field-name
Atj-gen-shallow-number-fields
Atj-gen-shallow-number-id-part
Atj-gen-shallow-or-call
Atj-gen-shallow-pkg-class
Atj-gen-shallow-pkg-classes
Atj-gen-shallow-pkg-fields
Atj-gen-shallow-pkg-methods
Atj-gen-shallow-primarray-write-method
Atj-gen-shallow-primarray-write-methods
Atj-gen-shallow-rational-id-part
Atj-gen-shallow-string
Atj-gen-shallow-string-field
Atj-gen-shallow-string-field-name
Atj-gen-shallow-string-fields
Atj-gen-shallow-symbol
Atj-gen-shallow-symbol-field
Atj-gen-shallow-symbol-field-name
Atj-gen-shallow-symbol-fields
Atj-gen-shallow-synonym-all-methods
Atj-gen-shallow-synonym-method
Atj-gen-shallow-synonym-method-params
Atj-gen-shallow-synonym-methods
Atj-gen-shallow-term
Atj-gen-shallow-term-fns
Atj-gen-shallow-terms
Atj-gen-shallow-test-code
Atj-gen-shallow-test-code-asgs
Atj-gen-shallow-test-code-comps
Atj-gen-shallow-test-code-mv-asgs
Atj-gen-shallow-value
Atj-gen-static-initializer
Atj-gen-string
Atj-gen-symbol
Atj-gen-symbols
Atj-gen-test-class
Atj-gen-test-cunit
Atj-gen-test-failures-field
Atj-gen-test-file
Atj-gen-test-main-method
Atj-gen-test-method
Atj-gen-test-method-name
Atj-gen-test-methods
Atj-gen-test-value
Atj-gen-test-values
Atj-gen-value
Atj-gen-value-flat
Atj-gen-values
Atj-gen-values-flat
Atj-get-fn-method-name
Atj-get-function-type-info
Atj-get-function-type-info-from-table
Atj-get-pkg-class-name
Atj-implementation
Atj-indent
Atj-input-processing
Atj-java-abstract-syntax
Atj-java-input-types
Atj-java-pretty-printer
Atj-java-primitive-array-model
Atj-java-primitive-arrays
Atj-java-primitives
Atj-java-syntax-operations
Atj-jblock-list-to-2-jblocks
Atj-jblock-list-to-3-jblocks
Atj-jexpr-list-to-2-jexprs
Atj-jexpr-list-to-3-jexprs
Atj-jitype-listp
Atj-jitype-listp-basics
Atj-jitypep
Atj-jprim-binop-fn-p
Atj-jprim-binop-fn-to-jbinop
Atj-jprim-constr-fn-of-qconst-to-expr
Atj-jprim-constr-fn-p
Atj-jprim-constr-fn-to-ptype
Atj-jprim-conv-fn-p
Atj-jprim-conv-fn-to-jtype
Atj-jprim-deconstr-fn-p
Atj-jprim-deconstr-fn-to-ptype
Atj-jprim-fn-p
Atj-jprim-unop-fn-p
Atj-jprim-unop-fn-to-junop
Atj-jprimarr-conv-fromlist-fn-p
Atj-jprimarr-conv-fromlist-fn-to-ptype
Atj-jprimarr-conv-tolist-fn-p
Atj-jprimarr-conv-tolist-fn-to-ptype
Atj-jprimarr-fn-p
Atj-jprimarr-length-fn-p
Atj-jprimarr-new-init-fn-p
Atj-jprimarr-new-init-fn-to-comp-jtype
Atj-jprimarr-new-init-fn-to-ptype
Atj-jprimarr-new-len-fn-p
Atj-jprimarr-new-len-fn-to-comp-jtype
Atj-jprimarr-read-fn-p
Atj-jprimarr-write-fn-p
Atj-jprimarr-write-to-method-name
Atj-library-extensions
Atj-lift-loop-test
Atj-macro-definition
Atj-main-function-type
Atj-main-function-type-fn
Atj-main-function-type-input-theorem
Atj-main-function-type-input-theorems
Atj-main-function-type-output-theorem
Atj-main-function-type-output-theorems
Atj-make-parallel-asg
Atj-mark-formals+body
Atj-mark-lambda-formals
Atj-mark-term
Atj-mark-terms
Atj-mark-var-new
Atj-mark-var-old
Atj-mark-vars-new
Atj-maybe-function-type
Atj-maybe-function-type-case
Atj-maybe-function-type-equiv
Atj-maybe-function-type-fix
Atj-maybe-function-type-info
Atj-maybe-function-type-info-case
Atj-maybe-function-type-info-equiv
Atj-maybe-function-type-info-fix
Atj-maybe-function-type-info-none
Atj-maybe-function-type-info-p
Atj-maybe-function-type-info-some
Atj-maybe-function-type-info-some->val
Atj-maybe-function-type-none
Atj-maybe-function-type-p
Atj-maybe-function-type-some
Atj-maybe-function-type-some->val
Atj-maybe-type
Atj-maybe-type-case
Atj-maybe-type-equiv
Atj-maybe-type-fix
Atj-maybe-type-list
Atj-maybe-type-list-equiv
Atj-maybe-type-list-fix
Atj-maybe-type-listp
Atj-maybe-type-listp-basics
Atj-maybe-type-none
Atj-maybe-type-some
Atj-maybe-type-some->val
Atj-maybe-typep
Atj-name-translation
Atj-number-of-results
Atj-other-function-type
Atj-other-function-type-fn
Atj-other-function-type-theorem
Atj-other-function-type-theorems
Atj-parallel-asg-depgraph
Atj-pkg-to-class
Atj-pkgs-to-classes
Atj-pkgs-to-translate
Atj-post-translate-body
Atj-post-translate-jcbody-elements
Atj-post-translation
Atj-post-translation-cache-const-methods
Atj-post-translation-fold-returns
Atj-post-translation-lift-loop-tests
Atj-post-translation-remove-array-write-calls
Atj-post-translation-remove-continue
Atj-post-translation-simplify-conds
Atj-post-translation-tailrec-elimination
Atj-pre-translate
Atj-pre-translation
Atj-pre-translation-array-analysis
Atj-pre-translation-conjunctions
Atj-pre-translation-disjunctions
Atj-pre-translation-multiple-values
Atj-pre-translation-no-aij-types-analysis
Atj-pre-translation-remove-dead-if-branches
Atj-pre-translation-remove-return-last
Atj-pre-translation-trivial-vars
Atj-pre-translation-type-annotation
Atj-pre-translation-unused-vars
Atj-pre-translation-var-renaming
Atj-pre-translation-var-reuse
Atj-primarray-write-method-name
Atj-process-inputs
Atj-process-java-class
Atj-process-java-package
Atj-process-no-aij-types
Atj-process-output-dir
Atj-process-output-subdir
Atj-process-output-type-spec
Atj-process-output-type-specs
Atj-process-targets
Atj-process-test
Atj-process-test-input
Atj-process-test-input-jprim-value
Atj-process-test-input-jprim-values
Atj-process-test-inputs
Atj-process-tests
Atj-qconstants
Atj-qconstants->chars
Atj-qconstants->integers
Atj-qconstants->next-index
Atj-qconstants->numbers
Atj-qconstants->pairs
Atj-qconstants->rationals
Atj-qconstants->strings
Atj-qconstants->symbols
Atj-qconstants-p
Atj-remove-array-write-call-asgs-in-jblock
Atj-remove-array-write-call-asgs-in-jstatem
Atj-remove-array-write-call-asgs-in-jstatems+jblocks
Atj-remove-array-write-call-in-asg
Atj-remove-array-write-call-return
Atj-remove-array-write-call-returns-in-jblock
Atj-remove-array-write-call-returns-in-jstatem
Atj-remove-array-write-call-returns-in-jstatems+jblocks
Atj-remove-array-write-calls
Atj-remove-continue-in-jblock
Atj-remove-continue-in-jstatem
Atj-remove-continue-in-jstatems+jblocks
Atj-remove-ending-continue
Atj-remove-return-last
Atj-rename-formal
Atj-rename-formals
Atj-rename-formals+body
Atj-rename-term
Atj-rename-terms
Atj-restore-and-calls-in-term
Atj-restore-and-calls-in-terms
Atj-restore-mv-calls-in-args
Atj-restore-mv-calls-in-body
Atj-restore-mv-calls-in-term
Atj-restore-or-calls-in-term
Atj-restore-or-calls-in-terms
Atj-select-mv-term-types
Atj-serialize-parallel-asg
Atj-shallow-code-generation
Atj-shallow-fns-that-may-throw
Atj-shallow-quoted-constant-generation
Atj-simplify-conds-in-jblock
Atj-simplify-conds-in-jexpr
Atj-simplify-conds-in-jexprs
Atj-simplify-conds-in-jstatem
Atj-simplify-conds-in-jstatems+jblocks
Atj-string-ascii-java-identifier-listp
Atj-string-ascii-java-identifier-listp-basics
Atj-string-ascii-java-identifier-p
Atj-string-ascii-java-package-name-p
Atj-symbol-type-alist
Atj-symbol-type-alist-equiv
Atj-symbol-type-alist-fix
Atj-symbol-type-alistp
Atj-test
Atj-test->function
Atj-test->inputs
Atj-test->name
Atj-test->outputs
Atj-test-equiv
Atj-test-fix
Atj-test-list
Atj-test-list-equiv
Atj-test-list-fix
Atj-test-listp
Atj-test-listp-basics
Atj-test-structures
Atj-test-value
Atj-test-value-ACL2
Atj-test-value-ACL2->get
Atj-test-value-ACL2-list
Atj-test-value-case
Atj-test-value-equiv
Atj-test-value-fix
Atj-test-value-jboolean
Atj-test-value-jboolean->get
Atj-test-value-jboolean[]
Atj-test-value-jboolean[]->get
Atj-test-value-jbyte
Atj-test-value-jbyte->get
Atj-test-value-jbyte[]
Atj-test-value-jbyte[]->get
Atj-test-value-jchar
Atj-test-value-jchar->get
Atj-test-value-jchar[]
Atj-test-value-jchar[]->get
Atj-test-value-jint
Atj-test-value-jint->get
Atj-test-value-jint[]
Atj-test-value-jint[]->get
Atj-test-value-jlong
Atj-test-value-jlong->get
Atj-test-value-jlong[]
Atj-test-value-jlong[]->get
Atj-test-value-jshort
Atj-test-value-jshort->get
Atj-test-value-jshort[]
Atj-test-value-jshort[]->get
Atj-test-value-kind
Atj-test-value-list
Atj-test-value-list-equiv
Atj-test-value-list-fix
Atj-test-value-listp
Atj-test-value-listp-basics
Atj-test-value-of-type
Atj-test-value-to-type
Atj-test-valuep
Atj-test-values-of-types
Atj-test-values-to-types
Atj-testp
Atj-tutorial
Atj-tutorial-ACL2-environment
Atj-tutorial-ACL2-terms
Atj-tutorial-ACL2-values
Atj-tutorial-aij
Atj-tutorial-background
Atj-tutorial-customization
Atj-tutorial-deep
Atj-tutorial-deep-guards
Atj-tutorial-deep-shallow
Atj-tutorial-evaluator
Atj-tutorial-motivation
Atj-tutorial-native-functions
Atj-tutorial-screen-output
Atj-tutorial-shallow
Atj-tutorial-shallow-guards
Atj-tutorial-simplified-uml
Atj-tutorial-tests
Atj-tutorial-translated
Atj-type
Atj-type-<
Atj-type-<=
Atj-type-ACL2
Atj-type-ACL2->get
Atj-type-annotate-args
Atj-type-annotate-formals+body
Atj-type-annotate-mv-let
Atj-type-annotate-mv-nth-terms
Atj-type-annotate-term
Atj-type-annotate-var
Atj-type-annotate-vars
Atj-type-bottom-<=
Atj-type-bottom-list-<=
Atj-type-bottom-list-meet
Atj-type-bottom-meet
Atj-type-case
Atj-type-conv
Atj-type-conv-allowed-p
Atj-type-equiv
Atj-type-fix
Atj-type-from-keyword
Atj-type-id
Atj-type-irrelevant
Atj-type-join
Atj-type-jprim
Atj-type-jprim->get
Atj-type-jprimarr
Atj-type-jprimarr->comp
Atj-type-kind
Atj-type-list
Atj-type-list-<
Atj-type-list-<=
Atj-type-list-equiv
Atj-type-list-fix
Atj-type-list-from-keyword-list
Atj-type-list-join
Atj-type-list-list
Atj-type-list-list-equiv
Atj-type-list-list-fix
Atj-type-list-listp
Atj-type-list-listp-basics
Atj-type-list-meet
Atj-type-list-to-jitype-list
Atj-type-list-to-keyword-list
Atj-type-list-to-type
Atj-type-list-to-type-list-list
Atj-type-listp
Atj-type-listp-basics
Atj-type-macros
Atj-type-meet
Atj-type-of-id
Atj-type-of-value
Atj-type-rewrap-term
Atj-type-rewrap-terms
Atj-type-semilattices
Atj-type-to-jitype
Atj-type-to-keyword
Atj-type-to-pred
Atj-type-to-pred-gen-mono-thm
Atj-type-to-pred-gen-mono-thms
Atj-type-to-pred-gen-mono-thms-1
Atj-type-to-pred-gen-mono-thms-2
Atj-type-to-type-list
Atj-type-top-<=
Atj-type-top-join
Atj-type-top-list-<=
Atj-type-top-list-join
Atj-type-unannotate-var
Atj-type-unannotate-vars
Atj-type-unwrap-term
Atj-type-wrap-term
Atj-type-wrapped-variable-p
Atj-typep
Atj-types
Atj-types-conv-allowed-p
Atj-types-for-java-primitive-arrays
Atj-types-for-java-primitives
Atj-types-id
Atj-types-of-conv
Atj-types-of-id
Atj-unmark-var
Atj-unmark-vars
Atj-var-add-index
Atj-var-to-jvar
Atj-vars-in-jexpr
Atj-vars-in-jexpr-list
Atj-worklist-iterate
Atom
Atom-listp
Atom-size
Attach-meta-fncs
Attachments
Attributes
Attributes-equiv
Attributes-fix
Attributes-p
Auto-bindings
Auto-instance
Auto-termination
Autohide
Avx-pfx-well-formed-p
Axe
Axi
Axi-const
Axi-gate
Axi-gate->left
Axi-gate->op
Axi-gate->right
Axi-lit
Axi-lit->abs
Axi-lit->negp
Axi-lit-count
Axi-lit-equiv
Axi-lit-fix
Axi-lit-p
Axi-litlist
Axi-litlist-equiv
Axi-litlist-fix
Axi-litlist-p
Axi-litlist-p-basics
Axi-map
Axi-map-equiv
Axi-map-fix
Axi-map-p
Axi-op-p
Axi-term
Axi-term-count
Axi-term-equiv
Axi-term-fix
Axi-term-kind
Axi-term-p
Axi-termlist
Axi-termlist-equiv
Axi-termlist-fix
Axi-termlist-p
Axi-termlist-p-basics
Axi-var
Axi-var->name
B
B*
B*-binders
B-and
B-andc1
B-andc2
B-eqv
B-ior
B-ite
B-nand
B-nor
B-not
B-orc1
B-orc2
B-xor
B64-bytes-from-vals
B64-char-from-value
B64-dec1
B64-dec2
B64-dec3
B64-decode-last-group
B64-decode-list-impl
B64-decode-str-impl
B64-enc1
B64-enc2
B64-enc3
B64-encode-last-group
B64-encode-last-group-str
B64-encode-list-impl
B64-encode-str-impl
B64-vals-from-bytes
B64-value-from-code
Baby-jubjub
Baby-jubjub-a
Baby-jubjub-add
Baby-jubjub-curve
Baby-jubjub-d
Baby-jubjub-mul
Baby-jubjub-order
Baby-jubjub-order/8
Baby-jubjub-pointp
Baby-jubjub-prime
Baby-jubjub-subgroup-prime
Backchain-limit
Backchain-limit-rw
Backchaining
Backquote
Backref
Backref->len
Backref->loc
Backref-alist
Backref-alist-equiv
Backref-alist-fix
Backref-alist-in-bounds
Backref-alist-p
Backref-equiv
Backref-extract-substr
Backref-fix
Backref-in-bounds
Backref-p
Backtrack
Backtrack-bad-generalizations
Backtrack-limit
Badge
Badge-userfn
Bag
Bagp
Bakery-algorithm
Balance
Balance!
Balance-config
Balance-config->gatesimp
Balance-config->search-higher-levels
Balance-config->search-limit
Balance-config->search-second-lit
Balance-config->supergate-limit
Balance-config->verbosity-level
Balance-config-equiv
Balance-config-fix
Balance-config-p
Balance-core
Base-api
Base-fsm
Base-fsm->nextstate
Base-fsm->values
Base-fsm-equiv
Base-fsm-fix
Base-fsm-p
Base58
Base58-char=>val
Base58-character
Base58-character-fix
Base58-character-list
Base58-character-list-equiv
Base58-character-list-fix
Base58-character-listp
Base58-character-listp-basics
Base58-characterp
Base58-chars=>vals
Base58-decode
Base58-encode
Base58-encode/decode-inverses-theorems
Base58-val<=>char-inverses-theorems
Base58-val=>char
Base58-vals<=>chars-inverses-theorems
Base58-vals=>chars
Base58-value
Base58-value-fix
Base58-value-list
Base58-value-list-equiv
Base58-value-list-fix
Base58-value-listp
Base58-value-listp-basics
Base58-valuep
Base58check
Base58check-encode
Base64
Base64-decode
Base64-decode-list
Base64-encode
Base64-encode-list
Base64-impl
Base64-revappend-decode
Base64-revappend-encode
Basename
Basename!
Basenames
Bash
Bash-term-to-dnf
Basic Arithmetic Functions
Basic-alist-equiv-congruences
Basic-bind-elim
Basic-boot-strap
Basic-exec-charp
Basic-expt-normalization
Basic-expt-type-rules
Basic-floating-point-utilities
Basic-list-equiv-congruences
Basic-logops-induction-schemes
Basic-member-lemmas
Basic-nat-to-bin-chars
Basic-nat-to-dec-chars
Basic-nat-to-hex-chars
Basic-nat-to-oct-chars
Basic-print-complex
Basic-print-int
Basic-print-nat
Basic-print-rat
Basic-printing
Basic-printing
Basic-product-normalization
Basic-products-with-negations
Basic-rational-identities
Basic-signed-byte-p-of-*
Basic-signed-byte-p-of-+
Basic-signed-byte-p-of-+-with-cin
Basic-signed-byte-p-of-1+lognot
Basic-signed-byte-p-of-binary-minus
Basic-signed-byte-p-of-floor
Basic-signed-byte-p-of-floor-split
Basic-signed-byte-p-of-lognot
Basic-signed-byte-p-of-mixed-*
Basic-signed-byte-p-of-mod
Basic-signed-byte-p-of-rem
Basic-signed-byte-p-of-truncate
Basic-signed-byte-p-of-truncate-split
Basic-signed-byte-p-of-unary-minus
Basic-signed-byte-p-of-unary-minus-2
Basic-source-charp
Basic-subsetp-lemmas
Basic-sum-normalization
Basic-tutorial
Basic-unsigned-byte-p-of-*
Basic-unsigned-byte-p-of-+
Basic-unsigned-byte-p-of-+-with-cin
Basic-unsigned-byte-p-of-floor
Basic-unsigned-byte-p-of-mod
Basic-unsigned-byte-p-of-rem
Basic-unsigned-byte-p-of-truncate
Basics
Basics
Basicsanity
Bdd
Bdd-algorithm
Bdd-equiv
Bdd-introduction
Bdd-mode-or-p-true
Bdd-sat-dfs
Bddify
Bebits=>nat
Bebits=>nat-injectivity
Bebits=>nat-injectivity*
Bebits=>nat-injectivity+
Bebits=>nat-of-nat=>bebits
Bebits=>nat-of-nat=>bebits*
Bebits=>nat-of-nat=>bebits+
Bebytes=>bits
Bebytes=>nat
Bebytes=>nat-injectivity
Bebytes=>nat-injectivity*
Bebytes=>nat-injectivity+
Bebytes=>nat-of-nat=>bebytes
Bebytes=>nat-of-nat=>bebytes*
Bebytes=>nat-of-nat=>bebytes+
Bech32
Bech32-chars-to-octets
Bech32-collect-high-3-bits
Bech32-collect-low-5-bits
Bech32-hrp-expand
Bech32-index-of-last-1
Bech32-or-bech32m-verify-checksum
Bech32-polymod
Bech32-polymod-aux
Bech32-split-address
Bech32-verify-checksum
Bech32m-verify-checksum
Bed
Bed-eval
Bed-from-aig
Bed-from-aig-aux
Bed-match-var
Bed-mk1
Bed-op-and
Bed-op-andc1
Bed-op-andc2
Bed-op-arg1
Bed-op-arg2
Bed-op-eqv
Bed-op-eval
Bed-op-false
Bed-op-fix
Bed-op-fix$
Bed-op-ior
Bed-op-nand
Bed-op-nor
Bed-op-not1
Bed-op-not2
Bed-op-orc1
Bed-op-orc2
Bed-op-p
Bed-op-true
Bed-op-xor
Bed-order
Bendian=>nat
Best-aig
Best-practices
Beta-reduce
Beubyte11s=>bits
Beubyte11s=>nat
Beubyte11s=>nat-injectivity
Beubyte11s=>nat-injectivity*
Beubyte11s=>nat-injectivity+
Beubyte11s=>nat-of-nat=>beubyte11s
Beubyte11s=>nat-of-nat=>beubyte11s*
Beubyte11s=>nat-of-nat=>beubyte11s+
Beval
Bexp
Bexp-and
Bexp-and->left
Bexp-and->right
Bexp-case
Bexp-const
Bexp-const->value
Bexp-count
Bexp-equal
Bexp-equal->left
Bexp-equal->right
Bexp-equiv
Bexp-fix
Bexp-kind
Bexp-less
Bexp-less->left
Bexp-less->right
Bexp-not
Bexp-not->arg
Bexpp
Bfix
Bfix
Bfr
Bfr
Bfr->aignet-lit
Bfr-<-=-ss
Bfr-<-ss
Bfr-*-ss
Bfr-+-ss
Bfr-=-ss
Bfr-=-uu
Bfr-abs-s
Bfr-and
Bfr-and-macro-exec-part
Bfr-and-macro-logic-part
Bfr-andc1
Bfr-andc2
Bfr-ash-ss
Bfr-binary-and
Bfr-binary-or
Bfr-case
Bfr-cp-ev
Bfr-depends-on
Bfr-env-equiv
Bfr-equiv
Bfr-eval
Bfr-eval
Bfr-eval-alist
Bfr-eval-cp
Bfr-eval-list
Bfr-eval-patterns
Bfr-eval-vals
Bfr-expt-su
Bfr-fix
Bfr-floor-ss
Bfr-floor-ss-aux
Bfr-from-param-space
Bfr-iff
Bfr-integer-length-s
Bfr-integer-length-s1
Bfr-ite
Bfr-ite-bss-fn
Bfr-ite-bss-fn-aux
Bfr-ite-bvv-fn
Bfr-ite-bvv-fn-aux
Bfr-ite-fn
Bfr-list->s
Bfr-list->u
Bfr-list-fix
Bfr-listp$
Bfr-listp$-basics
Bfr-listp-witness
Bfr-logand-ss
Bfr-logapp-nss
Bfr-logapp-nus
Bfr-logapp-nus-aux
Bfr-logapp-russ
Bfr-logbitp-n2v
Bfr-logeqv-ss
Bfr-logext-ns
Bfr-loghead-ns
Bfr-loghead-nu
Bfr-logior-ss
Bfr-lognot-s
Bfr-logtail-ns
Bfr-logxor-ss
Bfr-lookup
Bfr-mcheck
Bfr-mcheck-abc-simple
Bfr-mod-ss
Bfr-mod-ss-aux
Bfr-mode
Bfr-mode
Bfr-mode-case
Bfr-mode-is
Bfr-mode-p
Bfr-nand
Bfr-negate
Bfr-nor
Bfr-not
Bfr-or
Bfr-or-macro-exec-part
Bfr-or-macro-logic-part
Bfr-p
Bfr-param-env
Bfr-patterns
Bfr-reasoning
Bfr-reasoning-mode
Bfr-rem-ss
Bfr-scons
Bfr-set-var
Bfr-set-var
Bfr-sign-abs-not-s
Bfr-sign-s
Bfr-snorm
Bfr-sterm
Bfr-to-param-space
Bfr-to-param-space-weak
Bfr-truncate-ss
Bfr-ucons
Bfr-unary-minus-s
Bfr-unparam-env
Bfr-updates
Bfr-updates-equiv
Bfr-updates-fix
Bfr-updates-p
Bfr-var
Bfr-varname-fix
Bfr-varname-p
Bfr-varnamelist
Bfr-varnamelist-equiv
Bfr-varnamelist-fix
Bfr-varnamelist-p
Bfr-varnamelist-p-basics
Bfr-xor
Bfrstate
Bfrstate>=
Bfrstate->bound
Bfrstate->mode
Bfrstate-case
Bfrstate-fix
Bfrstate-mode-is
Bfrstate-p
Bibliography
Bibliography
Bigmem
Bigmem-concrete-stobj
Bignum-extract
Bin-digit
Bin-digit-char
Bin-digit-char-fix
Bin-digit-char-listp
Bin-digit-char-listp-basics
Bin-digit-char-p
Bin-digit-char-value
Bin-digit-chars-value
Bin-digit-chars-value1
Bin-digit-fix
Bin-digit-list
Bin-digit-list-equiv
Bin-digit-list-fix
Bin-digit-listp
Bin-digit-listp-basics
Bin-digit-string-p
Bin-digit-string-p-aux
Bin-digit-tree
Bin-digit-value
Bin-digitp
Bin-digitp-is-grammar-bin-digitp
Bin-digitp-when-grammar-bin-digitp
Bin-integer-literal
Bin-integer-literal->digits/uscores
Bin-integer-literal->prefix-upcase-p
Bin-integer-literal->suffix?
Bin-integer-literal-equiv
Bin-integer-literal-fix
Bin-integer-literalp
Binary
Binary Operations
Binary-*
Binary-+
Binary--
Binary-append
Binary-bitop
Binary-bitop-cofactor1
Binary-bitop-cofactor2
Binary-bitop-swap
Binary-bittest
Binary-digits
Binary-digits-grammar-validation
Binary-digits-std/strings-theorems
Binary-file-load-fn
Binary-integer-literals
Binary-minus-for-gl
Binary-op
Binary-op-add
Binary-op-and
Binary-op-case
Binary-op-div
Binary-op-eq
Binary-op-equiv
Binary-op-fix
Binary-op-ge
Binary-op-gt
Binary-op-iff
Binary-op-implied
Binary-op-implies
Binary-op-kind
Binary-op-le
Binary-op-lt
Binary-op-mul
Binary-op-ne
Binary-op-nonstrictp
Binary-op-or
Binary-op-rem
Binary-op-strictp
Binary-op-sub
Binary-opp
Bind-free
Bind-free-examples
Bind-var
Bind-word-to-bits
Binder
Bindig/uscore
Bindig/uscore-case
Bindig/uscore-digit
Bindig/uscore-digit->get
Bindig/uscore-digit-list
Bindig/uscore-equiv
Bindig/uscore-fix
Bindig/uscore-kind
Bindig/uscore-list
Bindig/uscore-list-equiv
Bindig/uscore-list-fix
Bindig/uscore-list-wfp
Bindig/uscore-listp
Bindig/uscore-listp-basics
Bindig/uscore-p
Bindig/uscore-underscore
Bindig/uscores-to-digits
Binding
Binding
Binding
Binding->expr
Binding->type
Binding->value
Binding->var
Binding->variables
Binding-equiv
Binding-equiv
Binding-equiv
Binding-fix
Binding-fix
Binding-fix
Binding-list
Binding-list-equiv
Binding-list-fix
Binding-listp
Binding-listp-basics
Binding-p
Bindinglist
Bindinglist-equiv
Bindinglist-fix
Bindinglist-p
Bindinglist-p-basics
Bindingp
Bindingp
Bindings
Binify
Binify-width
Binop
Binop-add
Binop-asg
Binop-asg-add
Binop-asg-and
Binop-asg-div
Binop-asg-ior
Binop-asg-mul
Binop-asg-rem
Binop-asg-shl
Binop-asg-shr
Binop-asg-sub
Binop-asg-xor
Binop-bitand
Binop-bitior
Binop-bitxor
Binop-case
Binop-div
Binop-eq
Binop-equiv
Binop-expected-grades
Binop-fix
Binop-ge
Binop-gt
Binop-kind
Binop-le
Binop-list
Binop-list-equiv
Binop-list-fix
Binop-listp
Binop-listp-basics
Binop-logand
Binop-logor
Binop-lt
Binop-mul
Binop-ne
Binop-purep
Binop-rem
Binop-shl
Binop-shr
Binop-strictp
Binop-sub
Binopp
Bip-173
Bip-350
Bip32
Bip32-chain-code
Bip32-chain-code-fix
Bip32-chain-code-p
Bip32-ckd
Bip32-ckd*
Bip32-ckd-priv
Bip32-ckd-priv*
Bip32-ckd-priv-pub
Bip32-ckd-priv-pub-nh
Bip32-ckd-pub
Bip32-ckd-pub*
Bip32-compliant-accounts-for-limit-p
Bip32-compliant-accounts-p
Bip32-compliant-addresses-for-limit-p
Bip32-compliant-addresses-p
Bip32-compliant-chains-p
Bip32-compliant-depth-p
Bip32-compliant-tree-p
Bip32-deserialize-key
Bip32-executable-attachments
Bip32-export-key
Bip32-ext-key
Bip32-ext-key-case
Bip32-ext-key-equiv
Bip32-ext-key-fix
Bip32-ext-key-kind
Bip32-ext-key-p
Bip32-ext-key-priv
Bip32-ext-key-priv->get
Bip32-ext-key-pub
Bip32-ext-key-pub->get
Bip32-ext-priv-key
Bip32-ext-priv-key->chain-code
Bip32-ext-priv-key->key
Bip32-ext-priv-key-equiv
Bip32-ext-priv-key-fix
Bip32-ext-priv-key-p
Bip32-ext-pub-key
Bip32-ext-pub-key->chain-code
Bip32-ext-pub-key->key
Bip32-ext-pub-key-equiv
Bip32-ext-pub-key-fix
Bip32-ext-pub-key-p
Bip32-extend-tree
Bip32-extended-keys
Bip32-get-priv-key-at-path
Bip32-get-pub-key-at-path
Bip32-import-key
Bip32-index-tree
Bip32-index-tree-fix
Bip32-index-treep
Bip32-key-derivation
Bip32-key-fingerprint
Bip32-key-identifier
Bip32-key-serialization
Bip32-key-tree
Bip32-key-tree->index-tree
Bip32-key-tree->root-depth
Bip32-key-tree->root-index
Bip32-key-tree->root-key
Bip32-key-tree->root-parent
Bip32-key-tree-equiv
Bip32-key-tree-fix
Bip32-key-tree-priv-p
Bip32-key-treep
Bip32-key-trees
Bip32-master-key
Bip32-master-key-generation
Bip32-master-tree
Bip32-n
Bip32-path
Bip32-path-in-tree-p
Bip32-path-set
Bip32-path-set-closedp
Bip32-path-set-closedp-exec
Bip32-path-set-closedp-exec-attach
Bip32-path-set-closedp-exec-correctness
Bip32-path-set-closedp-exec-inner
Bip32-path-set-closedp-exec-outer
Bip32-path-set-closedp-executable-attachment
Bip32-path-set-equiv
Bip32-path-setp
Bip32-path-sfix
Bip32-serialization-versions
Bip32-serialize-key
Bip32-serialized-key-p
Bip32-valid-depths-p
Bip32-valid-depths-p-exec
Bip32-valid-depths-p-exec-attach
Bip32-valid-depths-p-exec-correctness
Bip32-valid-depths-p-executable-attachment
Bip32-valid-keys-p
Bip32-valid-keys-p-exec
Bip32-valid-keys-p-exec-attach
Bip32-valid-keys-p-exec-correctness
Bip32-valid-keys-p-executable-attachment
Bip32-wallet-structure
Bip39
Bip39-english-words-bound-p
Bip39-entropy
Bip39-entropy-fix
Bip39-entropy-size-p
Bip39-entropy-to-mnemonic
Bip39-entropy-to-seed
Bip39-entropy-to-word-indexes
Bip39-entropyp
Bip39-mnemonic-to-seed
Bip39-word-indexes-to-words
Bip39-words-to-mnemonic
Bip43
Bip43-export-key
Bip43-import-key
Bip43-key-tree-has-purpose-p
Bip43-purpose
Bip43-purpose-fix
Bip43-purposep
Bip44
Bip44-coin-type
Bip44-coin-type-fix
Bip44-coin-type-p
Bip44-coin-type-set
Bip44-coin-type-set-equiv
Bip44-coin-type-set-fix
Bip44-coin-type-setp
Bip44-coin-types
Bip44-compliant-accounts-for-limit-p
Bip44-compliant-accounts-p
Bip44-compliant-addresses-for-limit-p
Bip44-compliant-addresses-p
Bip44-compliant-chains-p
Bip44-compliant-coins-for-set-p
Bip44-compliant-coins-p
Bip44-compliant-depth-p
Bip44-compliant-tree-p
Birational-montgomery-twisted-edwards
Bird-in-hole
Bird-in-some-hole
Bit Extraction
Bit Slices
Bit Vector Addition
Bit Vectors
Bit->bool
Bit-blasting
Bit-equiv
Bit-list
Bit-list
Bit-list-equiv
Bit-list-equiv
Bit-list-fix
Bit-list-fix
Bit-listp
Bit-listp
Bit-listp-basics
Bit-listp-basics
Bit-size
Bit-size-fix
Bit-size-p
Bit-vectors
Bit/byte/integer-conversions
Bitand-integer-values
Bitand-schar-schar
Bitand-schar-sint
Bitand-schar-sllong
Bitand-schar-slong
Bitand-schar-sshort
Bitand-schar-uchar
Bitand-schar-uint
Bitand-schar-ullong
Bitand-schar-ulong
Bitand-schar-ushort
Bitand-sint-schar
Bitand-sint-sint
Bitand-sint-sllong
Bitand-sint-slong
Bitand-sint-sshort
Bitand-sint-uchar
Bitand-sint-uint
Bitand-sint-ullong
Bitand-sint-ulong
Bitand-sint-ushort
Bitand-sllong-schar
Bitand-sllong-sint
Bitand-sllong-sllong
Bitand-sllong-slong
Bitand-sllong-sshort
Bitand-sllong-uchar
Bitand-sllong-uint
Bitand-sllong-ullong
Bitand-sllong-ulong
Bitand-sllong-ushort
Bitand-slong-schar
Bitand-slong-sint
Bitand-slong-sllong
Bitand-slong-slong
Bitand-slong-sshort
Bitand-slong-uchar
Bitand-slong-uint
Bitand-slong-ullong
Bitand-slong-ulong
Bitand-slong-ushort
Bitand-sshort-schar
Bitand-sshort-sint
Bitand-sshort-sllong
Bitand-sshort-slong
Bitand-sshort-sshort
Bitand-sshort-uchar
Bitand-sshort-uint
Bitand-sshort-ullong
Bitand-sshort-ulong
Bitand-sshort-ushort
Bitand-uchar-schar
Bitand-uchar-sint
Bitand-uchar-sllong
Bitand-uchar-slong
Bitand-uchar-sshort
Bitand-uchar-uchar
Bitand-uchar-uint
Bitand-uchar-ullong
Bitand-uchar-ulong
Bitand-uchar-ushort
Bitand-uint-schar
Bitand-uint-sint
Bitand-uint-sllong
Bitand-uint-slong
Bitand-uint-sshort
Bitand-uint-uchar
Bitand-uint-uint
Bitand-uint-ullong
Bitand-uint-ulong
Bitand-uint-ushort
Bitand-ullong-schar
Bitand-ullong-sint
Bitand-ullong-sllong
Bitand-ullong-slong
Bitand-ullong-sshort
Bitand-ullong-uchar
Bitand-ullong-uint
Bitand-ullong-ullong
Bitand-ullong-ulong
Bitand-ullong-ushort
Bitand-ulong-schar
Bitand-ulong-sint
Bitand-ulong-sllong
Bitand-ulong-slong
Bitand-ulong-sshort
Bitand-ulong-uchar
Bitand-ulong-uint
Bitand-ulong-ullong
Bitand-ulong-ulong
Bitand-ulong-ushort
Bitand-ushort-schar
Bitand-ushort-sint
Bitand-ushort-sllong
Bitand-ushort-slong
Bitand-ushort-sshort
Bitand-ushort-uchar
Bitand-ushort-uint
Bitand-ushort-ullong
Bitand-ushort-ulong
Bitand-ushort-ushort
Bitand-values
Bitarr
Bitarr-copy-cares-to-s32v-col
Bitarr-or-cares-with-s32v-col
Bitarr-to-s32v-col
Bitcoin
Bitior-integer-values
Bitior-schar-schar
Bitior-schar-sint
Bitior-schar-sllong
Bitior-schar-slong
Bitior-schar-sshort
Bitior-schar-uchar
Bitior-schar-uint
Bitior-schar-ullong
Bitior-schar-ulong
Bitior-schar-ushort
Bitior-sint-schar
Bitior-sint-sint
Bitior-sint-sllong
Bitior-sint-slong
Bitior-sint-sshort
Bitior-sint-uchar
Bitior-sint-uint
Bitior-sint-ullong
Bitior-sint-ulong
Bitior-sint-ushort
Bitior-sllong-schar
Bitior-sllong-sint
Bitior-sllong-sllong
Bitior-sllong-slong
Bitior-sllong-sshort
Bitior-sllong-uchar
Bitior-sllong-uint
Bitior-sllong-ullong
Bitior-sllong-ulong
Bitior-sllong-ushort
Bitior-slong-schar
Bitior-slong-sint
Bitior-slong-sllong
Bitior-slong-slong
Bitior-slong-sshort
Bitior-slong-uchar
Bitior-slong-uint
Bitior-slong-ullong
Bitior-slong-ulong
Bitior-slong-ushort
Bitior-sshort-schar
Bitior-sshort-sint
Bitior-sshort-sllong
Bitior-sshort-slong
Bitior-sshort-sshort
Bitior-sshort-uchar
Bitior-sshort-uint
Bitior-sshort-ullong
Bitior-sshort-ulong
Bitior-sshort-ushort
Bitior-uchar-schar
Bitior-uchar-sint
Bitior-uchar-sllong
Bitior-uchar-slong
Bitior-uchar-sshort
Bitior-uchar-uchar
Bitior-uchar-uint
Bitior-uchar-ullong
Bitior-uchar-ulong
Bitior-uchar-ushort
Bitior-uint-schar
Bitior-uint-sint
Bitior-uint-sllong
Bitior-uint-slong
Bitior-uint-sshort
Bitior-uint-uchar
Bitior-uint-uint
Bitior-uint-ullong
Bitior-uint-ulong
Bitior-uint-ushort
Bitior-ullong-schar
Bitior-ullong-sint
Bitior-ullong-sllong
Bitior-ullong-slong
Bitior-ullong-sshort
Bitior-ullong-uchar
Bitior-ullong-uint
Bitior-ullong-ullong
Bitior-ullong-ulong
Bitior-ullong-ushort
Bitior-ulong-schar
Bitior-ulong-sint
Bitior-ulong-sllong
Bitior-ulong-slong
Bitior-ulong-sshort
Bitior-ulong-uchar
Bitior-ulong-uint
Bitior-ulong-ullong
Bitior-ulong-ulong
Bitior-ulong-ushort
Bitior-ushort-schar
Bitior-ushort-sint
Bitior-ushort-sllong
Bitior-ushort-slong
Bitior-ushort-sshort
Bitior-ushort-uchar
Bitior-ushort-uint
Bitior-ushort-ullong
Bitior-ushort-ulong
Bitior-ushort-ushort
Bitior-values
Bitmaskp
Bitnot-integer-value
Bitnot-schar
Bitnot-sint
Bitnot-sllong
Bitnot-slong
Bitnot-sshort
Bitnot-uchar
Bitnot-uint
Bitnot-ullong
Bitnot-ulong
Bitnot-ushort
Bitnot-value
Bitops
Bitops-books
Bitops-compatibility
Bitops/ash-bounds
Bitops/defaults
Bitops/equal-by-logbitp
Bitops/extra-defs
Bitops/fast-logext
Bitops/fast-logrev
Bitops/fast-rotate
Bitops/ihs-extensions
Bitops/ihsext-basics
Bitops/integer-length
Bitops/logbitp-bounds
Bitops/merge
Bitops/parity
Bitops/part-install
Bitops/part-select
Bitops/rotate
Bitops/saturate
Bitops/signed-byte-p
Bitp
Bitp-basics
Bits-0-31
Bits-0-7
Bits-as-digits-in-base-2
Bits-between
Bits-equiv
Bits-length
Bits-to-byte
Bits-to-byte-little
Bits/bytes-digit-grouping
Bits/ubyte11s-digit-grouping
Bits=>bebytes
Bits=>beubyte11s
Bits=>lebytes
Bits=>leubyte11s
Bitscan-fwd
Bitscan-rev
Bitset-binary-intersect
Bitset-binary-union
Bitset-cardinality
Bitset-delete
Bitset-difference
Bitset-insert
Bitset-intersect
Bitset-intersectp
Bitset-list
Bitset-list*
Bitset-memberp
Bitset-members
Bitset-singleton
Bitset-subsetp
Bitset-union
Bitsets
Bitxor-integer-values
Bitxor-schar-schar
Bitxor-schar-sint
Bitxor-schar-sllong
Bitxor-schar-slong
Bitxor-schar-sshort
Bitxor-schar-uchar
Bitxor-schar-uint
Bitxor-schar-ullong
Bitxor-schar-ulong
Bitxor-schar-ushort
Bitxor-sint-schar
Bitxor-sint-sint
Bitxor-sint-sllong
Bitxor-sint-slong
Bitxor-sint-sshort
Bitxor-sint-uchar
Bitxor-sint-uint
Bitxor-sint-ullong
Bitxor-sint-ulong
Bitxor-sint-ushort
Bitxor-sllong-schar
Bitxor-sllong-sint
Bitxor-sllong-sllong
Bitxor-sllong-slong
Bitxor-sllong-sshort
Bitxor-sllong-uchar
Bitxor-sllong-uint
Bitxor-sllong-ullong
Bitxor-sllong-ulong
Bitxor-sllong-ushort
Bitxor-slong-schar
Bitxor-slong-sint
Bitxor-slong-sllong
Bitxor-slong-slong
Bitxor-slong-sshort
Bitxor-slong-uchar
Bitxor-slong-uint
Bitxor-slong-ullong
Bitxor-slong-ulong
Bitxor-slong-ushort
Bitxor-sshort-schar
Bitxor-sshort-sint
Bitxor-sshort-sllong
Bitxor-sshort-slong
Bitxor-sshort-sshort
Bitxor-sshort-uchar
Bitxor-sshort-uint
Bitxor-sshort-ullong
Bitxor-sshort-ulong
Bitxor-sshort-ushort
Bitxor-uchar-schar
Bitxor-uchar-sint
Bitxor-uchar-sllong
Bitxor-uchar-slong
Bitxor-uchar-sshort
Bitxor-uchar-uchar
Bitxor-uchar-uint
Bitxor-uchar-ullong
Bitxor-uchar-ulong
Bitxor-uchar-ushort
Bitxor-uint-schar
Bitxor-uint-sint
Bitxor-uint-sllong
Bitxor-uint-slong
Bitxor-uint-sshort
Bitxor-uint-uchar
Bitxor-uint-uint
Bitxor-uint-ullong
Bitxor-uint-ulong
Bitxor-uint-ushort
Bitxor-ullong-schar
Bitxor-ullong-sint
Bitxor-ullong-sllong
Bitxor-ullong-slong
Bitxor-ullong-sshort
Bitxor-ullong-uchar
Bitxor-ullong-uint
Bitxor-ullong-ullong
Bitxor-ullong-ulong
Bitxor-ullong-ushort
Bitxor-ulong-schar
Bitxor-ulong-sint
Bitxor-ulong-sllong
Bitxor-ulong-slong
Bitxor-ulong-sshort
Bitxor-ulong-uchar
Bitxor-ulong-uint
Bitxor-ulong-ullong
Bitxor-ulong-ulong
Bitxor-ulong-ushort
Bitxor-ushort-schar
Bitxor-ushort-sint
Bitxor-ushort-sllong
Bitxor-ushort-slong
Bitxor-ushort-sshort
Bitxor-ushort-uchar
Bitxor-ushort-uint
Bitxor-ushort-ullong
Bitxor-ushort-ulong
Bitxor-ushort-ushort
Bitxor-values
Blake2-hash
Blake2s-256
Blankargs
Block
Block->statements
Block-count
Block-dead
Block-equiv
Block-fix
Block-item
Block-item-case
Block-item-count
Block-item-declon
Block-item-declon->get
Block-item-equiv
Block-item-fix
Block-item-kind
Block-item-list
Block-item-list-equiv
Block-item-list-fix
Block-item-listp
Block-item-listp-basics
Block-item-stmt
Block-item-stmt->get
Block-itemp
Block-loopinit
Block-nofunp
Block-noloopinitp
Block-option
Block-option-case
Block-option-count
Block-option-dead
Block-option-equiv
Block-option-fix
Block-option-loopinit
Block-option-nofunp
Block-option-noloopinitp
Block-option-none
Block-option-renamefun
Block-option-renamevar
Block-option-some
Block-option-some->val
Block-option-unique-funs
Block-option-unique-vars
Block-optionp
Block-renamefun
Block-renamevar
Block-result
Block-result-equiv
Block-result-err
Block-result-err->get
Block-result-fix
Block-result-kind
Block-result-ok
Block-result-ok->get
Block-resultp
Block-unique-funs
Block-unique-vars
Blockp
Blockquote
Bls12-377-domain-parameters
Bls12-377-parameter-x
Bls12-377-scalar-field-prime
Bls12-381-scalar-field-prime
Bn-254-group-prime
Body
Book-compiled-file
Book-contents
Book-example
Book-hash
Book-hash-mismatch
Book-makefiles
Book-name
Book-runes-alist
Bookdata
Books
Books-certification
Books-certification-alt
Books-certification-classic
Books-reference
Books-tour
Bool
Bool->bit
Bool->get
Bool->sign
Bool->vec
Bool-and
Bool-eq
Bool-equiv
Bool-fix
Bool-fix
Bool-ne
Bool-not
Bool-or
Boole$
Boolean-and
Boolean-array
Boolean-array->components
Boolean-array-equiv
Boolean-array-fix
Boolean-array-from-boolean-list
Boolean-array-index-in-range-p
Boolean-array-length
Boolean-array-new-init
Boolean-array-new-len
Boolean-array-read
Boolean-array-to-boolean-list
Boolean-array-write
Boolean-arrayp
Boolean-convention
Boolean-eq
Boolean-from-schar
Boolean-from-sint
Boolean-from-sllong
Boolean-from-slong
Boolean-from-sshort
Boolean-from-uchar
Boolean-from-uint
Boolean-from-ullong
Boolean-from-ulong
Boolean-from-ushort
Boolean-ior
Boolean-list
Boolean-list-equiv
Boolean-list-fix
Boolean-listp
Boolean-listp-basics
Boolean-literal-tree
Boolean-literalp
Boolean-literalp-is-grammar-boolean-literalp
Boolean-literalp-when-grammar-boolean-literalp
Boolean-literals
Boolean-literals-grammar-validation
Boolean-neq
Boolean-not
Boolean-operations
Boolean-operations
Boolean-reasoning
Boolean-result
Boolean-result
Boolean-result-equiv
Boolean-result-equiv
Boolean-result-err
Boolean-result-err
Boolean-result-err->get
Boolean-result-err->get
Boolean-result-fix
Boolean-result-fix
Boolean-result-kind
Boolean-result-kind
Boolean-result-ok
Boolean-result-ok
Boolean-result-ok->get
Boolean-result-ok->get
Boolean-resultp
Boolean-resultp
Boolean-value
Boolean-value->bool
Boolean-value-equiv
Boolean-value-fix
Boolean-value-list
Boolean-value-list-equiv
Boolean-value-list-fix
Boolean-value-listp
Boolean-value-listp-basics
Boolean-valuep
Boolean-values
Boolean-xor
Booleanp
Boolp
Bools->int
Boothpipe-run
Bounded-lit-fix
Bounders
Boundrw-subst
Boundrw-subst->alist
Boundrw-subst->lhs
Boundrw-subst->rhs
Boundrw-subst-p
Boundrw-substlist-p
Boundrw-substlist-p-basics
Bounds-of-integer-values
Box
Br
Branch
Branch->action
Branch->condition
Branch-count
Branch-equiv
Branch-fix
Branch-list
Branch-list->condition-list
Branch-list-equiv
Branch-list-fix
Branch-listp
Branch-listp-basics
Branches-same-under-mask-p
Branchp
Break$
Break-lemma
Break-on-error
Break-rewrite
Breaks
Bridge
Broken-link
Broken-link-table
Brr
Brr-commands
Brr-evisc-tuple
Brr-near-missp
Brr@
Bsp
Bsp-position
Bsp-size
Bspp
Build
Build-lt
Build-the-manual
Building-ACL2
Building-an-ipasir-solver-library
Built-in-clause
Built-ins
Builtin-defaxioms
Builtin-defaxioms/defthms
Builtin-defaxioms/defthms-about-alists
Builtin-defaxioms/defthms-about-apply$
Builtin-defaxioms/defthms-about-arrays
Builtin-defaxioms/defthms-about-bad-atoms
Builtin-defaxioms/defthms-about-booleans
Builtin-defaxioms/defthms-about-characters
Builtin-defaxioms/defthms-about-cons-pairs
Builtin-defaxioms/defthms-about-eqlables
Builtin-defaxioms/defthms-about-io
Builtin-defaxioms/defthms-about-lists
Builtin-defaxioms/defthms-about-logical-connectives
Builtin-defaxioms/defthms-about-numbers
Builtin-defaxioms/defthms-about-ordinals
Builtin-defaxioms/defthms-about-random$
Builtin-defaxioms/defthms-about-strings
Builtin-defaxioms/defthms-about-symbols
Builtin-defaxioms/defthms-about-system-utilities
Builtin-defaxioms/defthms-about-tau
Builtin-defaxioms/defthms-about-total-order
Builtin-defaxioms/defthms-by-rule-classes
Builtin-defaxioms/defthms-by-types/functions
Builtin-defaxioms/defthms-of-class-built-in-clause
Builtin-defaxioms/defthms-of-class-clause-processor
Builtin-defaxioms/defthms-of-class-compound-recognizer
Builtin-defaxioms/defthms-of-class-congruence
Builtin-defaxioms/defthms-of-class-definition
Builtin-defaxioms/defthms-of-class-elim
Builtin-defaxioms/defthms-of-class-equivalence
Builtin-defaxioms/defthms-of-class-forward-chaining
Builtin-defaxioms/defthms-of-class-generalize
Builtin-defaxioms/defthms-of-class-induction
Builtin-defaxioms/defthms-of-class-linear
Builtin-defaxioms/defthms-of-class-meta
Builtin-defaxioms/defthms-of-class-refinement
Builtin-defaxioms/defthms-of-class-rewrite
Builtin-defaxioms/defthms-of-class-rewrite-quoted-constant
Builtin-defaxioms/defthms-of-class-tau-system
Builtin-defaxioms/defthms-of-class-type-prescription
Builtin-defaxioms/defthms-of-class-type-set-inverter
Builtin-defaxioms/defthms-of-class-well-founded-relation
Builtin-defaxioms/defthms-without-rule-classes
Builtin-defthms
Builtins
Bump-all-meta-rules
Bump-down-rule
Bump-rule
Bump-rules
Butlast
Bv
Bvar-db-consistency-error
Bvar-db-consistency-error-case
Bvar-db-consistency-error-equiv
Bvar-db-consistency-error-eval-error
Bvar-db-consistency-error-eval-error->msg
Bvar-db-consistency-error-eval-error->obj
Bvar-db-consistency-error-fix
Bvar-db-consistency-error-inconsistency
Bvar-db-consistency-error-inconsistency->obj
Bvar-db-consistency-error-inconsistency->obj-val
Bvar-db-consistency-error-inconsistency->var-val
Bvar-db-consistency-error-kind
Bvar-db-consistency-error-p
Bvar-db-consistency-errorlist
Bvar-db-consistency-errorlist-equiv
Bvar-db-consistency-errorlist-fix
Bvar-db-consistency-errorlist-p
Bvar-db-consistency-errorlist-p-basics
Bvchop
Bvec
Bvminus
Bvplus
Bvuminus
By
Byte
Byte
Byte-array
Byte-array->components
Byte-array-equiv
Byte-array-fix
Byte-array-from-sbyte8-list
Byte-array-index-in-range-p
Byte-array-length
Byte-array-new-init
Byte-array-new-len
Byte-array-read
Byte-array-to-sbyte8-list
Byte-array-write
Byte-arrayp
Byte-arrays
Byte-fix
Byte-fix
Byte-list
Byte-list-equiv
Byte-list-fix
Byte-list20
Byte-list20-fix
Byte-list20p
Byte-list32
Byte-list32-fix
Byte-list32p
Byte-list64
Byte-list64-fix
Byte-list64p
Byte-listp
Byte-listp
Byte-listp-basics
Byte-sequences
Byte-to-bits
Byte-to-bits-little
Byte-to-char
Byte-to-double
Byte-to-float
Byte-to-int
Byte-to-long
Byte-to-short
Byte-value
Byte-value->int
Byte-value-equiv
Byte-value-fix
Byte-value-list
Byte-value-list-equiv
Byte-value-list-fix
Byte-value-listp
Byte-value-listp-basics
Byte-valuep
Bytelist-bytelist-map
Bytelist-bytelist-mapp
Bytelist-bytelist-mequiv
Bytelist-bytelist-mfix
Bytelist-to-nibblelist-keys
Bytelist-to-nibblelist-keys-aux
Bytep
Bytep
Bytep-additional-theorems
Bytes
Bytes
Bytes
Bytes->charlist
Bytes->string
Bytes-as-digits-in-base-256
C
Caaaar
Caaadr
Caaar
Caadar
Caaddr
Caadr
Caar
Cadaar
Cadadr
Cadar
Caddar
Cadddr
Caddr
Cadr
Calc-trans-rules-of-names
Calist
Calist-equiv
Calist-fix
Calistp
Call-gate-descriptor-attributesbits
Call-gate-descriptor-attributesbits->dpl
Call-gate-descriptor-attributesbits->p
Call-gate-descriptor-attributesbits->s
Call-gate-descriptor-attributesbits->type
Call-gate-descriptor-attributesbits->unknownbits
Call-gate-descriptor-attributesbits-debug
Call-gate-descriptor-attributesbits-equiv-under-mask
Call-gate-descriptor-attributesbits-fix
Call-gate-descriptor-attributesbits-p
Call-gate-descriptorbits
Call-gate-descriptorbits->all-zeroes?
Call-gate-descriptorbits->dpl
Call-gate-descriptorbits->offset15-0
Call-gate-descriptorbits->offset31-16
Call-gate-descriptorbits->offset63-32
Call-gate-descriptorbits->p
Call-gate-descriptorbits->res1
Call-gate-descriptorbits->res2
Call-gate-descriptorbits->res3
Call-gate-descriptorbits->s
Call-gate-descriptorbits->selector
Call-gate-descriptorbits->type
Call-gate-descriptorbits-debug
Call-gate-descriptorbits-equiv-under-mask
Call-gate-descriptorbits-fix
Call-gate-descriptorbits-p
Call-primitive-function
Calling-ld-in-bad-contexts
Cancel-equal-+-*
Cancel-parity-lits
Candidate-assign
Candidate-assign->edge
Candidate-assign->val
Candidate-assign-equiv
Candidate-assign-fix
Candidate-assign-p
Candidate-assigns
Candidate-assigns-equiv
Candidate-assigns-fix
Candidate-assigns-p
Candidate-assigns-p-basics
Candidate-ids
Candidate-with-least-nth-place-votes
Candidates-for-propagation
Candidates-with-min-votes
Canonical-address-listp
Canonical-address-p
Canonical-hints-specifier-p
Canonical-pathname
Canonicalize-alias-pairs
Canonicalize-hints-specifier
Canonicalize-to-q-ite
Cap-length
Captures-bindings
Car
Cardinality
Cardinality
Caremask
Carry-out
Carry-out-bit
Case
Case-match
Case-split
Case-split-limitations
Case-splitting
Case-statement-problems
Caseelim
Cases
Cases
Casesplit
Casesplit-alist
Casesplit-alist-equiv
Casesplit-alist-fix
Casesplit-alist-p
Casesplit-event-generation
Casesplit-fn
Casesplit-gen-appcond-cond-guard
Casesplit-gen-appcond-cond-guard-name
Casesplit-gen-appcond-name-from-parts
Casesplit-gen-appcond-new-guard
Casesplit-gen-appcond-new-guard-name
Casesplit-gen-appcond-thm-hyp
Casesplit-gen-appcond-thm-hyp-name
