When the theorem prover explicitly assigns a name, like *1, to a formula, it has decided to prove the formula by induction.
*1
