Wow, thank you very much!
Just FYI, in the 20190602 version of the Metamath book, in the "write
source" subsection (5.3.2) there is no option for /extract.
On Saturday, April 6, 2024 at 6:45:50 PM UTC+2 ginogiott...@gmail.com wrote:
> > Now I want to create this set_simplified.mm file. Mario
> Now I want to create this set_simplified.mm file. Mario Carneiro suggests
to use a ""metamath aware" slicer". Is there such a slicer already created?
Yes, there is already such slicer, you do the following:
READ set.mm
WRITE SOURCE 2p2e4.mm /EXTRACT 2p2e4
This creates a working .mm file that
Thank you for all the answers, they are quite informative.
Now I want to create this set_simplified.mm file. Mario Carneiro suggests
to use a ""metamath aware" slicer". Is there such a slicer already created?
I guess it is not as easy as just deleting, from set.mm, the subtheorems
that are not
On Tue, Apr 2, 2024 at 6:56 PM Anarcocap-socdem <
jordi.molins.coron...@gmail.com> wrote:
> Thank you very much for the answer.
>
> Let us see if I understand this:
>
> Let us assume I take the 619 different subtheorems used in 2p2e4 (I get
> this number, 619, by doing SHOW TRACE_BACK 2p2e4
Thank you very much for the answer.
Let us see if I understand this:
Let us assume I take the 619 different subtheorems used in 2p2e4 (I get
this number, 619, by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS). These 619
subtheorems can be listed by doing show trace_back 2p2e4. The total number
of
> 3. Is there some way to print/export to file the 12178 steps, and even
the 5.9 x 10^12 steps, all at once? I ask this since running show
trace_back 2p2e4 /tree gives me a tree, but with only the name of the
subtheorems, not the steps themselves. And I have been unable to find a
command that
> 1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated that
"A longest path back to an axiom from 2 + 2 = 4 is *184 layers* deep".
However, if I run show trace_back 2p2e4 /count_steps, it is stated that
"The maximum path length is 84". Is there a typo somewhere? (84 != 184).
Note
Hello, I am trying to understand 2p2e4, as an excuse to understand metamath
better.
I have a few questions:
1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated that "A
longest path back to an axiom from 2 + 2 = 4 is *184 layers* deep".
However, if I run show trace_back 2p2e4
