Exhaustion of variable names is a sort of theoretical concern, because "26 variables should be enough for anyone". In practice it usually just means that you can't be particularly descriptive with your variable naming. For automated theorem generation, I usually just make up $v/$f statements on the spot, so you obtain infinite variables that way. But set.mm mostly just sticks to its original alphabet set. Class variables are the most common, and those have a few more than 26 because of symbol variables like .+ that give you a bit more symbolic flexibility, while wff variables have a lot less than 26 because we don't have the whole greek alphabet, I think there is only 12 or so and I'm actually using the whole set in simp-11l. Generally speaking, if you need that many variables you probably should break your theorem down into more intelligible pieces and/or make more definitions, which can be used to encapsulate binders and free up some more variables for use.
On Thu, Mar 12, 2020 at 2:51 AM 'Stanislas Polu' via Metamath < [email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/CACZd_0zcyMSuAzFfhbEJCNp1WJwpWVE6_%3DkowJ6zrW5u%2BfYqSg%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/CAFXXJSu7C5%3Does%3D4ZgAkV1%3DKWiY2dZn1S5%2BXLgBcZpC4o7HnWw%40mail.gmail.com.
