Software FoundationsのIMPあたりをやってて疑問が湧いた. w = while True do Skip endが停止しないことを示したい. つまり, $\langle w, s \rangle \to s' \Rightarrow False$ を示したい. ($s, s' : \mathbb{Z} \to \mathbb{Z}$ は変数の値を保持する環境)…