Thanks both for the explanations. I had it working, but since the generated proofs were in some cases so different from those in set.mm, I was trying to understand why.
One of the things I noticed, and caused the differences I had, was avoiding the use of $p statements in parsing rules. For instance, weq and wceq seem to be similar, but weq is a $p while wceq is a $a, but they seem to be basically equivalent when used in generated proof. Including weq creates in some cases, several distinct correct parsing alternatives for the same statement, while using just $a rules (wceq instead of weq) does not. Tested (only) with ax8, replacing the original proof with one that contained a proof generated just from $a rules (from base ax8 proof statements), and set.mm was verified without errors. The proof is bigger and I understand that's a concern always present, but, other than that, do you see any problems with it? Best regards, Jorge Agra -- 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/980d8c60-d073-4784-81c8-11a698612730n%40googlegroups.com.
