Add test cases about minimization

tests/min_found.expected

@@ -0,0 +1,29 @@
+MM> READ "min_found.mm"
+Reading source file "min_found.mm"... 761 bytes
+761 bytes were read into the source buffer.
+The source has 18 statements; 5 are $a and 2 are $p.
+SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
+No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
+if you want to check them.
+MM> Continuous scrolling is now in effect.
+MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
+..................................................
+All proofs in the database were verified in x.xx s.
+MM> Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
+You will be working on statement (from "SHOW STATEMENT th2"):
+18 th2 $p D $= ... $.
+Note:  The proof you are starting with is already complete.
+MM-PA> Bytes refer to compressed proof size, steps to uncompressed length.
+Scanning forward through statements...
+Proof of "th2" decreased from 24 to 15 bytes using "in1".
+Scanning backward through statements...
+Proof of "th2" decreased from 24 to 15 bytes using "in1".
+The forward scan results were used.
+MM-PA> Proof of "th2":
+---------Clip out the proof below this line to put it in the source file:
+    ( ax-1 in1 ) AB $.
+---------The proof of "th2" (15 bytes) ends above this line.
+MM-PA> EXIT
+Warning:  You have not saved changes to the proof of "th2".
+Do you want to EXIT anyway (Y, N) <N>? Y
+Exiting the Proof Assistant.  Type EXIT again to exit Metamath.

tests/min_found.in

@@ -0,0 +1,4 @@
+verify proof *
+prove th2
+minimize * /allow *
+show new /compressed

tests/min_found.mm

@@ -0,0 +1,31 @@
+$( A shortening found by the minimizer.  The comparison with min_not_found.mm
+   suggests that the minimizer's ability to detect it depends on the presence
+   of statement "A" in the steps of the minimized proof.  The costant C and
+   axiom ax-3 are not used here, but they are kept anyway to lessen the amount
+   of differences with min_not_found.mm. $)
+
+  $c A B C D $.
+
+  ax-1 $a A $.
+  ax-2 $a B $.
+  ax-3 $a C $.
+
+  ${
+    in1.1 $e A $.
+    in1 $a D $.
+  $}
+
+  ${
+    in2.1 $e B $.
+    in2.2 $e A $.
+    in2.3 $e B $.
+    in2.4 $e B $.
+    in2.5 $e B $.
+    in2 $a D $.
+  $}
+
+  $( Minimized proof, found automatically.  (New usage is discouraged.) $)
+  th1 $p D $= ( ax-1 in1 ) AB $.
+
+  $( Non-minimized proof. $)
+  th2 $p D $= ( ax-2 ax-1 in2 ) ABAAAC $.

tests/min_not_found.expected

@@ -0,0 +1,24 @@
+MM> READ "min_not_found.mm"
+Reading source file "min_not_found.mm"... 788 bytes
+788 bytes were read into the source buffer.
+The source has 18 statements; 5 are $a and 2 are $p.
+SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
+No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
+if you want to check them.
+MM> Continuous scrolling is now in effect.
+MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
+..................................................
+All proofs in the database were verified in x.xx s.
+MM> Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
+You will be working on statement (from "SHOW STATEMENT th2"):
+18 th2 $p D $= ... $.
+Note:  The proof you are starting with is already complete.
+MM-PA> Bytes refer to compressed proof size, steps to uncompressed length.
+Scanning forward through statements...
+No shorter proof was found.
+MM-PA> Proof of "th2":
+---------Clip out the proof below this line to put it in the source file:
+    ( ax-2 ax-3 in2 ) ABAAAC $.
+---------The proof of "th2" (24 bytes) ends above this line.
+MM-PA> EXIT
+Exiting the Proof Assistant.  Type EXIT again to exit Metamath.

tests/min_not_found.in

@@ -0,0 +1,4 @@
+verify proof *
+prove th2
+minimize * /allow *
+show new /compressed

tests/min_not_found.mm

@@ -0,0 +1,31 @@
+$( A shortening not found by the minimizer.  The comparison with min_found.mm
+   suggests that the minimizer's inability to detect it is due to the absence
+   of statement "C" in any of the steps of the minimized proof.  The
+   shortening is detected if proveFloating is set to 1 in replaceStatement
+   called by minimizeProof, which allows absent $e statements to be found. $)
+
+  $c A B C D $.
+
+  ax-1 $a A $.
+  ax-2 $a B $.
+  ax-3 $a C $.
+
+  ${
+    in1.1 $e A $.
+    in1 $a D $.
+  $}
+
+  ${
+    in2.1 $e B $.
+    in2.2 $e C $.
+    in2.3 $e B $.
+    in2.4 $e B $.
+    in2.5 $e B $.
+    in2 $a D $.
+  $}
+
+  $( Minimized proof, not found automatically.  (New usage is discouraged.) $)
+  th1 $p D $= ( ax-1 in1 ) AB $.
+
+  $( Non-minimized proof. $)
+  th2 $p D $= ( ax-2 ax-3 in2 ) ABAAAC $.