1
00:00:00,000 --> 00:00:06,925
Start the derivation by applying the Init4 tactic.

2
00:00:07,000 --> 00:00:11,075
Enter the name of the program to be derived: TTFF

3
00:00:11,075 --> 00:00:28,625
Specify the mutable and immutable variables.

4
00:00:28,625 --> 00:01:10,000
Specify the precondition and the postcondition.

5
00:01:10,000 --> 00:01:48,525
Use the Latex commands to enter formulas. Additional commands (\and, \or etc.) are also provided to facilitate specifying formulas.

6
00:01:48,525 --> 00:01:52,575
Enter the global invariants if any. $N \ge 0$ could also have been entered as a global invariant.

7
00:01:52,575 --> 00:01:55,975
Apply the tactic.

8
00:01:55,975 --> 00:02:02,220
Tactic Information and the unknown program fragment is shown in the Content Panel.