Signs A B C D E F G H I J K L M N O P Q R S T U V W X Y Z ACL2-PC::

`*standard-input*`

`*standard-output*`

`*standard-input*`

`state`

`include-book`

's `:dir`

argument
`:match-free`

value to `:once`

or `:all`

in existing rules
`nth`

/`update-nth`

terms
`:`

`doc`

and `:`

`more-doc`

text
`args`

, `guard`

, `type`

, `constraint`

, etc., of a function symbol
`state`

`eql`

as test
`eq`

as test
`keyword-value-listp`

`bind-free`

hypotheses
`break-rewrite`

`:BY`

`car`

of the `caaar`

`car`

of the `caadr`

`car`

of the `caar`

`car`

of the `cadar`

`car`

of the `caddr`

`car`

of the `cadr`

`car`

of the `car`

`car`

of the `cdaar`

`car`

of the `cdadr`

`car`

of the `cdar`

`car`

of the `cddar`

`car`

of the `cdddr`

`car`

of the `cddr`

`car`

of the `cdr`

`nil`

`eql`

`:CASES`

`cdr`

of the `caaar`

`cdr`

of the `caadr`

`cdr`

of the `caar`

`cdr`

of the `cadar`

`cdr`

of the `caddr`

`cdr`

of the `cadr`

`cdr`

of the `car`

`cdr`

of the `cdaar`

`cdr`

of the `cdadr`

`cdr`

of the `cdar`

`cdr`

of the `cddar`

`cdr`

of the `cdddr`

`cdr`

of the `cddr`

`cdr`

of the `cdr`

`cons`

pair, else `nil`

`defpkg`

s reside
`certify-book`

`encapsulate`

events
`:default`

from the header of a 1- or 2-dimensional array
`defun`

'd functions
`ld`

` `

argument position of a given function
`equiv1`

refines `equiv2`

`:`

`program`

considered unsound
`mutual-recursion`

`include-book`

's `:dir`

argument
`:dimensions`

from the header of a 1- or 2-dimensional array
`force`

d `case-split`

s
`:DO-NOT`

`:DO-NOT-INDUCT`

`:doc name`

)
`:doc! name`

)
`force`

d `split`

s
`car`

s are suitable for `eql`

`eql`

`eql`

`(hide ...)`

as `<hidden>`

`:EXPAND`

`:(str alist co-channel state evisc) => state`

`:(str alist co-channel state evisc) => state`

`:(str alist co-channel state evisc) => state`

`:(str alist col co-channel state evisc) => (mv col state)`

`:(str alist col channel state evisc) => (mv col state)`

`:GUARD-HINTS`

`:HANDS-OFF`

`defpkg`

events that are `local`

`rebuild`

` `

forced hypotheses are attacked immediately
`:INDUCT`

`include-book`

read the correct files
`cons`

(not element) of a list
`ld`

's response to an error
`ld`

`ld`

suppresses details when printing
`ld`

prints the result of evaluation
`ld`

evaluates
`ld`

prints the forms to be `eval`

'd
`ld`

`ld`

prints ``ACL2 Loading ...''
`i`

th bit of an integer
`:logic`

`:maximum-length`

from the header of an array
`:MEASURE`

`eql`

as test
`eq`

as test
`:meta`

rule (a hand-written simplifier)
` `

(often cited in more accessible documentation)
`floor`

`:MODE`

`:`

`doc`

or `:`

`more-doc`

