1
00:00:00,000 --> 00:00:08,000
We want to step into the consequent of this formula.

2
00:00:08,000 --> 00:00:22,000
Apply the StepintoSubFormula tactic

3
00:00:22,000 --> 00:00:26,000
Start the subformula selection mode(press ctrl+F10) to select the subformula.

4
00:00:26,000 --> 00:00:32,000
Select the consequent of the implication.

5
00:00:32,000 --> 00:00:41,000
Enter the subformula id.

6
00:00:41,000 --> 00:00:47,000
Apply the tactic.

7
00:00:47,000 --> 00:00:51,000
A new formula node is generated in the synthesis tree.

8
00:00:51,000 --> 00:01:02,000
The consequent becomes the active formula whereas the antecedent is added in the frame context.