4.3 Dividing the Demonstrations
There are also many different formations for demonstrations. These are called skeletons of demonstrations.
For instance, let us assume that we want to demonstrate p
& q & r. At this point, the following demonstrations can also be
done. (This paragraph becomes the repeat of 4.1.)
p & q & r
proof
······
thus p;
······
thus q;
······
thus r;
······
end;
First, let us assume that p could be demonstrated and it
becomes thus p. Also, continuing with the demonstration, it becomes thus
q, when we demonstrate even further, it becomes thus r. In this case, the
Mizar system looks for thus .... . For this, three thus appear so that
of a proposition p & q & r that should be demonstrated first, we
will recognize the fact that p could be demonstrated. Also, we will recognize
that the second one could be demonstrated with thus q. Finally, we will
be aware that everything could be demonstrated with thus r. The end can
also be stated as thus theses. In this case, system and p,q are already
demonstrated and only r is left; therefore, we will recognize that r is
the thesis. In this way, we will be aware that thus thesis is thus r. It
is fine to write either one of them.
In addition, when demonstrating p & q & r, we can
either demonstrate p first then q & r next, or p & q first and
r later. We can demonstrate by dividing freely.