次に場合に分けて証明するときの話をします．証明したいのはA and Bという命題 で，この命題は場合分けすれば証明できるとします．例えばx=1の場合とx=2 の場合 と，xがその他の値を取る場合とに分けて証明したいとします．x=1,2で特異点になっ ているということです．このときには次のような証明の構造をとります．
L:( x=1 or x=2 or not ( x=1 & x=2 ))
now per cases by L;
case LA:x=1;
···
thus A and B;
case LB:x=2;
thus A and B;
case LC:not (x=1 & x=2);
···
thus A and B;
end;
now per cases ～ endの中で，それぞれの場合についてcaseを分けて証明しま す．case x=1 から最初の thus A and B までで x=1 のときの証明をします．同様に，
x=2の時，その他の場合についても証明します．このとき，nowからendまでの文は全 体で
1
つのA and Bとみなします．例えばnow ～ endの後にthenとすれば，then は now ～ end 全体を受けるわけです．case でそれぞれの場合に分けられていますが，それぞれの場合の帰結の部分を最後に渡すわけです．ですから，これ全体を引用したと きにはcaseに分かれたということは忘れてしまって，結論だけが全部同じということ がチェックされるわけです．だからこれは
1
つの式だということです．なお，Lのよう な式は論理的に明らかなので，now per cases by L の by L はなくてもいいのです．4.8.1 場合分けの前提
ここで注意があります．この場合は，x=1 or x=2 or not (x=1 & x=2) ---(1) という式を場合分けするときに前提として使っています．この場合分けがすべての場合 を覆っているということをいっているわけです．このように場合分けするときは，すべ ての場合についていっていることを言わなければなりません．
なお，上の例のように(1)式の成立が明らかなときには，now per cases
の後の
by は不要です．4.8.2 場合分けでのラベル
当然ながら場合分けをして証明するときには，それぞれの場合の証明でのラベルは，
その場合の証明の中でのみ有効です．もし，その場合の証明以外でその証明のラベルを 使おうとすると，ラベルがないというエラーとなります．
4.8.3 ラベルについての注意
それから，ここでラベルの注意をしておきます．Mizarでは，同じラベルを使っても かまいませんが，直前のものが優先されます．
例えば，
L1:...;
...
L1:...;
... by L1;ここでは直前の L1 が引用される
この例で何か証明したときにby L1とすると，下の L1
の文が引用されます．
このことは間違いやすくL1, L2, L3, ...
とラベルをつけていって，どこまで
ラベルを使ったのかを忘れてしまい，またL3とつけたとします．そして，by L3とす ると，自分では前のL3のつもりで必ずL3から推論できると思っても，いくらやって もエラーがでてきてしまうわけです．このようなことを最初のうちによくやります．こ のときはよく捜すと，同じラベルが1
つ隠れているのです．もうひとつ別のところにあ ることがあります．4.9 @proof の使い方
Mizar
で長い articleを書いていると，くりかえしMizar
チェッカーでチェックすることになります．長い
article
をチェックするには時間がかかります．このようなとき，既 に証明が終わった定理などはチェックすることを省略することによって，Mizarチェッ クにかかる時間を節約することができます．定理などのチェックするのを省略するには，proofを@proofに変えて置きます．こ うすることにより，Mizarチェッカーはその定理をチェックしません.
もちろん