This rule can be used forwards to copy a previous line in the proof (this is done to increase readability) or backwards to complete a box or proof by matching the goal line with an identical line shown in the proof.
To use it forwards:
- select an empty line and click on Tick.
- then select the line you wish to copy (this line must be in the scope of the empty line).
- a new line containing the same formula as line you selected will then be added to the proof.
To use it backwards:
- select the goal you wish to apply tick to and click on Tick.
- then select the line which matches the goal formula you selected (this line must be in the scope of the goal line).
- the box containing the goal line will then close (the empty line is removed and the box will turn grey).
|