4.5　now の使い方

　さらに証明のスケルトンですが，not pを証明するのに，nowを使うことがあります．now は次のように使います．

　　　　 now assume p;
　　　　 ······
　　　　 ······
　　　　 thus contradiction;
　　　　end;


　now は　now 〜 end で1つの文(論理式)とみなします．この now 〜 end は，not p と同じものです．あるいは，assume p で， p implies contradiction という論理式です．