• 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
  • %-
  • %.
  • %.-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-concrete-syntax-rules*
  • *all-http-grammar-rules*
  • *all-http-message-grammar-rules*
  • *all-json-grammar-rules*
  • *all-uri-grammar-rules*
  • *alpha*
  • *alternation*
  • *atc-all-rules*
  • *atc-allowed-options*
  • *atc-array-read-return-rewrite-rules*
  • *atc-array-read-type-prescription-rules*
  • *atc-boolean-from-type-fns*
  • *atc-compound-recognizer-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-rules*
  • *atc-exec-expr-call-or-pure-rules*
  • *atc-exec-expr-pure-list-rules*
  • *atc-exec-expr-pure-rules*
  • *atc-exec-fun-rules*
  • *atc-exec-ident-rules*
  • *atc-exec-stmt-rules*
  • *atc-exec-test-rules*
  • *atc-exec-unary-rules*
  • *atc-identifier-rules*
  • *atc-init-scope-rules*
  • *atc-integer-conv-rules*
  • *atc-integer-convs-return-rewrite-rules*
  • *atc-integer-convs-type-prescription-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-integer-types*
  • *atc-integer-value-rules*
  • *atc-more-rewrite-rules*
  • *atc-not-rules*
  • *atc-op-type-fns*
  • *atc-op-type1-type2-fns*
  • *atc-other-definition-rules*
  • *atc-other-executable-counterpart-rules*
  • *atc-other-rewrite-rules*
  • *atc-promote-value-rules*
  • *atc-symbolic-computation-state-rules*
  • *atc-table*
  • *atc-type-base-const-fns*
  • *atc-type-prescription-rules*
  • *atc-type1-from-type2-fns*
  • *atc-uaconvert-values-rules*
  • *atc-value-listp-rules*
  • *atc-value-optionp-rules*
  • *atc-valuep-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*
  • *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*
  • *c-nl*
  • *c-wsp*
  • *case-insensitive-string*
  • *case-sensitive-string*
  • *char*
  • *char-val*
  • *ckeywords*
  • *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-abstracted*
  • *concrete-syntax-rules-parse-tree*
  • *core-rules*
  • *core-rules-abstracted*
  • *core-rules-parse-tree*
  • *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*
  • *defdigits-table-name*
  • *defined-as*
  • *definterface-hash-table-name*
  • *definterface-hmac-table-name*
  • *defmapping-table-name*
  • *demo-usage*
  • *demo2-opts-usage*
  • *digit*
  • *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-new*
  • *grammar-old*
  • *grammar-parser-error-msg*
  • *group*
  • *hex-val*
  • *hexdig*
  • *htab*
  • *http-grammar-rules*
  • *imap-grammar-rules*
  • *imf-grammar-rules*
  • *jkeywords*
  • *json-grammar-rules*
  • *jubjub-l*
  • *key-path-prefix*
  • *l-merkle-sapling*
  • *lexical-grammar*
  • *lf*
  • *logops-functions*
  • *lwsp*
  • *newline*
  • *nls*
  • *nls*
  • *not-toohard-ops*
  • *null-literal*
  • *num-val*
  • *octet*
  • *option*
  • *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*
  • *smt-architecture*
  • *smt-basics*
  • *smt-functions*
  • *smt-types*
  • *smt-uninterpreted-types*
  • *smtp-grammar-rules*
  • *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-&amp*
  • *vl-html-&gt*
  • *vl-html-&lt*
  • *vl-html-&nbsp*
  • *vl-html-&quot*
  • *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->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*
  • +
  • -
  • /
  • /=
  • /_
  • /_-fn
  • 0f-38-three-byte-opcodes-map
  • 0f-3a-three-byte-opcodes-map
  • 1*_
  • 1+
  • 1-
  • 1. An Example GL Proof
  • 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
  • 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-1x
  • 4vec-1z
  • 4vec-==
  • 4vec-===
  • 4vec-===*
  • 4vec-?
  • 4vec-?!
  • 4vec-?*
  • 4vec-[=
  • 4vec-assigns
  • 4vec-assigns-equiv
  • 4vec-assigns-fix
  • 4vec-assigns-p
  • 4vec-bit-extract
  • 4vec-bit-index
  • 4vec-bit?
  • 4vec-bit?!
  • 4vec-bitand
  • 4vec-bitnot
  • 4vec-bitor
  • 4vec-bitxor
  • 4vec-boolmaskp
  • 4vec-clog2
  • 4vec-concat
  • 4vec-countones
  • 4vec-driver
  • 4vec-driver->strength
  • 4vec-driver->value
  • 4vec-driver-equiv
  • 4vec-driver-fix
  • 4vec-driver-p
  • 4vec-driverlist
  • 4vec-driverlist-equiv
  • 4vec-driverlist-fix
  • 4vec-driverlist-p
  • 4vec-driverlist-p-basics
  • 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-netassigns
  • 4vec-netassigns-equiv
  • 4vec-netassigns-fix
  • 4vec-netassigns-p
  • 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-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-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::casesplit
  • ACL2-pc::cg
  • ACL2-pc::change-goal
  • ACL2-pc::cl-proc
  • ACL2-pc::claim
  • 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::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::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::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::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::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::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-defaults
  • 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
  • Abelian-groups
  • Abelian-semigroups
  • Abnf
  • Abnf-tree-list-with-root-p
  • Abnf-tree-list-with-root-p-basics
  • Abnf-tree-with-root-p
  • 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-sensitive/insensitive-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-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-binop
  • Add-commutativity-2
  • 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
  • Add-funs-in-statement-list
  • Add-funtype
  • Add-funtypes-in-statement-list
  • Add-hypo-cp
  • Add-include-book-dir
  • Add-include-book-dir!
  • 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-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-to-fn
  • Add-suffix-to-fn-or-const
  • 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-var
  • Add-var
  • Add-var-value
  • Add-vars
  • 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-option
  • Address-option-case
  • Address-option-equiv
  • Address-option-fix
  • Address-option-none
  • Address-option-some
  • Address-option-some->val
  • Address-optionp
  • Address-p
  • Address-p
  • Addresses
  • Addressing-method-code-p
  • Addresslist
  • Addresslist-equiv
  • Addresslist-fix
  • Addresslist-p
  • Addresslist-p-basics
  • Addressp
  • Adjacent-p
  • 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-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
  • 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
  • Alpha-char-p
  • Alpha/digit-char-p
  • Alpha/digit-charlist-p
  • Alpha/digit-charlist-p-basics
  • Alpha/digit-chars
  • Alpha/digit/dash-char-p
  • Alpha/digit/dash-charlist-p
  • Alpha/digit/dash-charlist-p-basics
  • Alpha/digit/dash-chars
  • Alpha/digit/uscore/dollar-char-p
  • Alpha/digit/uscore/dollar-charlist-p
  • Alpha/digit/uscore/dollar-charlist-p-basics
  • Alpha/digit/uscore/dollar-chars
  • Alpha/uscore/dollar-char-p
  • Alpha/uscore/dollar-charlist-p
  • Alpha/uscore/dollar-charlist-p-basics
  • Alpha/uscore/dollar-chars
  • 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-introduction
  • 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*
  • And-node
  • And-node->fanin0
  • And-node->fanin1
  • And4
  • Annotate
  • Annotate
  • Annotated-ACL2-scripts
  • 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
  • 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
  • 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/nat-listp
  • Arithmetic/natp-posp
  • Arithmetic/rational-listp
  • Arities-okp
  • Arity
  • Arity+
  • Arity-reasoning
  • Array
  • Array
  • Array-equiv
  • Array-fieldinfo
  • Array-fieldinfo->size-key
  • Array-fieldinfo->tr-key
  • Array-fieldinfo-p
  • Array-fix
  • Array-kind
  • Array-length
  • Array-result
  • Array-result-equiv
  • Array-result-err
  • Array-result-err->get
  • Array-result-fix
  • Array-result-kind
  • Array-result-ok
  • Array-result-ok->get
  • Array-resultp
  • Array-schar
  • Array-schar->get
  • Array-sint
  • Array-sint->get
  • Array-sllong
  • Array-sllong->get
  • Array-slong
  • Array-slong->get
  • Array-sshort
  • Array-sshort->get
  • 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-uchar
  • Array-uchar->get
  • Array-uint
  • Array-uint->get
  • Array-ullong
  • Array-ullong->get
  • Array-ulong
  • Array-ulong->get
  • Array-ushort
  • Array-ushort->get
  • Array1
  • Array1-disabled-lemmas
  • Array1-functions
  • Array1-lemmas
  • Array1p
  • Array2p
  • Arrayp
  • 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-listp
  • Assertion-listp-basics
  • Assertionp
  • Assertions
  • Assign
  • Assign
  • Assign->netassigns
  • Assignment
  • Assignment-equiv
  • Assignment-fix
  • Assignment-for-prime-p
  • Assignment-list
  • Assignment-list-equiv
  • Assignment-list-fix
  • Assignment-listp
  • Assignment-listp-basics
  • 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
  • Atc
  • Atc-abstract-syntax
  • Atc-abstract-syntax-operations
  • Atc-add-var
  • Atc-affecting-term-for-let-p
  • Atc-arrays
  • 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-iconst
  • Atc-check-let
  • Atc-check-loop-call
  • Atc-check-new-function-name
  • Atc-check-sint-from-boolean
  • Atc-check-symbol-2part
  • Atc-check-symbol-3part
  • Atc-check-symbol-4part
  • Atc-check-unop
  • Atc-check-var
  • Atc-computation-states
  • Atc-conditional-expressions
  • Atc-def-integer-arrays
  • Atc-def-integer-arrays-indices
  • Atc-def-integer-arrays-loop-inner
  • Atc-def-integer-arrays-loop-outer
  • Atc-def-integer-bits
  • Atc-def-integer-bits-linear-rule
  • Atc-def-integer-conversion
  • Atc-def-integer-conversions-loop-inner
  • Atc-def-integer-conversions-loop-outer
  • Atc-def-integer-operations-1
  • Atc-def-integer-operations-1-loop
  • Atc-def-integer-operations-2
  • Atc-def-integer-operations-2-loop-inner
  • Atc-def-integer-operations-2-loop-outer
  • Atc-def-integer-operations-2-loop-same
  • Atc-def-integer-values
  • Atc-def-integer-values-loop
  • Atc-defun-integer
  • Atc-distributivity-over-if-rewrite-rules
  • Atc-dynamic-semantics
  • Atc-errors
  • 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-rules
  • Atc-exec-expr-call-or-pure-rules
  • Atc-exec-expr-pure-list-rules
  • Atc-exec-expr-pure-rules
  • Atc-exec-fun-rules
  • Atc-exec-ident-rules
  • Atc-exec-stmt-rules
  • Atc-exec-test-rules
  • Atc-exec-unary-rules
  • Atc-exec-unary-rules-generation
  • Atc-execution
  • Atc-execution-rules
  • Atc-find-affected
  • Atc-fn
  • Atc-fn-info
  • Atc-fn-info->affect
  • Atc-fn-info->correct-thm
  • Atc-fn-info->fun-env-thm
  • 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-pointer-listp
  • Atc-formal-pointer-listp-basics
  • Atc-formal-pointerp
  • Atc-function-environments
  • Atc-gen-appconds
  • Atc-gen-bindings-for-cfun-formals
  • Atc-gen-bindings-for-loop-formals
  • Atc-gen-cfun-correct-thm
  • Atc-gen-cfun-fun-env-thm
  • Atc-gen-everything
  • Atc-gen-exec-stmt-while-for-loop
  • Atc-gen-expr-bool
  • Atc-gen-expr-cval
  • Atc-gen-expr-cval-pure
  • Atc-gen-expr-cval-pure-list
  • Atc-gen-expr-pure
  • Atc-gen-ext-declon
  • Atc-gen-ext-declon-list
  • Atc-gen-file
  • Atc-gen-file-event
  • Atc-gen-fn-result-thm
  • Atc-gen-init-fun-env-thm
  • 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-param-declon-list
  • Atc-gen-print-result
  • Atc-gen-print-result-aux
  • Atc-gen-prog-const
  • Atc-gen-stmt
  • Atc-gen-transunit
  • Atc-gen-tyspecseq
  • Atc-gen-wf-thm
  • Atc-get-var
  • Atc-get-var-check-innermost
  • Atc-get-vars
  • Atc-get-vars-check-innermost
  • Atc-ident-char-listp
  • Atc-ident-stringp
  • Atc-identifier-rules
  • Atc-implementation
  • Atc-init-scope-rules
  • Atc-input-processing
  • Atc-integer-conv-rules
  • Atc-integer-conversions
  • Atc-integer-conversions-signed-from-unsigned-okp
  • Atc-integer-fixtype-to-type
  • Atc-integer-formats
  • Atc-integer-operations
  • Atc-integer-size-rules
  • Atc-integer-type-bits
  • Atc-integer-type-fixtype
  • Atc-integer-type-minbits
  • Atc-integer-type-string
  • Atc-integer-value-rules
  • Atc-integers
  • Atc-let-designations
  • Atc-letter/digit/uscore-char-listp
  • Atc-letter/digit/uscore-char-listp-basics
  • Atc-letter/digit/uscore-char-p
  • Atc-loop-body-term-subst
  • Atc-macro-definition
  • Atc-make-mv-nth-terms
  • Atc-maybe-call-infop
  • Atc-not-rules
  • Atc-other-rewrite-rules
  • Atc-pointers
  • Atc-portable-ascii-identifiers
  • Atc-pretty-printer
  • Atc-process-const-name
  • Atc-process-const-name-aux
  • Atc-process-fn1...fnp
  • Atc-process-function
  • Atc-process-function-list
  • Atc-process-inputs
  • Atc-process-output-file
  • Atc-promote-value-rules
  • Atc-proof-support
  • Atc-pure-c-valued-termp
  • Atc-shallow-embedding
  • Atc-static-semantics
  • Atc-stmt-noncval-termp
  • 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-type-alist
  • Atc-symbol-type-alist-equiv
  • Atc-symbol-type-alist-fix
  • Atc-symbol-type-alist-list
  • Atc-symbol-type-alist-list-equiv
  • Atc-symbol-type-alist-list-fix
  • Atc-symbol-type-alist-listp
  • Atc-symbol-type-alist-listp-basics
  • Atc-symbol-type-alistp
  • Atc-symbolic-computation-state-rules
  • Atc-symbolic-computation-states
  • Atc-syntaxp-hyp-for-expr-pure
  • Atc-table
  • Atc-table-definition
  • Atc-table-lookup
  • Atc-table-record-event
  • Atc-term-recognizers
  • 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-type-predicate
  • Atc-typed-formals
  • Atc-types
  • Atc-uaconvert-rules-generation
  • Atc-uaconvert-values-rules
  • Atc-update-var-term-alist
  • Atc-value-listp-rules
  • Atc-value-optionp-rules
  • Atc-valuep-rules
  • Atc-values
  • Atc-var-assignablep
  • Atc-vars-assignablep
  • 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-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-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-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
  • Atj-post-translation
  • 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-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-output-dir
  • 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
  • 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+
  • 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
  • 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->expr
  • Binding->type
  • Binding->var
  • Binding-equiv
  • Binding-equiv
  • 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
  • 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
  • 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-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
  • Bitarr
  • Bitarr-copy-cares-to-s32v-col
  • Bitarr-or-cares-with-s32v-col
  • Bitarr-to-s32v-col
  • Bitcoin
  • 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
  • Bitmaskp
  • Bitnot-schar
  • Bitnot-sint
  • Bitnot-sllong
  • Bitnot-slong
  • Bitnot-sshort
  • Bitnot-uchar
  • Bitnot-uint
  • Bitnot-ullong
  • Bitnot-ulong
  • Bitnot-ushort
  • 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-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
  • 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-option
  • Block-option-case
  • Block-option-count
  • Block-option-dead
  • Block-option-equiv
  • Block-option-fix
  • Block-option-loopinit
  • Block-option-none
  • Block-option-some
  • Block-option-some->val
  • Block-optionp
  • 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
  • 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-equiv
  • Boolean-result-err
  • Boolean-result-err->get
  • Boolean-result-fix
  • Boolean-result-kind
  • Boolean-result-ok
  • Boolean-result-ok->get
  • 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-direct
  • Boothpipe-step1
  • Boothpipe-step2
  • Bounded-lit-fix
  • Bounders
  • Box
  • Br
  • Branches-same-under-mask-p
  • Break$
  • Break-lemma
  • Break-on-error
  • Break-rewrite
  • Breaks
  • Bridge
  • Broken-link
  • Broken-link-table
  • Brr
  • Brr-commands
  • Brr-evisc-tuple
  • Brr@
  • Bsp
  • Bsp-position
  • Bsp-size
  • Bspp
  • Build
  • Build-lt
  • Build-the-manual
  • Building-ACL2
  • Building-an-ipasir-solver-library
  • Built-in-clause
  • Built-in-theorems
  • Built-in-theorems-about-alists
  • Built-in-theorems-about-arithmetic
  • Built-in-theorems-about-arrays
  • Built-in-theorems-about-bad-atoms
  • Built-in-theorems-about-booleans
  • Built-in-theorems-about-characters
  • Built-in-theorems-about-cons-pairs
  • Built-in-theorems-about-eqlables
  • Built-in-theorems-about-lists
  • Built-in-theorems-about-logical-connectives
  • Built-in-theorems-about-random$
  • Built-in-theorems-about-strings
  • Built-in-theorems-about-symbols
  • Built-in-theorems-about-system-utilities
  • Built-in-theorems-about-total-order
  • Built-in-theorems-for-tau
  • Built-ins
  • 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
  • Casesplit-gen-appconds
  • Casesplit-gen-appconds-cond-guard
  • Casesplit-gen-appconds-new-guard
  • Casesplit-gen-appconds-new-guard-aux
  • Casesplit-gen-appconds-thm-hyp
  • Casesplit-gen-everything
  • Casesplit-gen-new-fn
  • Casesplit-gen-old-to-new-thm
  • Casesplit-implementation
  • Casesplit-input-processing
  • Casesplit-library-extensions
  • Casesplit-macro-definition
  • Casesplit-process-condition
  • Casesplit-process-conditions
  • Casesplit-process-inputs
  • Casesplit-process-old
  • Casesplit-process-theorem
  • Casesplit-process-theorems
  • Casesplit-process-thm-name
  • Cat
  • Catpath
  • Catpaths
  • Cbd
  • Cblock
  • Cblock-expression-building
  • Cblock-path-checking
  • Ccg
  • Ccg-xargs
  • Ccl-installation
  • Ccl-installation-extra
  • Ccl-installation-linux-brief
  • Ccl-installation-linux-elaborate
  • Ccl-installation-mac-brief
  • Ccl-installation-mac-elaborate
  • Ccl-only
  • Ccl-updates
  • Cdaaar
  • Cdaadr
  • Cdaar
  • Cdadar
  • Cdaddr
  • Cdadr
  • Cdar
  • Cddaar
  • Cddadr
  • Cddar
  • Cdddar
  • Cddddr
  • Cdddr
  • Cddr
  • Cdr
  • Cdr-cdr-induct
  • Cdr-dec-induct
  • Cdr-induct
  • Ceiling
  • Cert-pl-on-windows
  • Cert.pl
  • Cert_param
  • Certificate
  • Certify-book
  • Certify-book!
  • Certify-book-debug
  • Certify-book-failure
  • Certifying-books
  • Certifying-simple-books
  • Cf-spec16
  • Cf-spec32
  • Cf-spec64
  • Cf-spec8
  • Cgen
  • Cgen-local-timeout
  • Cgen-single-test-timeout
  • Cgen-timeout
  • Cgen::flush
  • Cgraph
  • Cgraph-alist
  • Cgraph-alist-equiv
  • Cgraph-alist-fix
  • Cgraph-alist-p
  • Cgraph-derivstate
  • Cgraph-derivstate->result-msg
  • Cgraph-derivstate->times-seen
  • Cgraph-derivstate-equiv
  • Cgraph-derivstate-fix
  • Cgraph-derivstate-p
  • Cgraph-derivstates
  • Cgraph-derivstates-equiv
  • Cgraph-derivstates-fix
  • Cgraph-derivstates-p
  • Cgraph-edge
  • Cgraph-edge->match-vars
  • Cgraph-edge->rule
  • Cgraph-edge->subst
  • Cgraph-edge-equiv
  • Cgraph-edge-fix
  • Cgraph-edge-p
  • Cgraph-edgelist
  • Cgraph-edgelist-equiv
  • Cgraph-edgelist-fix
  • Cgraph-edgelist-p
  • Cgraph-edgelist-p-basics
  • Cgraph-equiv
  • Cgraph-fix
  • Cgraph-p
  • Change
  • Change-4vec-driver
  • Change-a4vec
  • Change-abc-comb-simp-config
  • Change-addnames-indices
  • Change-address
  • Change-address
  • Change-address-option-none
  • Change-address-option-some
  • Change-aexp-add
  • Change-aexp-const
  • Change-aexp-mul
  • Change-aexp-var
  • Change-aig2c-config
  • Change-alias
  • Change-array-fieldinfo
  • Change-array-result-err
  • Change-array-result-ok
  • Change-array-schar
  • Change-array-sint
  • Change-array-sllong
  • Change-array-slong
  • Change-array-sshort
  • Change-array-type-class
  • Change-array-type-primitive
  • Change-array-type-variable
  • Change-array-uchar
  • Change-array-uint
  • Change-array-ullong
  • Change-array-ulong
  • Change-array-ushort
  • Change-assertion
  • Change-atc-call-info
  • Change-atc-fn-info
  • Change-atj-atype-boolean
  • Change-atj-atype-character
  • Change-atj-atype-cons
  • Change-atj-atype-integer
  • Change-atj-atype-number
  • Change-atj-atype-rational
  • Change-atj-atype-string
  • Change-atj-atype-symbol
  • Change-atj-atype-value
  • Change-atj-function-type
  • Change-atj-function-type-info
  • Change-atj-maybe-function-type-info-none
  • Change-atj-maybe-function-type-info-some
  • Change-atj-maybe-function-type-none
  • Change-atj-maybe-function-type-some
  • Change-atj-maybe-type-none
  • Change-atj-maybe-type-some
  • Change-atj-qconstants
  • Change-atj-test
  • Change-atj-test-value-ACL2
  • Change-atj-test-value-jboolean
  • Change-atj-test-value-jboolean[]
  • Change-atj-test-value-jbyte
  • Change-atj-test-value-jbyte[]
  • Change-atj-test-value-jchar
  • Change-atj-test-value-jchar[]
  • Change-atj-test-value-jint
  • Change-atj-test-value-jint[]
  • Change-atj-test-value-jlong
  • Change-atj-test-value-jlong[]
  • Change-atj-test-value-jshort
  • Change-atj-test-value-jshort[]
  • Change-atj-type-ACL2
  • Change-atj-type-jprim
  • Change-atj-type-jprimarr
  • Change-axi-const
  • Change-axi-gate
  • Change-axi-lit
  • Change-axi-var
  • Change-backref
  • Change-balance-config
  • Change-base-fsm
  • Change-bexp-and
  • Change-bexp-const
  • Change-bexp-equal
  • Change-bexp-less
  • Change-bexp-not
  • Change-bin-integer-literal
  • Change-bindig/uscore-digit
  • Change-bindig/uscore-underscore
  • Change-binding
  • Change-binop-add
  • Change-binop-asg
  • Change-binop-asg-add
  • Change-binop-asg-and
  • Change-binop-asg-div
  • Change-binop-asg-ior
  • Change-binop-asg-mul
  • Change-binop-asg-rem
  • Change-binop-asg-shl
  • Change-binop-asg-shr
  • Change-binop-asg-sub
  • Change-binop-asg-xor
  • Change-binop-bitand
  • Change-binop-bitior
  • Change-binop-bitxor
  • Change-binop-div
  • Change-binop-eq
  • Change-binop-ge
  • Change-binop-gt
  • Change-binop-le
  • Change-binop-logand
  • Change-binop-logor
  • Change-binop-lt
  • Change-binop-mul
  • Change-binop-ne
  • Change-binop-rem
  • Change-binop-shl
  • Change-binop-shr
  • Change-binop-sub
  • Change-bip32-ext-key-priv
  • Change-bip32-ext-key-pub
  • Change-bip32-ext-priv-key
  • Change-bip32-ext-pub-key
  • Change-bip32-key-tree
  • Change-block
  • Change-block-item-declon
  • Change-block-item-stmt
  • Change-block-option-none
  • Change-block-option-some
  • Change-bool
  • Change-boolean-array
  • Change-boolean-result-err
  • Change-boolean-result-ok
  • Change-boolean-value
  • Change-bvar-db-consistency-error-eval-error
  • Change-bvar-db-consistency-error-inconsistency
  • Change-byte-array
  • Change-byte-value
  • Change-candidate-assign
  • Change-cgraph-derivstate
  • Change-cgraph-edge
  • Change-char-array
  • Change-char-literal-char
  • Change-char-literal-escape
  • Change-char-val-insensitive
  • Change-char-val-sensitive
  • Change-char-value
  • Change-character-list-result-err
  • Change-character-list-result-ok
  • Change-character-result-err
  • Change-character-result-ok
  • Change-chase-position
  • Change-class-type-nested
  • Change-class-type-package
  • Change-class-type-simple
  • Change-comm-asg
  • Change-comm-if
  • Change-comm-while
  • Change-command-error-account-key-derivation-fail
  • Change-command-error-address-key-derivation-fail
  • Change-command-error-address-key-index-limit
  • Change-command-error-address-key-index-skipped
  • Change-command-error-address-key-index-too-large
  • Change-command-error-coin-type-key-derivation-fail
  • Change-command-error-external-chain-key-derivation-fail
  • Change-command-error-malformed-address-key-index
  • Change-command-error-malformed-data
  • Change-command-error-malformed-entropy
  • Change-command-error-malformed-gas-limit
  • Change-command-error-malformed-gas-price
  • Change-command-error-malformed-mnemonic
  • Change-command-error-malformed-nonce
  • Change-command-error-malformed-passphrase
  • Change-command-error-malformed-to
  • Change-command-error-malformed-value
  • Change-command-error-no-command
  • Change-command-error-pretransaction-rlp-fail
  • Change-command-error-purpose-key-derivation-fail
  • Change-command-error-root-key-derivation-fail
  • Change-command-error-state-file-absent
  • Change-command-error-state-file-malformed
  • Change-command-error-state-file-not-regular
  • Change-command-error-state-file-present
  • Change-command-error-state-file-untestable
  • Change-command-error-transaction-rlp-fail
  • Change-command-error-transaction-sign-fail
  • Change-command-error-wrong-command
  • Change-command-error-wrong-number-of-arguments
  • Change-compiled-stv
  • Change-compustate
  • Change-compustate-result-err
  • Change-compustate-result-ok
  • Change-config
  • Change-config
  • Change-congruence-rule
  • Change-const-char
  • Change-const-enum
  • Change-const-float
  • Change-const-int
  • Change-constprop-config
  • Change-constraint
  • Change-constraint-equal
  • Change-constraint-instance
  • Change-constraint-relation
  • Change-constraint-rule
  • Change-constraint-rule
  • Change-constraint-tuple
  • Change-constraint-tuple
  • Change-cstate
  • Change-cstate-result-err
  • Change-cstate-result-ok
  • Change-ctrex-rule
  • Change-cuts4-config
  • Change-data-item
  • Change-data-value-hex
  • Change-data-value-plain
  • Change-dec-integer-literal
  • Change-decdig/uscore-digit
  • Change-decdig/uscore-underscore
  • Change-decl
  • Change-declon-struct
  • Change-declon-var
  • Change-declor
  • Change-defarbrec-info
  • Change-defbyte-info
  • Change-defdigits-info
  • Change-definition
  • Change-definition-option-none
  • Change-definition-option-some
  • Change-definterface-hash-info
  • Change-definterface-hmac-info
  • Change-defmapping-info
  • Change-defsvtv-args
  • Change-demo
  • Change-demo2-opts
  • Change-design
  • Change-dom-supergates-sweep-config
  • Change-double-array
  • Change-double-value
  • Change-driver
  • Change-ecutnames
  • Change-element-char-val
  • Change-element-group
  • Change-element-num-val
  • Change-element-option
  • Change-element-prose-val
  • Change-element-rulename
  • Change-elf-header
  • Change-elf-section-header
  • Change-elf32-segment-header
  • Change-elf32_sym-info
  • Change-elf64-segment-header
  • Change-elf64_sym-info
  • Change-eoutcome
  • Change-eoutcome-result-err
  • Change-eoutcome-result-ok
  • Change-eqbylbp-config
  • Change-error
  • Change-escape-carriage-return
  • Change-escape-double-quote
  • Change-escape-letter-n
  • Change-escape-letter-r
  • Change-escape-letter-t
  • Change-escape-line-feed
  • Change-escape-sequence-b
  • Change-escape-sequence-backslash
  • Change-escape-sequence-double-quote
  • Change-escape-sequence-f
  • Change-escape-sequence-n
  • Change-escape-sequence-octal
  • Change-escape-sequence-r
  • Change-escape-sequence-single-quote
  • Change-escape-sequence-t
  • Change-escape-single-quote
  • Change-escape-u
  • Change-escape-x
  • Change-eval-state-error
  • Change-eval-state-final
  • Change-eval-state-init
  • Change-eval-state-trans
  • Change-eviscconfig
  • Change-evmac-appcond
  • Change-ex-args
  • Change-ex-outs
  • Change-exec-outcome-error
  • Change-exec-outcome-nonterminating
  • Change-exec-outcome-terminating
  • Change-expdata-surjmap
  • Change-expr-arrsub
  • Change-expr-binary
  • Change-expr-call
  • Change-expr-cast
  • Change-expr-cond
  • Change-expr-const
  • Change-expr-grade-additive
  • Change-expr-grade-and
  • Change-expr-grade-assignment
  • Change-expr-grade-cast
  • Change-expr-grade-conditional
  • Change-expr-grade-equality
  • Change-expr-grade-ior
  • Change-expr-grade-logical-and
  • Change-expr-grade-logical-or
  • Change-expr-grade-multiplicative
  • Change-expr-grade-postfix
  • Change-expr-grade-primary
  • Change-expr-grade-relational
  • Change-expr-grade-shift
  • Change-expr-grade-top
  • Change-expr-grade-unary
  • Change-expr-grade-xor
  • Change-expr-ident
  • Change-expr-member
  • Change-expr-memberp
  • Change-expr-option-none
  • Change-expr-option-some
  • Change-expr-postdec
  • Change-expr-postinc
  • Change-expr-predec
  • Change-expr-preinc
  • Change-expr-unary
  • Change-expression-add
  • Change-expression-const
  • Change-expression-funcall
  • Change-expression-literal
  • Change-expression-mul
  • Change-expression-option-none
  • Change-expression-option-some
  • Change-expression-path
  • Change-expression-var
  • Change-ext-declon-declon
  • Change-ext-declon-fundef
  • Change-fact-info
  • Change-fgl-binder-rule-bmeta
  • Change-fgl-binder-rule-brewrite
  • Change-fgl-binder-rune-bformula
  • Change-fgl-binder-rune-bmeta
  • Change-fgl-binder-rune-brewrite
  • Change-fgl-casesplit-config
  • Change-fgl-config
  • Change-fgl-congruence-rune
  • Change-fgl-env
  • Change-fgl-ipasir-config
  • Change-fgl-rule-meta
  • Change-fgl-rule-primitive
  • Change-fgl-rule-rewrite
  • Change-fgl-rune-definition
  • Change-fgl-rune-formula
  • Change-fgl-rune-meta
  • Change-fgl-rune-primitive
  • Change-fgl-rune-rewrite
  • Change-fgl-satlink-monolithic-sat-config
  • Change-fhg-args
  • Change-fhg-single-args
  • Change-flatnorm-res
  • Change-flatnorm-setup
  • Change-flatten-res
  • Change-float-array
  • Change-float-value
  • Change-floating-point-type-double
  • Change-floating-point-type-float
  • Change-floating-point-value-double
  • Change-floating-point-value-float
  • Change-fn-info-elt
  • Change-fraig-config
  • Change-frame
  • Change-frame
  • Change-fty-info
  • Change-fty-type-alist
  • Change-fty-type-list
  • Change-fty-type-option
  • Change-fty-type-prod
  • Change-fun-env-result-err
  • Change-fun-env-result-ok
  • Change-fun-info
  • Change-fun-info-option-none
  • Change-fun-info-option-some
  • Change-fun-table-result-err
  • Change-fun-table-result-ok
  • Change-fun-type
  • Change-fun-type-option-none
  • Change-fun-type-option-some
  • Change-func
  • Change-funcall
  • Change-funcall-option-none
  • Change-funcall-option-some