4.5 now の使い方

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



  now assume p;



    .....



    .....



   thus contradiction;



  end;

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

4.5.1 end についての注意

end についての注意ですが，Mizar では, proof 〜 end ，now 〜 end などで end が出てきて，またこれらがネスティングをなしてきます．end がたくさんあると，どれがどの end かわからなくなってしまいます．ですから, now を書いたら end は必要なので，now を書いたら end をすぐに書いてしまいます．あとは，この中にエディターでどんどん挿入していけばいいわけです．同様に，proof と書いたら，必ず end と書いてしまいます．end だけを書くということはないと決めておくと間違いはありません．