Start the derivation by applying the Init4 tactic.
Enter the name of the program to be derived: TTFF
Specify the mutable and immutable variables.
Specify the precondition and the postcondition.
Use the Latex commands to enter formulas. Additional commands (\and, \or etc.) are also provided to facilitate specifying formulas.
Enter the global invariants if any. $N \ge 0$ could also have been entered as a global invariant.
Apply the tactic.
Tactic Information and the unknown program fragment is shown in the Content Panel.