I think mmj2 only ever uses wceq, because it "parses" formulas and using
weq introduces an ambiguity into the resulting grammar. However
metamath-exe's MINIMIZE will find shorter proofs using lemmas, and it
treats syntax lemmas just like real lemmas, so it will "optimize" the proof
to use weq. I
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
On Mon, Feb 12, 2024 at 8:40 AM Glauco wrote:
> The proofs produced by mmj2 are not exactly the same, because (in my
> opinion) mmj2 has a small bug in the knapsack algorithm
>
> IMHO, metamath.exe and mmj2 don't produce the same compressed proofs (I've
> shown several examples, in the past)
>
Hi jagra,
starting from an uncompressed proof, you can compress it in several
different ways, depending on how you order the labels. There's not a spec
for how you order the labels.
Yamma's configuration allows you to choose between three ordering
algorithms:
fifo
mostReferencedFirst
