4.3　証明の分割

　証明の構成もいろいろあります．これらを証明のスケルトンといいます．
　たとえば，p & q & r を証明したいとします．このとき，次のように証明することも出来ます(この節は4.1の繰り返しになります)．

　　　　p & q & r
　　　　　proof
　　　　　 ······
　　　　　 thus p;
　　　　　 ······
　　　　　 thus q;
　　　　　 ······
　　　　　 thus r;
　　　　　 ······
　　　　　end;


　まず p が証明できたとします．そうすると thus p となります．また証明を続けて thus q ，さらに証明していって thus r．この場合 Mizar のシステムは，thus　. . .を捜します．これには thus が3つもでてきますので，最初のthus　で証明すべき命題　p & q & r のうちの p が証明できたということを認識し，次に thus q で2番目も証明できたことを認識します．最後に thus r ですべて証明されたことを認識します．最後は thus thesis とすることもできます．この場合，システムは既に p, q は証明されていて，残っているのは r だけで，r が thesis だと認識します．こうして， thus thesis は thus r であるということを認識します．どちらを書いてもかまいません．
　それから　p & q & r を証明するときに，p を先に証明し，q & r を後に証明したり，あるいは p & q を先に証明し，rを後に証明してもかまいません．自由に分割して証明することができます．