This is a minor design decision in the metamath spec. It's nice to be explicit about this, but you can always safely assume that all dummy variables are disjoint from all other variables with no loss in the generality of the theorem, and some verifiers even do this automatically. But the spec itself requires that these annotations be present, so that would not be strictly conforming.
Mario On Thu, Mar 12, 2020 at 12:50 AM 'Stanislas Polu' via Metamath < [email protected]> wrote: > Wanted to follow-up on the question above that may have been lost in > translation, if anyone could shed some light on it: > > > One question that remains pertains to DVs: I'm surprised to see the DVs > bubble up even if the variable does not appear in the final statement? Why > is that the case? > > Thanks! > > -stan > > On Mon, Mar 9, 2020 at 1:41 PM Stanislas Polu <[email protected]> wrote: > >> Finished proof available here: >> https://github.com/metamath/set.mm/compare/develop...spolu:spolu-mathbox?expand=1 >> >> What an adventure, thank you all for your precious help! >> >> ``` >> $d B c t $. $d B u v $. $d B x $. $d B t y $. $d F c t $. $d F u v $. >> $d F x $. $d F t y $. $d G c t $. $d G u v $. $d G x $. $d G t y $. >> $d c ph t $. $d ph u v $. $d ph x $. $d ph t y $. $d u y $. >> imo72b2.1 $e |- ( ph -> F : RR --> RR ) $. >> imo72b2.2 $e |- ( ph -> G : RR --> RR ) $. >> imo72b2.4 $e |- ( ph -> B e. RR ) $. >> imo72b2.5 $e |- ( ph -> A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( >> F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) ) $. >> imo72b2.6 $e |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 ) $. >> imo72b2.7 $e |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) $. >> $( IMO 1972 B2. $) >> imo72b2 $p |- ( ph -> ( abs ` ( G ` B ) ) <_ 1 ) $= >> ``` >> >> One question that remains pertains to DVs: I'm surprised to see the DVs >> bubble up even if the variable does not appear in the final statement? Why >> is that the case? >> >> Also, to answer my own question as well as react on Benoit's remark: >> >> > > One question for which I'm looking guidance is on using quantifiers >> or not. >> >> > That's a very important question, and I hope someone with more >> experience will be able to shed some insight. In particular, if one has a >> hypothesis, say, "E. x ph", then it is common to see in textbooks things >> like "Let y be such that ph(y). Then [subproof], so [conclusion which does >> not depend on y]. Therefore, [that conclusion]." I would formalize it in >> set.mm by using the "deduction style" and prepending "[. y / x ]. ph" as >> an antecedent to each line of the subproof. Maybe there are better >> strategies ? >> >> From the experience formalizing imo72b2, I think that when relying on >> natural deduction forms, hypotheses should favor quantifiers (stronger) >> while conclusions shouldn't (easier to work with). Going from a lemma >> without quantifier to a resolved goal with quantifier is relatively easy >> with rspcdv, rspcedvd and the likes. >> >> -stan >> >> On Sat, Mar 7, 2020 at 1:25 PM Stanislas Polu <[email protected]> wrote: >> >>> Thanks! Makes perfect sense. I will adapt the proof accordingly! >>> >>> -stan >>> >>> On Sat, Mar 7, 2020 at 10:47 AM Mario Carneiro <[email protected]> >>> wrote: >>> >>>> Yep, you correctly identified eliman0 as the bad lemma here. I hadn't >>>> heard of it but it's using a trick to avoid having to prove that the input >>>> is in the domain of the function. Using metamath.exe, I searched for this >>>> pattern and got a few results: >>>> >>>> MM> sea * '( ? ` ? ) e. ( ? " ? )'/j >>>> 19563 eliman0 $p |- ( ( A e. B /\ -. ( F ` A ) = (/) ) -> ( F ` A ) e. >>>> ( F " B >>>> ) ) >>>> 20603 funfvima $p |- ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) >>>> e. ( F >>>> " A ) ) ) >>>> 20604 funfvima2 $p |- ( ( Fun F /\ A C_ dom F ) -> ( B e. A -> ( F ` B >>>> ) e. ( F >>>> " A ) ) ) >>>> 20611 fnfvima $p |- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( >>>> F " S ) >>>> ) >>>> 20740 f1elima $p |- ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( ( F ` >>>> X ) e. >>>> ( F " Y ) <-> X e. Y ) ) >>>> 79323 kqfvima $e |- F = ( x e. X |-> { y e. J | x e. y } ) $p |- ( ( J >>>> e. ( >>>> TopOn ` X ) /\ U e. J /\ A e. X ) -> ( A e. U <-> ( F ` A ) e. ( F >>>> " U ) ) >>>> ) >>>> >>>> and the actual theorems you want to reference are either funfvima, >>>> funfvima2, or fnfvima depending on how the function is presented. (Arguably >>>> eliman0 should be moved to after fnfvima and given a more similar name, >>>> e.g. fviman0.) In this case, the function has known domain and range so I >>>> would go for fnfvima, using fnco to prove that ( abs o. F ) Fn RR. >>>> >>>> >>>> On Fri, Mar 6, 2020 at 11:59 PM 'Stanislas Polu' via Metamath < >>>> [email protected]> wrote: >>>> >>>>> (fvco3d is a natural deduction form of fvco3 proved here: >>>>> https://github.com/metamath/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65#diff-12dc1484b058d1ee6cb68a74194d66c7R641421-R641429 >>>>> ) >>>>> >>>>> -stan >>>>> >>>>> On Sat, Mar 7, 2020 at 8:54 AM Stanislas Polu <[email protected]> >>>>> wrote: >>>>> >>>>>> Interesting! >>>>>> >>>>>> It basically comes from an attempt at satisfying the conditions >>>>>> for eliman0. Here's the full proof draft: >>>>>> >>>>>> ``` >>>>>> $( <MM> <PROOF_ASST> THEOREM=imo72b2lem1 LOC_AFTER=? >>>>>> >>>>>> h1::imo72b2lem1.1 |- ( ph -> F : RR --> RR ) >>>>>> h2::imo72b2lem1.7 |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) >>>>>> h3::imo72b2lem0.6 |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 >>>>>> ) >>>>>> >>>>>> !d84:: |- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= >>>>>> (/) ) >>>>>> d83:d84:adantrr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>>> -> ( ( abs o. F ) ` x ) =/= (/) ) >>>>>> d81:d83:neneqd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>>> -. ( ( abs o. F ) ` x ) = (/) ) >>>>>> >>>>>> d95:1:ffvelrnda |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR ) >>>>>> d94:d95:adantrr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>>> ( F ` x ) e. RR ) >>>>>> d92:d94:recnd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>>> -> ( F ` x ) e. CC ) >>>>>> d93::simprr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>>> ( F ` x ) =/= 0 ) >>>>>> d91:d92,d93:absrpcld |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>>> -> ( abs ` ( F ` x ) ) e. RR+ ) >>>>>> d9:d91:rpgt0d |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>>> 0 < ( abs ` ( F ` x ) ) ) >>>>>> >>>>>> d80::simprl |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>>> x e. RR ) >>>>>> d82::eliman0 |- ( ( x e. RR /\ -. ( ( abs o. F ) ` x ) = (/) >>>>>> ) -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) ) >>>>>> d75:d80,d81,d82:syl2anc |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) >>>>>> ) -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) ) >>>>>> oeqaa::imaco |- ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) ) >>>>>> d71:d75,oeqaa:syl6eleq |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) >>>>>> ) -> ( ( abs o. F ) ` x ) e. ( abs " ( F " RR ) ) ) >>>>>> d73:1:adantr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>>> F : RR --> RR ) >>>>>> d74::simprl |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>>> x e. RR ) >>>>>> d72:d73,d74:fvco3d |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>>> ( ( abs o. F ) ` x ) = ( abs ` ( F ` x ) ) ) >>>>>> d7:d72,d71:eqeltrrd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>>> -> ( abs ` ( F ` x ) ) e. ( abs " ( F " RR ) ) ) >>>>>> >>>>>> d10::simpr |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>>> /\ z = ( abs ` ( F ` x ) ) ) -> z = ( abs ` ( F ` x ) ) ) >>>>>> d8:d10:breq2d |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>>> /\ z = ( abs ` ( F ` x ) ) ) -> ( 0 < z <-> 0 < ( abs ` ( F ` x ) ) ) ) >>>>>> >>>>>> d6:d7,d8,d9:rspcedvd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>>> -> E. z e. ( abs " ( F " RR ) ) 0 < z ) >>>>>> qed:2,d6:rexlimddv |- ( ph -> E. z e. ( abs " ( F " RR ) ) 0 < z ) >>>>>> >>>>>> $) >>>>>> >>>>>> -stan >>>>>> >>>>>> On Fri, Mar 6, 2020 at 11:58 PM Mario Carneiro <[email protected]> >>>>>> wrote: >>>>>> >>>>>>> The composition function value combination is easy enough to >>>>>>> eliminate using fvco, but the equality to the empty set is a type error, >>>>>>> because the lhs is a real number and the question of whether the empty >>>>>>> set >>>>>>> is a real number is deliberately left ambiguous by the real number >>>>>>> axioms. >>>>>>> So I would like to know what steps got you to this point. There are some >>>>>>> function value theorems that assume this as a "convenience" but there >>>>>>> should be analogues of them that don't (probably with some other >>>>>>> assumption >>>>>>> like the function is a set). >>>>>>> >>>>>>> On Fri, Mar 6, 2020 at 8:02 AM 'Stanislas Polu' via Metamath < >>>>>>> [email protected]> wrote: >>>>>>> >>>>>>>> Thanks again Mario! >>>>>>>> >>>>>>>> I made more progress towards the final demonstration of the full >>>>>>>> IMO problem. Working on the following lemma: >>>>>>>> >>>>>>>> ``` >>>>>>>> h1::imo72b2lem1.1 |- ( ph -> F : RR --> RR ) >>>>>>>> >>>>>>>> h2::imo72b2lem1.7 |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) >>>>>>>> >>>>>>>> h3::imo72b2lem0.6 |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ >>>>>>>> 1 ) >>>>>>>> ``` >>>>>>>> >>>>>>>> I need to prove the following goal which seems pretty obvious but >>>>>>>> I'm struggling to find a way to discharge it: >>>>>>>> >>>>>>>> ``` >>>>>>>> d84:: |- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= (/) >>>>>>>> ) >>>>>>>> ``` >>>>>>>> >>>>>>>> Any idea on how to proceed with this? >>>>>>>> >>>>>>>> Thanks thanks! >>>>>>>> >>>>>>>> -stan >>>>>>>> >>>>>>>> On Thu, Mar 5, 2020 at 6:27 PM Mario Carneiro <[email protected]> >>>>>>>> wrote: >>>>>>>> >>>>>>>>> There is a theorem specifically for that translation, something >>>>>>>>> like A. x e. ( F " A ) P[x] <-> A. y e. A P[( F ` y )]. It's probably >>>>>>>>> called ralima but you've caught me on the bus again. >>>>>>>>> >>>>>>>>> Mario >>>>>>>>> >>>>>>>>> On Thu, Mar 5, 2020, 8:07 AM 'Stanislas Polu' via Metamath < >>>>>>>>> [email protected]> wrote: >>>>>>>>> >>>>>>>>>> Thanks Mario! >>>>>>>>>> >>>>>>>>>> I just finished formalizing the following lemma (which is a good >>>>>>>>>> chunk of the proof \o/): >>>>>>>>>> >>>>>>>>>> ``` >>>>>>>>>> $d F c x $. $d c ph x $. >>>>>>>>>> imo72b2lem.1 $e |- ( ph -> F : RR --> RR ) $. >>>>>>>>>> imo72b2lem.2 $e |- ( ph -> G : RR --> RR ) $. >>>>>>>>>> imo72b2lem.3 $e |- ( ph -> A e. RR ) $. >>>>>>>>>> imo72b2lem.4 $e |- ( ph -> B e. RR ) $. >>>>>>>>>> imo72b2lem.5 $e |- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - >>>>>>>>>> B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) $. >>>>>>>>>> imo72b2lem.6 $e |- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ >>>>>>>>>> 1 ) $. >>>>>>>>>> imo72b2lem.7 $e |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) $. >>>>>>>>>> >>>>>>>>>> imo72b2lem $p |- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G >>>>>>>>>> ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) $= >>>>>>>>>> ``` >>>>>>>>>> >>>>>>>>>> Proof here: >>>>>>>>>> https://github.com/spolu/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65 >>>>>>>>>> >>>>>>>>>> One thing I'm quite dissatisfied with is the shape of >>>>>>>>>> `imo72b2lem.6`. I'd much rather have the more natural/intuitive >>>>>>>>>> expression >>>>>>>>>> `|- ( ph -> A. x e. RR ( abs ` ( F `x ) ) <_ 1 )` but I completely >>>>>>>>>> failed >>>>>>>>>> to prove imo72b2lem.6 from it. Any help on this would be greatly >>>>>>>>>> appreciated! >>>>>>>>>> >>>>>>>>>> -stan >>>>>>>>>> >>>>>>>>>> On Wed, Mar 4, 2020 at 8:45 PM Mario Carneiro <[email protected]> >>>>>>>>>> wrote: >>>>>>>>>> >>>>>>>>>>> Can't look right now, but you should search for a theorem of the >>>>>>>>>>> form A = (/) <-> ( F " A ) = (/) . >>>>>>>>>>> >>>>>>>>>>> On Wed, Mar 4, 2020, 11:30 AM 'Stanislas Polu' via Metamath < >>>>>>>>>>> [email protected]> wrote: >>>>>>>>>>> >>>>>>>>>>>> I'm now looking to prove that `( abs " ( F " RR ) ) =/= (/)` >>>>>>>>>>>> given `F : RR --> RR`. From my exploration of the definition of >>>>>>>>>>>> --> I >>>>>>>>>>>> believe this should be enough but I don't see an easy path towards >>>>>>>>>>>> that? >>>>>>>>>>>> Would anybody have an example in mind that could give me a little >>>>>>>>>>>> bit of >>>>>>>>>>>> inspiration? >>>>>>>>>>>> >>>>>>>>>>>> Thanks for the continued support! >>>>>>>>>>>> >>>>>>>>>>>> -stan >>>>>>>>>>>> >>>>>>>>>>>> On Wed, Mar 4, 2020 at 6:29 PM Benoit <[email protected]> >>>>>>>>>>>> wrote: >>>>>>>>>>>> >>>>>>>>>>>>> Stan: you're right about the need to prove this (if using >>>>>>>>>>>>> explicit substitution): look for the utility theorems exchanging >>>>>>>>>>>>> [. / ]. >>>>>>>>>>>>> with other symbols (quantifiers, operations). As said by Jim and >>>>>>>>>>>>> Thierry, >>>>>>>>>>>>> who are more experienced in proof building, implicit substitution >>>>>>>>>>>>> might be >>>>>>>>>>>>> easier to use. I think it is instructive to compare the details >>>>>>>>>>>>> of both >>>>>>>>>>>>> proving styles on a specific example (e.g. ralbidv, suggested by >>>>>>>>>>>>> Thierry, >>>>>>>>>>>>> would be analogous to exchanging [. / ]. with A.). >>>>>>>>>>>>> >>>>>>>>>>>>> Still, I think adding what I called rspesbcd could prove >>>>>>>>>>>>> useful (if it is not already in set.mm under another label; I >>>>>>>>>>>>> cannot search now, but it probably is already somewhere). >>>>>>>>>>>>> >>>>>>>>>>>>> Benoît >>>>>>>>>>>>> >>>>>>>>>>>>> -- >>>>>>>>>>>>> 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/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.com >>>>>>>>>>>>> <https://groups.google.com/d/msgid/metamath/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%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 [email protected]. >>>>>>>>>>>> To view this discussion on the web visit >>>>>>>>>>>> https://groups.google.com/d/msgid/metamath/CACZd_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%40mail.gmail.com >>>>>>>>>>>> <https://groups.google.com/d/msgid/metamath/CACZd_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%40mail.gmail.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 [email protected]. >>>>>>>>>>> To view this discussion on the web visit >>>>>>>>>>> https://groups.google.com/d/msgid/metamath/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%40mail.gmail.com >>>>>>>>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%40mail.gmail.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 [email protected]. >>>>>>>>>> To view this discussion on the web visit >>>>>>>>>> https://groups.google.com/d/msgid/metamath/CACZd_0zgFkBD0kOaAXNGyB3PL18Qt06uSHV%3DEmwOjh6Rk5j3OQ%40mail.gmail.com >>>>>>>>>> <https://groups.google.com/d/msgid/metamath/CACZd_0zgFkBD0kOaAXNGyB3PL18Qt06uSHV%3DEmwOjh6Rk5j3OQ%40mail.gmail.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 [email protected]. >>>>>>>>> To view this discussion on the web visit >>>>>>>>> https://groups.google.com/d/msgid/metamath/CAFXXJSs4iVxdk7Uz1_bW-heUVCJy-CMGENLNtzWd8%2B12rFEVBQ%40mail.gmail.com >>>>>>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSs4iVxdk7Uz1_bW-heUVCJy-CMGENLNtzWd8%2B12rFEVBQ%40mail.gmail.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 [email protected]. >>>>>>>> To view this discussion on the web visit >>>>>>>> https://groups.google.com/d/msgid/metamath/CACZd_0x2N3k16mC%2Byc_%3D6HvNQ3OWpAXtQ3fHkMv%3DPqERwFR60Q%40mail.gmail.com >>>>>>>> <https://groups.google.com/d/msgid/metamath/CACZd_0x2N3k16mC%2Byc_%3D6HvNQ3OWpAXtQ3fHkMv%3DPqERwFR60Q%40mail.gmail.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 [email protected]. >>>>>>> To view this discussion on the web visit >>>>>>> https://groups.google.com/d/msgid/metamath/CAFXXJSv0pGnDb%2Bfae5_ZS_mAK_R6MeMQPAL4gsHD-9S5g2XSVQ%40mail.gmail.com >>>>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSv0pGnDb%2Bfae5_ZS_mAK_R6MeMQPAL4gsHD-9S5g2XSVQ%40mail.gmail.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 [email protected]. >>>>> >>>> To view this discussion on the web visit >>>>> https://groups.google.com/d/msgid/metamath/CACZd_0yzRWT%3DZn6qPpgXPbzSabuOqHVSLW6uG9aF6S6yYht5mA%40mail.gmail.com >>>>> <https://groups.google.com/d/msgid/metamath/CACZd_0yzRWT%3DZn6qPpgXPbzSabuOqHVSLW6uG9aF6S6yYht5mA%40mail.gmail.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 [email protected]. >>>> To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/metamath/CAFXXJSutmF6LrPLUHM%3DoBbd5d_4kE8jeM9j-gFsc9tnYVU4Mcg%40mail.gmail.com >>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSutmF6LrPLUHM%3DoBbd5d_4kE8jeM9j-gFsc9tnYVU4Mcg%40mail.gmail.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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CACZd_0wpSzR5JhXYHkGLSq9F%2ByUVc_p-JAZ%2BnX5gO26gKsz82A%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CACZd_0wpSzR5JhXYHkGLSq9F%2ByUVc_p-JAZ%2BnX5gO26gKsz82A%40mail.gmail.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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStM%2BGKK%3DpcBdeyNUr9pUe78pbNsdeeuu7jL8vLtTUMEaA%40mail.gmail.com.
