Strategy Menu:

Reexpress Command

You can use the Reexpress command to rewrite a given or a goal in a different but equivalent way. Select the given or goal that you want to reexpress and give the Reexpress command. A dialog box will open, offering a number of different ways of reexpressing the selected statement. (Double-clicking on a given or goal is a shortcut for selecting it and giving the Reexpress command.) The statement to be reexpressed appears at the top of the dialog box, and initially the entire statement is selected. You can apply a reexpression to only part of the statement by selecting the part you want to reexpress. 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 “x∈A∧y∈B”, what will be selected is the statement “x∈A”. Click on the buttons in the dialog box to perform the indicated reexpressions on the selected part of the statement.

Once you have reexpressed the statement in the way you want, click the OK button. The new version of the statement will be listed as a variant of the original in the list of givens and goals. A variant of a given or goal is listed below the original and indented. You can select a variant and apply commands to it just like any other given or goal.

Here is what the various buttons in the Reexpress dialog box do: