Description: (Note: This inference rule and the previous one, idi 1, will
normally never appear in a completed proof.)
This is a technical inference to assist proof development. It provides
a temporary way to add an independent subproof to a proof under
development, for later assignment to a normal proof step.
The Metamath (Metamath-exe) program Proof Assistant requires proofs to
be developed backwards from the conclusion with no gaps, and it has no
mechanism that lets the user work on isolated subproofs. This inference
provides a workaround for this limitation. It can be inserted at any
point in a proof to allow an independent subproof to be developed on the
side, for later use as part of the final proof.
Instructions:
- Assign this inference to any unknown step in the proof.
Typically, the last unknown step is the most convenient, since
MM-PA> ASSIGN LAST can be used. This step will be
replicated in hypothesis a1ii.1, from where the development of the main
proof can continue. - Develop the independent subproof backwards
from hypothesis a1ii.2. If desired, use a
MM-PA> LET STEP
command to pre-assign the conclusion of the independent subproof to
a1ii.2. - After the independent subproof is complete, use
MM-PA> IMPROVE ALL
to assign it automatically to an unknown
step in the main proof that matches it. - After the entire proof
is complete, use
MM-PA> MINIMIZE_WITH * to clean up
(discard) all a1ii 2 references automatically.
This can also be used to apply subproofs from other theorems. In step
2, simply assign the theorem to a1ii.2, and run
MM-PA> EXPAND <theorem>
to "import" a subproof
from another theorem.
This inference was originally designed to assist importing partially
completed Proof Worksheets from the mmj2 Proof Assistant GUI, but it can
also be useful on its own. Interestingly, no axioms are required for
its proof. It is the inference associated with a1i 11.
(Contributed by
NM, 7-Feb-2006.) (Proof modification is discouraged.)
(New usage is discouraged.) |
