スイッチの例の続き

SWITCH = (on -> off -> SWITCH).

この定義は何を示すかというと、次のようなラベルのシーケンスを定義していることになります。

on -> off -> on -> off -> on -> off ...

この場合、onとoffがラベルになります。

さて、シーケンスが定義されれば、その正しさを検証したくなるのが人間ですが、さすがにこの例では正しさも何もないので、それはもう少し先で。