
The following is not a complete list of Nuprl tactics; only those tactics
which are used in the proofs in this study are listed here. Tactics are
listed alphabetically. If you are do not know what a tactic or a conversion
is, you should return to the Introduction to Nuprl
page before proceeding. If you are not familiar with the tactics listed here,
you may want to print this page out or leave a window in your web browser
open to it while you complete this study. Recall that hypotheses can be
referred to by number, with hypothesis 0 being the conclusion.
 ...
 an abbreviation for "THEN Auto"; see the entries for THEN and
Auto for further explanation
 ...a
 an abbreviation for "THENA Auto"; see the entries for THEN and
Auto for further explanation
 ...as
 an abbreviation for "THENA SIAuto"; see the entries for THEN and
SIAuto for further explanation
 AbReduce
 used in the form "AbReduce i", simplifies hypothesis i using
a defined set of equivalences
 Arith
 performs a restricted form of arithmetic reasoning which covers integer
addition and multiplication, inequalities and equality
 ArithSimp
 used in the form "ArithSimp i", creates a main subgoal where
hypothesis i is rewritten to be in arithmetical canonical form and an
auxiliary subgoal to show that the replacement statement is equivalent to
the original statement of hypothesis i
 Assert
 used in the form "Assert t", generates two subgoals, one which adds
t as a new hypothesis and the other with t as the goal to prove
from the current hypotheses
 Auto or Auto'
 repeatedly applies a set of elementary automatic proving techniques
(including Arith, GenExRepD, and others) until no more progress is made
 BackThruHyp
 used in the form "BackThruHyp i" where i is a universally
quantified inference, matchs the current goal to the consequent of the
inference and takes the antecedents of the inference as subgoals
 BackThruLemma
 used in the form "BackThruLemma n" where n is the name of
a lemma whose statement is a universally quantified inference, matches the
current goal to the consequent of the inference and takes the antecedents of
the inference as subgoals
 BackThruLemmaWithUnfolds
 used in the form "BackThruLemmaWithUnfolds n
[name1 ... nameN]" where n is the name of a lemma whose
statement is a universally quantified inference and name1 through
nameN are names of externally defined mathematical objects, runs
BackThruLemma on n, performing an Unfold on any occurrences of
name1,...,nameN as necessary to complete the matching; see
BackThruLemma and Unfold for further information
 BHyp
 an abbreviation for "BackThruHyp"; see the entry for BackThruHyp for
further explanation
 BLemma
 an abbreviation for "BackThruLemma"; see the entry for
BackThruLemma for further explanation
 BoolCasesOnCExp
 used in the form "BoolCasesOnCExp t", does a case split of the
current goal based on whether t is true or false generating a truecase
and a falsecase subgoal
 D
 used in the form "D i", decomposes the outermost connective of
hypothesis i, performing as many Unfold operations as necessary on
externally defined mathematical objects until a connective that it can
decompose is outermost; see Unfold for further information
 Decide
 used in the form "Decide (p)", performs a case split on whether the
proposition p is true or false; two subgoals are created, one with
p added as a new hypothesis and the other with "not p" added as
a new hypothesis
 Dvars
 used in the form "Dvars [v1,...,vn] i" where the
[v1,...,vn] is a variable list, decomposes the outermost
operator of hypothesis i using the variables in the variable list to
name any new variables created; see D for further information on
decomposition
 FLemma
 an abbreviation for "FwdThruLemma"; see the entry for FwdThruLemma
for further explanation
 FwdThruLemma
 used in the form "BackThruLemma n" where n is the name of a
lemma whose statement is a universally quantified inference, matches the
antecedents to current hypotheses and adds the consequent of the inference as
a new hypothesis
 GenExRepD
 decomposes all universal quantifiers, implications and conjunctions in the
conclusion and all existential quantifiers, disjunctions and conjunctions in
all hypotheses until no outermost connective of the specified type exists to
be decomposed; see D for further information on decomposition
 GenRepD
 decomposes all universal quantifiers, implications and conjunctions in the
conclusion and all conjunctions in all hypotheses until no outermost connective
of the specified type exists to be decomposed; see D for further
information on decomposition
 HigherC
 used in the form "HigherC c", takes a conversion c and
specifies that it should be applied at the outermost place where it is
applicable
 HypSubst
 used in the form "HypSubst i c" where i is the number
of a hypothesis of the form "t1 = t2" and c is the number of a
hypothesis or the goal, a new subgoal is created where all occurrences of
t1 in clause number c are replaced with occurrences of t2,
a subgoal with "t1=t2" as the goal and a wf subgoal
 IfLab
 used in the form "IfLab lab T1 T2" where lab
