4.8 Dividing into Cases

Next, we will discuss about demonstrating by dividing into cases. Let us
assume that we want to demonstrate a proposition "A and B" and
it can be done if we divide these into cases. For instance, we want to
demonstrate by dividing into cases such as when x=1, x=2, and when x takes
some other value. This means that with x=1,2, it becomes a peculiar point.
At this point, it takes the structure of the following demonstrations.

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;

We will demonstrate by supposing each case in "now per cases ~ end".
We will demonstrate from "case x=1" to the beginning of "thus
A and B" when x=1. In the same way, we will also demonstrate when
x=2 and other cases. The sentences from now to end are considered as the
whole one "A and B". For example, if we have then after "now
~ end", "then" receives the whole "now ~ end".
Even though it is divided into each case with "case", the conclusion
of each case is handed over to the end. Therefore, when all of this is
cited, the fact that it was divided with "case" is forgotten
and the fact that only the conclusions are the same is checked. Thus, it
means that this is one formula.

In addition, since a formula like L is logically clear, there
may not be "by L" of "now per cases by L.".