>>147から一連の人
サンクスです。
意味は大体わかりました。普通の証明方法なんですね。
オラクルとどう使い分けるのかとか教えていただければありがたいです。
それと"rewind"も言ってることは分かるけど、どう使うものなのかと。

シミュレータを使って証明をformallyに書き直せといわれてますので
どう書くとformallyなんだかなぁと困ってました。



そういえば、Angel（？）なんて謎の概念も出てきてましたね