4.6.3　文の分割

　こういうスケルトンがあります．

　　　for x,y st P[x,y] & Q[x.y] holds R[x,y]
　　　 proof
　　　　let x,y such that L1:P[x,y] and L2:Q[x.y];
　　　　 ······
　　　　 ······
　　　　thus R[x,y];
　　　 end:


　これを次のように書き換えることもできます．注意しなければならないのは & と　and の違いです．
　3行目の，

　　　let x,y such that L1:P[x,y] and L2:Q[x,y];


は，

　　　　let x,y such that L:P[x,y] & Q[x,y];


というふうに，書くこともできます．前の書き方と後の書き方は原理的には同じです．前の書き方の and は，別のラベルをたてるために2つの文に分けるためのものです．これは，A & Bという1つの文を，A という文と，B という文とに分けたということです．それに対して，後の書き方はあくまで1つの文で，論理演算子でつながったものです．このように，and を使って1つの文を2つの文に分けたり，逆に & を使って2つの文を1つの文にすることもできます．