Thanks! Very clear. I was first worried about having misunderstood something fundamental about DVs (thanks for clarifying) and secondly about exhaustion of variable names which somewhat hurts the user experience but I presume it's a minor point.
-stan On Thu, Mar 12, 2020 at 10:20 AM Mario Carneiro <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/CAFXXJStM%2BGKK%3DpcBdeyNUr9pUe78pbNsdeeuu7jL8vLtTUMEaA%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_0zcyMSuAzFfhbEJCNp1WJwpWVE6_%3DkowJ6zrW5u%2BfYqSg%40mail.gmail.com.
