*> This is a typo, the theorem requires a and b to be disjoint. …*
Got it. Thank you Mario. Here is my video https://drive.google.com/file/d/1B_hiEfuP8KE3L_6uTnfdD7wkiLP15IIp/view?usp=sharing A couple of comments to the video. The volume may spike suddenly, so don't listen at high volume. At 13:15, I didn't manage to clearly explain the difference between how matching and unification work in mm-lamp. Matching can replace all kinds of variables but it can do that in the top expression only. Unification can replace variables in both expressions but it can replace meta-variables only. On Wednesday, December 4, 2024 at 11:46:31 AM UTC+1 savask wrote: > > I proved the fourth theorem. It seems one hypothesis is not needed. > > That's impressive, it didn't cross my mind that one need not assume the > second operation to be closed. > > > This proof is way too long so probably I used a very inefficient > approach. > > I'm also surprised at the length, given that the proof I know (from > wikipedia...) is quite short. In hindsight, I probably should have split > the task into smaller subtasks anyway, maybe I will do so in a revised > version of the problem set. > -- 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/6b0ab2a1-7c8d-4523-9c31-8221dbe15135n%40googlegroups.com.
