The problem is that the proof uses an old version of frlmgsum: Either frlmgsumOLD (deprecated!) must be used in step 85, or step 84 must be adapted to comply with the new version of frlmgsum.
Alexander On Saturday, April 25, 2020 at 7:41:56 AM UTC+2, David A. Wheeler wrote: > > On Fri, 10 Apr 2020 03:33:42 -0700 (PDT), Thomas Brendan Leahy < > [email protected] <javascript:>> wrote: > > I've deleted the proof itself, but to give you an idea, here's an HTML > file > > I made. > ... > > I'm trying to recover your proof of aacllem. Even after a few renames > I can't *quite* make it work in mmj2. > > Below is the proof in mmj2 format. > mmj2 is reporting the following: > E-PA-0410 Theorem aacllem: Step 85: Unification failure in derivation > proof step frlmgsum. The step's formula and/or its hypotheses could not be > reconciled with the referenced Assertion. Try the Unify/Step Selector > Search to find unifiable assertions for the step. > > Suggestions? It's probably a tiny problem. > > --- David A. Wheeler > -- 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/ea114f6a-2e55-4bdb-b716-54fa2ce03aa7%40googlegroups.com.
