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 “xAyB”, what will be selected is the statement “xA”. 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:

• Rename Bound Variable: This button can only be used when the selected expression starts with a quantifier. Use this button to rename the quantified variable. For example, you can rewrite “x(xA)” as “y(yA)”.
• (...): Use this button to add parentheses around an expression. If the statement has brackets around it, they are changed to parentheses. You can't use this button if adding parentheses would change the meaning of the statement; it's only for making the statement easier to read. (There are a few cases in which parentheses affect the workings of a command. For more information, see the Cases, Conjunction, Disjunction, Disjunctive Syllogism Addition, and Split Up commands.)
• [...]: Like (...).
• Remove () or []: Use this button to remove parentheses or brackets around an expression. Again, you can't do this if it would change the meaning of the statement.
• Reexpress Negative/Make Negative: When the selected expression starts with “”, this button is called Reexpress Negative. Use it to reexpress the negative statement as an equivalent positive one. For example, “x(xA)” gets reexpressed as “x(xA)” and “(xAxB)” becomes “xAxB”. If the “” symbol is followed by several quantifiers, pushing this button repeatedly will move the “” past the quantifiers one at a time. When the selected expression does not start with “”, this button is called Make Negative, and it reexpresses the expression as an equivalent one starting with “”. Often this reverses the effect of the Reexpress Negative button.
• Apply Definition: This button performs a number of different reexpressions, based on the definitions of symbols appearing in the selected expression. For example, “x = y” gets reexpressed as “a(axay)”, “xy” gets reexpressed as “a(axay)”, and “xAB” gets reexpressed as “xAxB”. Here is a list of all the reexpressions performed by this button:

  Statements of this form:	Are reexpressed like this:
  AB	a(aAaB)
  A =	a(aA)
  (a, b) = (c, d)	a = cb = d
  A = B	a(aAaB)
  x	x ≠ x
  x{a1, a2, ...,an}	x = a1x = a2...x = an
  xA1A2...An	xA1xA2...xAn
  xA1A2...An	xA1xA2...xAn
  xAB	(xA \ B)(xB \ A)
  xA \ B	xAxB
  (a, b)AB	aAbB
  xAB	aAbB(x = (a, b))
  (a, b)RS	c((a, c)S(c, b)R)
  xRS	abc((a, b)S(b, c)Rx = (a, c))
  xUF	xUAF(xA)
  xF	AF(xA)
  x(A)	xA
  (a, b)R-1	(b, a)R
  xR-1	ab(x = (a, b)(b, a)R)
  x{yA | P(y)}	xAP(x)
  x{f(y) | yA}	yA(x = f(y))
  x(a, b)	x = {a}x = {a, b}
  xAP(x)	x(xAP(x))
  xAP(x)	x(xAP(x))
  !xP(x)	x(P(x)y(P(y)y = x))