is a label for a subgoal such a "main" or "wf", this tactic is called after
another tactic has run and matches the labels of the created subgoals against
lab; if lab matches the label of the subgoal then T1 is
run, otherwise T2 is run
 InstHyp
 used in the form "InstHyp [t1,...,tn] i",
instantiates a universal formula in hypothesis i with the terms
t1 through tn
 InstLemma
 used in the form "InstLemma n [t1,..,tn]" where
n is the name of a lemma, instantiates the lemma n with the terms
t1 through tn
 IntSimpC
 a conversion which rewrites a statement to an equivalent statement which
is in arithmetical canonical form
 LemmaC
 used in the form "LemmaC n" where n is the name of a lemma
whose statement is a universally quantified inference with the consequent
"a r b" where r is an equivalence relation, creates a conversion
to replace instances of a with instances of b
 LemmaWithC
 used in the form "LemmaC [h] n", creates a conversion to
replace instances of a with instances of b as in LemmaC but
uses the additional binding information given by h to assist in
finding the conversion; see the entry for LemmaC for further information
 NthC
 used in the form "NthC i c", specifies that the conversion
c should be applied in the ith place where it is applicable
 OnClauses
 used in the form "OnClauses [i1,...,in] T" where
T is a tactic which has not had its hypothesis argument supplied, runs
T on hypotheses i1 through in
 OnHyps
 used in the form "OnHyps [i1,...,in] T" where T
is a tactic which has not had its hypothesis argument supplied and none of the
i's are 0, runs T on hypotheses i1 through in
 ReplaceWithEqv
 used in the form "ReplaceWithEqv c t i" where t
is a statement and c is a conversion, takes hypothesis i and
replaces it with t so long as the result of applying c to
hypothesis i is the same as applying c to t
 RevLemmaC
 used in the form "RevLemmaC n" where n is the name of a
lemma whose statement is a universally quantified inference with the
consequent "a r b" where r is an equivalence relation, creates
a conversion to replace instances of b with instances of a
 Rewrite
 used in the form "Rewrite c i" where c is a
conversion and i is the number of a hypothesis or the goal, applies
the conversion to the clause i
 RWH
 an abbreviation for "Rewrite (HigherC c)"; see the entries for
Rewrite and Higherc for further information
 RWN
 an abbreviation for "Rewrite (NthC n c)"; see the entries
for Rewrite and NthC for further information
 Sel
 used in the form "Sel n T" where n is an integer and
T is a tactic, runs T with n as an argument indicating
which branch (usually of a disjunction) to take
 SeqOnM
 used in the form "SeqOnM [T1,...Tn]" where
T1,...,Tn are tactics, runs T1 through Tn on
successive main suboals
 SIAuto
 runs the same an auto but with SupInf added to the set of automatic
proving techniques used; SupInf is a tactic to solve integer inequalities
 SplitOnConclITE
 finds the first occurrence of an "if...then...else" in the conclusion and
generates two subgoals, one for the case where the condition is true and the
other for the case where the condition is false
 THEN
 used in the form "T1 THEN T2" where T1 and T2
are tactics, runs T1 and then runs T2 on all of the generated
subgoals
 THENA
 used in the form "T1 THENA T2" where T1 and T2
are tactics, runs T1 and then runs T2 on the auxiliary subgoals
generated
 THENM
 used in the form "T1 THENM T2" where T1 and T2
are tactics, runs T1 and then runs T2 on the main subgoal
generated
 Thin
 used in the form "Thin i", removes hypothesis i from the
hypothesis list
 Try
 used in the form "Try T" where T is a tactic, try running
T and if it fails do nothing instead
 TryC
 used in the form "TryC c", specifies that if the conversion
c fails when it in is applied then it should instead return making no
changes
 Unfold
 used in the form "Unfold n i" where n is the name of
an externally defined mathematical object, replaces n with its
definition anywhere that it appears in hypothesis i
 UnfoldTopAb
 used in the form "UnfoldTopAb i", runs Unfold with the outermost
operator in the place of the name argument; see Unfold for further
information
 UnfoldTopC
 used in the form "UnfoldTopC n" where n is the name of an
externally defined mathematical object, creates a conversion which replaces a
statement t whose outermost operator is n with a statement
t' where n has been replaced with its definition
 UnivCD
 decomposes universal quantifiers and implications in the conclusion until
the outermost connective is not one of these two connectives; see D
for further information on decomposition
 Using
 used in the form "Using [s1,...,sn] T" where
[s1,...,sn] is a list of substitutions, runs tactic T using the
list of substitutions to help it instantiate universally quantified variables
as called for

