Strategy Menu:

Substitute Command

If you have a given of the form x = y, then in any given or goal you may substitute y for x or x for y. To perform such a substitution, select the given or goal in which you would like to do the substitution, and position the mouse over the Substitute command. A submenu will appear, listing all available substitutions; an entry of the form “xy” means “replace x by y”. Select the substitution you would like to perform, and a dialog box will open. The statement in which the substitution is to be performed appears at the top of the dialog box, and initially the entire statement is selected. You can perform the substitution in only part of the statement by selecting the part in which you want the substitution to be performed. Selecting works in the usual way, except that when you drag the mouse across a part of the statement, what gets selected is the smallest meaningful subexpression containing the symbols you drag across. For example, if you drag the mouse across the symbols “x” in the statement “xAyB”, what will be selected is the statement “xA”.

Click the Substitute button to perform the substitution. The other buttons in the dialog box can be used to rewrite the statement in some other ways; for details see the instructions for the Reexpress command.