4.6.3 Division of Sentences

There is a skeleton such as this:

      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:


    We can also rewrite this as the following. We need to pay careful attention to the difference of & and and.
The third line

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

is

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


We can also write like the above. Methods for writing the front and back are basically the same. In the method for writing the front, and is used for dividing into two sentences to build other labels. This means that one sentence A & B was divided into sentences A and B. On the other hand, the method for writing the back is persistently one sentence and it is connected by a logical calculation unit. As stated before, we can divide one sentence into two by using and, or, we can connect two sentences into one by using &.