Re: [Metamath] Trying to understand 2p2e4

2024-04-02 Thread Mario Carneiro
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

Re: [Metamath] Trying to understand 2p2e4

2024-04-02 Thread Anarcocap-socdem
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

Re: [Metamath] Trying to understand 2p2e4

2024-04-02 Thread Gino Giotto
> 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