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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e6bd6e24-9110-49cc-ac8b-08128a7828abn%40googlegroups.com.
