On 02/12/2024 13:29, savask wrote:
I have a question: do you use some automation (tactics) to do substitutions into the identity, like deriving step 23 of your M<P file? Or you simply remember the movements by heart?
Recently I've been using Yamma. Unfortunately it does not have auto-transformations like MMJ2, so there is no tactics for automatically proving e.g. variable substitutions. Most of the time I work backwards, from the formula I want to prove. Yamma proposes a reduced list of theorems which could lead to that result, and I choose from the list, partly from my memory. Otherwise I'm either entering the formula and letting the tool find the correct theorem to apply, or remembering the name of the theorem I want to apply, and letting the tool build the resulting formula. -- 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 visit https://groups.google.com/d/msgid/metamath/c8811771-bd98-4d95-96b9-1839a1d73505%40gmx.net.