's ```(cont'd)`

''
`:`

`doc`

documentation
`eql`

for equality)
`equal`

for equality)
`:NON-EXECUTABLE`

`:NONLINEARP`

`:NORMALIZE`

`NTH`

/`UPDATE-NTH`

expressions
`epsilon-0`

`break-rewrite`

`:u`

or `:`

`ubt`

`defpkg`

s
`eql`

as test
`eq`

as test
`er-progn`

`:program`

`ld`

`o<`

is well-founded on `o-p`

s
`:q`

) -- reenter with `(lp)`

`eql`

as test
`eq`

as test
`equal`

as test
`truncate`

`eql`

`eql`

) a list
`nth`

/`update-nth`

terms
`ld`

specials
`cdr`

) of the list
`:RESTRICT`

`:rewrite`

rules (possibly conditional ones)
`ignore`

declaration
`:match-free`

in future rules
`:match-free`

is missing
`:`

`definition`

and `:`

`rewrite`

rules used in preprocessing
`ld`

prints
`counters`

stobj
`counters`

stobj
`counters`

stobj
`:STOBJS`

`member`

of one list is a `member`

of the other
`eql`

as test
`:`

`rewrite`

, `:`

`meta`

, or `:`

`linear`

rule
`:USE`

`stable-under-simplificationp`

flag
`brr`

mode
`ld`

without `state`

-- a short-cut to a parallel universe
`defun`

` `

attempt an equality (or equivalence) substitution
` `

same as `(lisp x)`

` `

add an abbreviation
` `

call the ACL2 theorem prover's simplifier
` `

prove the current goal using bdds
` `

move backward one argument in the enclosing term
` `

insert matching ``bookends'' comments
` `

split into two cases
` `

change to another goal.
` `

change to another goal.
` `

add a new hypothesis
` `

display instructions from the current interactive session
` `

display instructions from the current interactive session
` `

insert a comment
` `

same as `contrapose`

` `

switch a hypothesis with the conclusion, negating both
` `

move top-level hypotheses to the conclusion
` `

move to the indicated subterm
` `

run the given instructions
` `

run the given instructions, halting once there is a ``failure''
` `

run the given instructions, halting once there is a ``failure''
` `

drop top-level hypotheses
` `

move to the indicated subterm
` `

call the ACL2 theorem prover's elimination process
` `

attempt an equality (or congruence-based) substitution
` `

exit after possibly saving the state
` `

exit the interactive proof-checker
` `

expand the current function call without simplification
` `

cause a failure
` `

forward chain from an implication in the hyps
` `

create a ``free variable''
` `

perform a generalization
` `

list the names of goals on the stack
` `

proof-checker help facility
` `

proof-checker help facility
` `

same as `help!`

` `

print the hypotheses
` `

illegal instruction
` `

set the current proof-checker theory
` `

generate subgoals using induction
` `

print the runes (definitions, lemmas, ...) used
` `

evaluate the given form in Lisp
` `

proof-checker help facility
` `

proof-checker help facility
` `

run the given instructions, and ``succeed'' if and only if they ``fail''
` `

used for interpreting `control-d`

` `

run instructions with output
` `

move forward one argument in the enclosing term
` `

run the first instruction; if (and only if) it ``fails'', run the
` `

second
` `

prettyprint the current term
` `

prettyprint the conclusion, highlighting the current term
` `

prettyprint the current term
` `

print the result of evaluating the given form
` `

print all the conclusions of (as yet unproved) goals
` `

print all the (as yet unproved) goals
` `

print the original goal
` `

repeatedly apply promote
` `

move antecedents of conclusion's `implies`

term to top-level
` `

hypotheses
` `

run the given instructions, reverting to existing state upon
` `

failure
` `

call the ACL2 theorem prover to prove the current goal
` `

substitute for a ``free variable''
` `

run instructions without output
` `

same as rewrite
` `

call the ACL2 theorem prover's simplifier
` `

call the ACL2 prover without induction, after going into
` `

induction
` `

remove one or more abbreviations
` `

repeat the given instruction until it ``fails''
` `

auxiliary to `repeat`

` `

replay one or more instructions
` `

remove the effect of an UNDO command
` `

drop all ` `

re-enter the proof-checker
` `

apply a rewrite rule
` `

auxiliary to THEN
` `

auxiliary to `then`

` `

print the runes (definitions, lemmas, ...) used
` `

simplify the current subterm
` `

simplify propositionally
` `

save the proof-checker state (state-stack)
` `

run the given list of instructions according to a multitude of
` `

options
` `

display the current abbreviations
` `

display the applicable rewrite rules
` `

``succeed'' without doing anything
` `

simplify with lemmas
` `

split the current goal into cases
` `

same as SHOW-REWRITES
` `

run the given instructions, and ``succeed''
` `

print the top-level hypotheses and the current subterm
` `

apply one instruction to current goal and another to new subgoals
` `

move to the top of the goal
` `

display the type-alist from the current context
` `

undo some instructions
` `

remove a proof-checker state
` `

move to the parent (or some ancestor) of the current subterm
` `

use a lemma instance
` `

execute the indicated instructions and combine all the new goals
` `

same as induct, but create a single goal
` `

combine goals into a single goal
` `

expand and (maybe) simplify function call at the current subterm
` `

expand function call at the current subterm, without simplifying