I'd love to help, but I'm not so great at knowing all of HOL's definitions.
It would be great if you gave an informal explanation of the meanings of
the symbols in the definition and I would take a stab at a sketch of a
formal proof.
Mario
On Mon, Feb 8, 2016 at 7:28 PM, Ramana Kumar <[email protected]>
wrote:
> Scott informed me that it is likely false (e.g., take m = 1 and a = 2). I
> can add additional assumptions that may help, though.
>
> Alternatively, I have a variant of the problem that looks like this:
>
> 0. m < dimword (:'a)
> 1. a <= m
> 2. 0 < m
> 3. 0 < a
> ----------------------------
> n2w m - n2w a < n2w m
>
> That one seems more likely to be true. But how to prove it?
>
> On 9 February 2016 at 10:02, Ramana Kumar <[email protected]>
> wrote:
>
>> Hi,
>>
>> Does anyone know whether the following goal is true or false?
>>
>> How would you prove it?
>>
>> If it's false, under what reasonable additional assumptions would it be
>> true?
>>
>> 0. m < dimword (:α)
>> 1. m < a
>> 2. 0 < m
>> ------------------------------------
>> n2w m − n2w a < n2w m
>>
>> Cheers,
>> Ramana
>>
>
>
>
> ------------------------------------------------------------------------------
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
