Hi Jorge,
I am not sure what you mean by saying that it is given as a hypothesis. So,
I will explain as detailed as I can. It may seem obvious that F(a) = 4 from
the original edition of the problem formulated in the “human language”. But
it is not explicitly given in the collection of hypotheses I chose. The
closest hypothesis in my collection is hyp4: |- { x | ( F ` x ) = 4 } = { A
, B } (I switched back to class variables). However, Metamath doesn’t
understand meaning of statements. It can only compare statements symbol by
symbol. That’s why I have to prove |- ( F ` A ) = 4 before I can use it in
my proof.
The same problem may be formalized in many ways, and you can choose another
approach, which will explicitly include F(a) = 4 and maybe some obvious
calculations done. For example:
|- 0 < k
|- 0 < l
|- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) )
|- ( F ` A ) = 4
|- ( F ` B ) = 4
|- ( abs ` ( A - B ) ) = 6
|- ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ; 3 2 ) = C
These hypotheses also should describe the same problem, but they explicitly
include |- ( F ` A ) = 4 and you will not have to prove it. (actually these
two collections of hypotheses may be not exactly equivalent, but I hope it
is clear what I mean)
-
Igor
On Wednesday, October 16, 2024 at 12:28:21 PM UTC+2 jagra wrote:
> Hi Igor,
>
> I haven't tried the proof myself, a little short on time right now, but I
> have doubts about why you are trying to prove F(a) = 4 or F(b). It seems to
> me this is given, an hypothesis, right?
>
> Regards,
> Jorge
>
>
>
> On Wed, Oct 16, 2024 at 8:41 AM Igor Ieskov <[email protected]> wrote:
>
>> Hi Glauco,
>>
>>
>> Yes, this answers my question. Thank you very much. Also I found this
>> thread
>> <https://groups.google.com/g/metamath/c/1T18-hzCw5E/m/Igpc2gWFBAAJ>
>> contains other shortcuts used in the video.
>>
>>
>> I don’t have much experience with mmj2. I used it to repeat proofs from
>> David’s video tutorials, but not for creating my own proofs.
>>
>>
>> -
>>
>> Igor
>>
>>
>> On Tuesday, October 15, 2024 at 11:50:12 PM UTC+2 Glauco wrote:
>>
>>> Hi Igor,
>>>
>>> with regard to your question, yamma, for now, is similar to mmj2. Do you
>>> have some experience with mmj2?
>>>
>>> I tend to proof backwards, thus yamma may have a bias toward this
>>> approach.
>>>
>>> Did you see this simple video?
>>>
>>> https://www.youtube.com/watch?v=N7W0VBsbOcQ
>>>
>>> As you can see, when it has to prove
>>>
>>> |- E. x x e. { 1 }
>>>
>>> if you hit ctrl+space , intellisense shows you the labels that are more
>>> likely to move you in the right direction.
>>>
>>> The one I chose is the 6th one, that is ceqsexv2d (intellisense
>>> details clearly show me that's the one I'm looking for)
>>>
>>> I would not be able to know it myself, so it saves me some search time.
>>>
>>> eximii , the first one suggested, is not the right one, but I can easily
>>> see why it's, in general, a good candidate for the given statement
>>>
>>> HTH
>>> Glauco
>>>
>>>
>>>
>>> Il giorno lunedì 14 ottobre 2024 alle 22:48:36 UTC+2 [email protected]
>>> ha scritto:
>>>
>>>> Thank you Glauco and Mario for helpful answers. I will need some time
>>>> to analyze and understand everything you wrote.
>>>>
>>>>
>>>> For now, I have one question. Glauco, you mentioned that you developed
>>>> this proof using Yamma. Can you explain at a high level what steps you’ve
>>>> done in Yamma to come up with such a proof? I am asking for the proof
>>>> of |- ( F ` a ) = 4. No need to explain how to set up Yamma, it can be
>>>> found in its readme
>>>> <https://github.com/glacode/yamma/blob/master/README.md>. I am more
>>>> interested in how much of this proof was constructed by Yamma and how much
>>>> was manual work. I didn’t have time yet to try to prove this in Yamma, but
>>>> I will surely try. So, what I think would be interesting for me (and
>>>> probably for others) is a high level list of actions you’ve done to create
>>>> this proof. For example:
>>>>
>>>>
>>>> 1) put all required hypotheses and the goal statement to Yamma.
>>>>
>>>> 2) I know that for such kind of proofs elrab assertion is usually used,
>>>> so type its name in and unify (press CTRL+U). New steps appeared.
>>>>
>>>> 3) …
>>>>
>>>>
>>>> I will be very surprised if you’ve just provided the hypotheses and the
>>>> goal statement and Yamma found everything else!
>>>>
>>>>
>>>> Sorry, if I am requesting too much. You can respond as high level or
>>>> detailed depending on how much free time you have. I am asking because I
>>>> tried to prove this using mm-lamp. Since I don’t know set.mm
>>>> assertions well, I just searched for assertions which I thought could be
>>>> used in the proof and tried to combine them somehow. I am interested in
>>>> how
>>>> you came up with this proof (how much automation you used and how much
>>>> your
>>>> experience with set.mm).
>>>>
>>>>
>>>> BTW, it is Igor writing :)
>>>>
>>>>
>>>> -
>>>>
>>>> Igor
>>>>
>>>>
>>>> On Monday, October 14, 2024 at 5:05:35 PM UTC+2 Glauco wrote:
>>>>
>>>>> Below is a full contradiction derived.
>>>>>
>>>>>
>>>>> It's amazing to see how ChatGPT can understand set.mm even though I
>>>>> guess there's not much content, when compared to other subjects.
>>>>>
>>>>> Here's a brief "conversation" (not perfect, but close...):
>>>>>
>>>>> https://chatgpt.com/share/670d3203-1d2c-8010-bb5b-2e4105fc5379
>>>>>
>>>>>
>>>>>
>>>>> h1::temp4.1 |- { x e. RR | ( F ` x ) = 4 } = { a , b }
>>>>> 2::pnfex |- +oo e. _V
>>>>> 3::preq1 |- ( a = +oo -> { a , b } = { +oo , b } )
>>>>> 4:3:eqeq2d |- ( a = +oo -> ( { x e. RR | ( F ` x ) = 4 } =
>>>>> { a , b } <-> { x e. RR | ( F ` x ) = 4 } = { +oo , b } ) )
>>>>> 5:2,4,1:vtocl |- { x e. RR | ( F ` x ) = 4 } = { +oo , b }
>>>>> 6:2:prid1 |- +oo e. { +oo , b }
>>>>> 7:6,5:eleqtrri |- +oo e. { x e. RR | ( F ` x ) = 4 }
>>>>> 8::elrabi |- ( +oo e. { x e. RR | ( F ` x ) = 4 } -> +oo e.
>>>>> RR )
>>>>> 9:7,8:ax-mp |- +oo e. RR
>>>>> 10::pnfnre2 |- -. +oo e. RR
>>>>> qed:9,10:pm2.24ii |- F.
>>>>>
>>>>> $= ( cpnf cr wcel wfal cv cfv c4 wceq crab cpr pnfex prid1 preq1
>>>>> eqeq2d vtocl
>>>>> eleqtrri elrabi ax-mp pnfnre2 pm2.24ii )
>>>>> FGHZIFAJBKLMZAGNZHUFFFDJZOZUHFUIPQU
>>>>> HCJZUIOZMUHUJMCFPUKFMULUJUHUKFUIRSETUAUGAFGUBUCUDUE $.
>>>>>
>>>>>
>>>>> $d a x
>>>>> $d a b
>>>>> $d F a
>>>>>
>>>>> Il giorno lunedì 14 ottobre 2024 alle 16:25:31 UTC+2 [email protected]
>>>>> ha scritto:
>>>>>
>>>>>> That's the first part of the proof. The second part of the proof is
>>>>>> to show a contradiction from this, because +oo is in the RHS but not the
>>>>>> LHS of that equality.
>>>>>>
>>>>>> On Mon, Oct 14, 2024 at 3:24 PM Glauco <[email protected]> wrote:
>>>>>>
>>>>>>> I think I got it. Thank you very much for the insight.
>>>>>>>
>>>>>>> h1::temp4.1 |- { x e. RR | ( F ` x ) = 4 } = { a , b }
>>>>>>> 2::pnfex |- +oo e. _V
>>>>>>> 3::preq1 |- ( a = +oo -> { a , b } = { +oo , b } )
>>>>>>> 4:3:eqeq2d |- ( a = +oo -> ( { x e. RR | ( F ` x ) = 4 } =
>>>>>>> { a , b } <-> { x e. RR | ( F ` x ) = 4 } = { +oo , b } ) )
>>>>>>> qed:2,4,1:vtocl |- { x e. RR | ( F ` x ) = 4 } = { +oo , b }
>>>>>>>
>>>>>>> $= ( cv cfv c4 wceq cr crab cpr cpnf pnfex preq1 eqeq2d vtocl )
>>>>>>> AFBGHIAJKZCFZDF
>>>>>>> ZLZIRMTLZICMNSMIUAUBRSMTOPEQ $.
>>>>>>>
>>>>>>> $d a x
>>>>>>> $d a b
>>>>>>> $d F a
>>>>>>>
>>>>>>>
>>>>>>> Il giorno lunedì 14 ottobre 2024 alle 15:02:42 UTC+2 Glauco ha
>>>>>>> scritto:
>>>>>>>
>>>>>>>> Hi Mario,
>>>>>>>>
>>>>>>>> I'm sure you're right, and in fact I would use a class A and
>>>>>>>> something like ph -> A e. V as an additional hyp.
>>>>>>>>
>>>>>>>> But I cannot reproduce the contradiction off the top of my head; it
>>>>>>>> would be interesting to see it, to gain a deeper understanding.
>>>>>>>>
>>>>>>>> Can you please show a short proof? (do you proof something like
>>>>>>>> +oo e. RR ? )
>>>>>>>>
>>>>>>>> Thank you
>>>>>>>> Glauco
>>>>>>>>
>>>>>>>>
>>>>>>>> Il giorno lunedì 14 ottobre 2024 alle 14:28:43 UTC+2
>>>>>>>> [email protected] ha scritto:
>>>>>>>>
>>>>>>>>> It's not safe to make an assumption of the form |- { x e. RR | ( F
>>>>>>>>> ` x ) = 4 } = { a , b } because the variables a,b are implicitly
>>>>>>>>> universally quantified in the hypothesis, which means you can prove a
>>>>>>>>> contradiction from it. (Consider what happens if you use vtocl on the
>>>>>>>>> hypothesis to replace a by +oo.) You should either use class
>>>>>>>>> variables A,B as I indicated, or add a context ph -> before every
>>>>>>>>> assumption (which is *not* assumed to be disjoint from a,b).
>>>>>>>>>
>>>>>>>>> On Mon, Oct 14, 2024 at 2:12 PM Glauco <[email protected]>
>>>>>>>>> wrote:
>>>>>>>>>
>>>>>>>>>> I take it back, you can get away with { x | ( F ` x ) = 4 } ,
>>>>>>>>>> here's the proof (but for your larger goal, I doubt it's enough)
>>>>>>>>>>
>>>>>>>>>> h1::temp3.1 |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 )
>>>>>>>>>> ) - ( ( 2 x. k ) x. x ) ) + l ) )
>>>>>>>>>> h2::temp3.2 |- { x | ( F ` x ) = 4 } = { a , b }
>>>>>>>>>> 3::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) )
>>>>>>>>>> 4:3:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a )
>>>>>>>>>> = 4 ) )
>>>>>>>>>> 5::vex |- a e. _V
>>>>>>>>>> 6::nfmpt1 |- F/_ x ( x e. RR |-> ( ( ( k x. ( x ^ 2
>>>>>>>>>> ) ) - ( ( 2 x. k ) x. x ) ) + l ) )
>>>>>>>>>> 7:1,6:nfcxfr |- F/_ x F
>>>>>>>>>> 8::nfcv |- F/_ x a
>>>>>>>>>> 9:7,8:nffv |- F/_ x ( F ` a )
>>>>>>>>>> 10:9:nfeq1 |- F/ x ( F ` a ) = 4
>>>>>>>>>> 11:10,5,4:elabf |- ( a e. { x | ( F ` x ) = 4 } <-> ( F ` a )
>>>>>>>>>> = 4 )
>>>>>>>>>> 12::vex |- a e. _V
>>>>>>>>>> 13:12:prid1 |- a e. { a , b }
>>>>>>>>>> 14:13,2:eleqtrri |- a e. { x | ( F ` x ) = 4 }
>>>>>>>>>> qed:14,11:mpbi |- ( F ` a ) = 4
>>>>>>>>>>
>>>>>>>>>> $= ( cv cfv c4 wceq cab wcel cpr vex cr c2 co cmul prid1 cexp
>>>>>>>>>> cmin caddc nfmpt1
>>>>>>>>>> eleqtrri cmpt nfcxfr nfcv nffv nfeq1 fveq2 eqeq1d elabf mpbi )
>>>>>>>>>> DIZAIZCJZKLZA
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> MZNUPCJZKLZUPUPEIZOUTUPVCDPZUAHUFUSVBAUPAVAKAUPCACAQBIZUQRUBSTSRVETSUQTSUCSF
>>>>>>>>>> IUDSZUGGAQVFUEUHAUPUIUJUKVDUQUPLURVAKUQUPCULUMUNUO $.
>>>>>>>>>>
>>>>>>>>>> $d a x
>>>>>>>>>>
>>>>>>>>>> Il giorno lunedì 14 ottobre 2024 alle 13:53:35 UTC+2 Glauco ha
>>>>>>>>>> scritto:
>>>>>>>>>>
>>>>>>>>>>> Since the
>>>>>>>>>>>
>>>>>>>>>>> $d F x
>>>>>>>>>>>
>>>>>>>>>>> constraint would conflict with your F definition, here is an
>>>>>>>>>>> alternative version
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> h1::temp3.1 |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2
>>>>>>>>>>> ) ) - ( ( 2 x. k ) x. x ) ) + l ) )
>>>>>>>>>>> h2::temp3.2 |- { x e. RR | ( F ` x ) = 4 } = { a , b }
>>>>>>>>>>> 3::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) )
>>>>>>>>>>> 4:3:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a
>>>>>>>>>>> ) = 4 ) )
>>>>>>>>>>> 5::nfcv |- F/_ x a
>>>>>>>>>>> 6::nfcv |- F/_ x RR
>>>>>>>>>>> 7::nfmpt1 |- F/_ x ( x e. RR |-> ( ( ( k x. ( x ^
>>>>>>>>>>> 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) )
>>>>>>>>>>> 8:1,7:nfcxfr |- F/_ x F
>>>>>>>>>>> 9:8,5:nffv |- F/_ x ( F ` a )
>>>>>>>>>>> 10:9:nfeq1 |- F/ x ( F ` a ) = 4
>>>>>>>>>>> 11:5,6,10,4:elrabf |- ( a e. { x e. RR | ( F ` x ) = 4 } <-> (
>>>>>>>>>>> a e. RR /\ ( F ` a ) = 4 ) )
>>>>>>>>>>> 12::vex |- a e. _V
>>>>>>>>>>> 13:12:prid1 |- a e. { a , b }
>>>>>>>>>>> 14:13,2:eleqtrri |- a e. { x e. RR | ( F ` x ) = 4 }
>>>>>>>>>>> 15:14,11:mpbi |- ( a e. RR /\ ( F ` a ) = 4 )
>>>>>>>>>>> qed:15:simpri |- ( F ` a ) = 4
>>>>>>>>>>>
>>>>>>>>>>> $= ( cv cr wcel cfv c4 wceq crab wa nfcv c2 co cmul cpr vex
>>>>>>>>>>> prid1 eleqtrri cexp
>>>>>>>>>>> cmin caddc cmpt nfmpt1 nfcxfr nffv nfeq1 fveq2 eqeq1d elrabf
>>>>>>>>>>> mpbi simpri ) D
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> IZJKZURCLZMNZURAIZCLZMNZAJOZKUSVAPURUREIZUAVEURVFDUBUCHUDVDVAAURJAURQZAJQAUT
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> MAURCACAJBIZVBRUESTSRVHTSVBTSUFSFIUGSZUHGAJVIUIUJVGUKULVBURNVCUTMVBURCUMUNUO
>>>>>>>>>>> UPUQ $.
>>>>>>>>>>>
>>>>>>>>>>> $d a x
>>>>>>>>>>>
>>>>>>>>>>> Il giorno lunedì 14 ottobre 2024 alle 13:42:45 UTC+2 Glauco ha
>>>>>>>>>>> scritto:
>>>>>>>>>>>
>>>>>>>>>>>> Hi Jorge,
>>>>>>>>>>>>
>>>>>>>>>>>> with Yamma you get something like this (I doubt you can get
>>>>>>>>>>>> away with { x | ( F ` x ) = 4 }, for instance ( F ` +oo ) is
>>>>>>>>>>>> not "well-defined" )
>>>>>>>>>>>>
>>>>>>>>>>>> ```
>>>>>>>>>>>> $theorem temp3
>>>>>>>>>>>>
>>>>>>>>>>>> * comments
>>>>>>>>>>>>
>>>>>>>>>>>> h1::temp3.1 |- { x e. RR | ( F ` x ) = 4 } = { a , b }
>>>>>>>>>>>> 2::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) )
>>>>>>>>>>>> 3:2:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a
>>>>>>>>>>>> ) = 4 ) )
>>>>>>>>>>>> 4:3:elrab |- ( a e. { x e. RR | ( F ` x ) = 4 } <->
>>>>>>>>>>>> ( a e. RR /\ ( F ` a ) = 4 ) )
>>>>>>>>>>>> 5::vex |- a e. _V
>>>>>>>>>>>> 6:5:prid1 |- a e. { a , b }
>>>>>>>>>>>> 7:6,1:eleqtrri |- a e. { x e. RR | ( F ` x ) = 4 }
>>>>>>>>>>>> 8:7,4:mpbi |- ( a e. RR /\ ( F ` a ) = 4 )
>>>>>>>>>>>> qed:8:simpri |- ( F ` a ) = 4
>>>>>>>>>>>>
>>>>>>>>>>>> $= ( cv cr wcel cfv c4 wceq crab wa cpr vex prid1 eleqtrri
>>>>>>>>>>>> fveq2 eqeq1d elrab
>>>>>>>>>>>> mpbi simpri )
>>>>>>>>>>>> CFZGHZUCBIZJKZUCAFZBIZJKZAGLZHUDUFMUCUCDFZNUJUCUKCOPEQUIUFAUCG
>>>>>>>>>>>> UGUCKUHUEJUGUCBRSTUAUB $.
>>>>>>>>>>>>
>>>>>>>>>>>> $d F x
>>>>>>>>>>>> $d a x
>>>>>>>>>>>> ```
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> Il giorno lunedì 14 ottobre 2024 alle 12:40:47 UTC+2
>>>>>>>>>>>> [email protected] ha scritto:
>>>>>>>>>>>>
>>>>>>>>>>>>> I wanted to check how far I can get in formalizing this
>>>>>>>>>>>>> problem and its solution. But I stuck in the very beginning.
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Firstly, I formalized the initial conditions as Mario
>>>>>>>>>>>>> suggested:
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> hyp1: |- 0 < k
>>>>>>>>>>>>>
>>>>>>>>>>>>> hyp2: |- 0 < l
>>>>>>>>>>>>>
>>>>>>>>>>>>> hyp3: |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k
>>>>>>>>>>>>> ) x. x ) ) + l ) )
>>>>>>>>>>>>>
>>>>>>>>>>>>> hyp4: |- { x | ( F ` x ) = 4 } = { a , b }
>>>>>>>>>>>>>
>>>>>>>>>>>>> hyp5: |- ( ( ( a - b ) ^ 2 ) + ( ( ( F ` a ) - ( F ` b ) ) ^ 2
>>>>>>>>>>>>> ) ) = ( 6 ^ 2 )
>>>>>>>>>>>>>
>>>>>>>>>>>>> hyp6: |- ( ( ( a ^ 2 ) + ( ( F ` a ) ^ 2 ) ) + ( ( b ^ 2 ) + (
>>>>>>>>>>>>> ( F ` b ) ^ 2 ) ) ) = c
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> I used { a , b } instead of { A , B } because then I can
>>>>>>>>>>>>> easily prove |- a e. _V, which is used in the proof below.
>>>>>>>>>>>>> Also, as I understand, a and b represent x-coordinates of the
>>>>>>>>>>>>> corresponding
>>>>>>>>>>>>> points.
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Next, I wanted to simplify hyp5, by proving that F(a) = F(b) =
>>>>>>>>>>>>> 4, so the hyp5 would be |- ( ( a - b ) ^ 2 ) = ( 6 ^ 2 ). But
>>>>>>>>>>>>> that’s where I am stuck. I can prove |- [ a / x ] ( F ` x ) =
>>>>>>>>>>>>> 4 which looks a right direction to move in:
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> 1| | vex | |- a e. _V
>>>>>>>>>>>>>
>>>>>>>>>>>>> 2| 1 | prid1 | |- a e. { a , b }
>>>>>>>>>>>>>
>>>>>>>>>>>>> 3| | hyp4 | |- { x | ( F ` x ) = 4 } = { a , b }
>>>>>>>>>>>>>
>>>>>>>>>>>>> 4| 3 | eleq2i | |- ( a e. { x | ( F ` x ) = 4 } <-> a e. {
>>>>>>>>>>>>> a , b } )
>>>>>>>>>>>>>
>>>>>>>>>>>>> 5| 2,4 | mpbir | |- a e. { x | ( F ` x ) = 4 }
>>>>>>>>>>>>>
>>>>>>>>>>>>> 6| | df-clab | |- ( a e. { x | ( F ` x ) = 4 } <-> [ a / x
>>>>>>>>>>>>> ] ( F ` x ) = 4 )
>>>>>>>>>>>>>
>>>>>>>>>>>>> 7| 5,6 | mpbi | |- [ a / x ] ( F ` x ) = 4
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> But I still cannot prove |- ( F ` a ) = 4. Any suggestions
>>>>>>>>>>>>> what approaches I can try to prove this?
>>>>>>>>>>>>>
>>>>>>>>>>>>> On Sunday, July 28, 2024 at 11:54:47 PM UTC+2 [email protected]
>>>>>>>>>>>>> wrote:
>>>>>>>>>>>>>
>>>>>>>>>>>>>> On Sun, Jul 28, 2024 at 11:43 PM Glauco <[email protected]>
>>>>>>>>>>>>>> wrote:
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I maybe wrong, but my feeling is that what Jagra calls A ,
>>>>>>>>>>>>>>> in Mario's translation is actually < A , 4 > (or < A, F(A) >
>>>>>>>>>>>>>>> , if you
>>>>>>>>>>>>>>> prefer).
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> I meant it to be interpreted as <A, F(A)>, and part of the
>>>>>>>>>>>>>> proof would be showing that F(A) = 4 so that the rest of the
>>>>>>>>>>>>>> statement
>>>>>>>>>>>>>> simplifies. (But that would seem to be part of the proof, not
>>>>>>>>>>>>>> the
>>>>>>>>>>>>>> formalization of the statement, if we want to read it literally.)
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> --
>>>>>>>>>> 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/161f583c-22bf-4699-b663-92652793f9c3n%40googlegroups.com
>>>>>>>>>>
>>>>>>>>>> <https://groups.google.com/d/msgid/metamath/161f583c-22bf-4699-b663-92652793f9c3n%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/4c4161e9-ccfc-4289-a19d-1bdcb701bbfbn%40googlegroups.com
>>>>>>>
>>>>>>> <https://groups.google.com/d/msgid/metamath/4c4161e9-ccfc-4289-a19d-1bdcb701bbfbn%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/0466031a-8f6f-4d1d-8a69-8ff2351dc4f6n%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/metamath/0466031a-8f6f-4d1d-8a69-8ff2351dc4f6n%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/032ef015-c78e-45c2-ad73-71f4419f8986n%40googlegroups.com.
