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