Here's what I did. I put the following in set.mm (right before
"Appendix: Typesetting definitions" although the exact location doesn't
matter much.
mephistolus1 $p |- ( ( 1 + 1 ) + 1 ) = 3 $=
c1 c1 caddc co c1 caddc co c2 c1 caddc co c3 c1 c1 caddc co c2 c1 caddc
1p1e2apr1 oveq1i 2p1e3 eqtri $.
and then I ran metamath.exe and gave it the following commands:
read set.mm
verify proof mephistolus1
whereupon it printed "mephistolus1" which means it verified (an error
would have printed an error message).
Exciting to see Mephistolus generating valid proofs!
On 8/9/19 1:43 PM, Olivier Binda wrote:
Could someone proofcheck it with another metamath proofchecker
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/48de0375-8600-0f7e-c42a-1c193ba6e43b%40panix.com.
