|Description: (Note: This
inference rule and the next one, idi 2, will normally
never appear in a completed proof. It can be ignored if you are using
this database to assist learning logic - please start with the statement
wn 5 instead.)
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 program's Proof Assistant requires proofs to be developed
backwards from the conclusion with no gaps, and it has no mechanism that
lets the user to 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: (1) Assign this inference to any unknown step in
proof. Typically, the last unknown step is the most convenient, since
'assign last' can be used. This step will be replicated in hypothesis
dummylink.1, from where the development of the main proof can continue.
(2) Develop the independent subproof backwards from hypothesis
dummylink.2. If desired, use a 'let' command to pre-assign the
conclusion of the independent subproof to dummylink.2. (3) After the
independent subproof is complete, use 'improve all' to assign it
automatically to an unknown step in the main proof that matches it. (4)
After the entire proof is complete, use 'minimize *' to clean up
(discard) all dummylink references automatically.
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. (Contributed by NM?, 7-Feb-2006.)