That error message means that the theorem df-bl.tick has a statement that does not match the expression |- ( A = B '. <-> ( A = B ^. 1 ) ) that you have provided. It's difficult to say more without seeing the rest of the code (and in particular, the definition of `df-bl.tick`).
Q1: No, this is a fatal error, the proof is not correct as written. One way you can try to clear things up is to delete the statement (just the |- ( A = B '. <-> ( A = B ^. 1 ) ) part) and let mmj2 fill it in for you. The only steps you can't delete are the hypotheses IIRC. Q2: I think there isn't any centralized listing other than the source code: https://github.com/digama0/mmj2/blob/1cd95c1fe4435899c8575644fccb412dd77d79e4/src/main/java/mmj/pa/PaConstants.java#L2790-L2794 . In general you can search the repo for uses of the constant which might have some additional clues about it, but most of them carry a decent amount of explanation text which will be more helpful than looking at the code. Q3: Yes, because set.mm only accepts completed proofs, and mmj2 will not produce a completed proof (a block starting with $= at the bottom of the file) until all unification errors are fixed and missing steps are filled in. On Thu, Feb 1, 2024 at 10:59 AM Brian Larson <brianralphlar...@gmail.com> wrote: > I much enjoy using mmj2, and am often amazed at how its unification > deduces a theorem to solve qed when I think I've got a couple more steps to > go. However, sometimes I get failure in its final unification check. > > The error message: > E-PA-0410 Theorem bl.tkeq: Step 100: Unification failure in derivation > proof step df-bl.tick. 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. > --------------------------------------------------------- > > The culprit: > 100::df-bl.tick |- ( A = B '. <-> ( A = B ^. 1 ) ) > > '. and ^. are modal logic operators which determine in which "world" > variables and predicates made with them should be evaluated: A must equal > B one thread period hence. > > Both operators can be applied to wffs or classes: > $( Define ` ( ph ^. A ) ` as a wff $) > wts $a wff ( ph ^. A ) $. > > $( Define ` ( A ^. B ) ` as a class $) > clts $a class ( A ^. B ) $. > > $( Define ` ph '. ` as a wff $) > wtick $a wff ph '. $. > > $( Define ` A '. ` as a class $) > ctick $a class A '. $. > > For other theorems which encountered this problem, I used MM-PA, and then > included such theorems in the ProofAsstUnifySearchExclude list. > > Q1) Is there some clever RunParamFile setting which will avoid the error? > Q2) Where can the list of error codes like E-PA-0410 be found? > Q3) Will the mmj2 check preclude such theorems from acceptance into > set.mm? > > > --Brian > > > -- > 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/e6bd6e24-9110-49cc-ac8b-08128a7828abn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/e6bd6e24-9110-49cc-ac8b-08128a7828abn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuBCQpLVCxm-PEhvBuNNti_soxCjEML5d%3Ds-5-kYXbsew%40mail.gmail.com.
