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;

suppose LA:x=1;

......

thus A and B;

suppose LB:x=2;

......

thus A and B;

suppose 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 suppose 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 suppose, 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 suppose is forgotten and the fact that only the conclusions are the same is checked. Thus, it means that this is one formula.


4.8.1 Premise for Dividing into Cases

We have some warnings for you here. This case is used as a premise when dividing a formula x=1 or x=2 or not (x=1 & x=2) into cases. It means that this division of cases covers all cases. When dividing into cases in this way, we have to state that we are stating this about all cases.


4.8.2 Labels for Dividing Into Cases

Unquestionably, when demonstrating by dividing into cases, the labels of each case demonstration is only valid during the demonstration of that particular case. If we try to use that label for the demonstration of another rather than that specific demonstration case, an error saying that there is no label will appear.


4.8.3 Warning About Labels

Further, we will give a warning about labels. In Mizar, it is acceptable to use the same label; however, the ones just before are prioritized.

For example:


L1:......;

......

L1:......;

...... by L1; Here, L1 of just before is cited.

When we want to demonstrate something with this case, if we put L1, the sentence of L1 below it will be cited.

This is easily mistaken and when we put labels L1,L2,L3,...... , we tend to forget until the labels were used. Also, let us assume that we put L3 and when we state by L3, even if we think that it is \verb| L3| and we can certainly infer from \verb| L3|, there will be an error. This kind of mistake is made often at first. When this happens, there is one label that is hiding if examined carefully. Sometimes, there is another one in a different place. This was a warning for labels.