Yes, I want the set of first components of the pairs. I replaced S with A,
and used IMAGE FST (A CROSS A), but the problem is not solved.
On Fri, Feb 5, 2016 at 8:52 AM, Ramana Kumar <[email protected]>
wrote:
> ``S CROSS S`` is a set of pairs. Although ``S`` is usually parsed as a
> constant, so you might want to use a different letter, or use Parse.hide"S".
>
> Do you want the set of first components of the pairs? That would be
> ``IMAGE FST (S CROSS S)``, and should be equal to ``S``.
>
> On 5 February 2016 at 14:42, Nadeem Iqbal <[email protected]>
> wrote:
>
>> Hi,
>>
>> Dear All,
>>
>> I am working in HOL4. I want to extract the domain of the set of binary
>> relations.
>> For example, when I tried this goal,
>>
>> g `! S. (FST (S CROSS S)) SUBSET (FST (S CROSS S))`;
>>
>> It could not run. Can any one guide me?
>>
>> Regards,
>>
>> Nadeem Iqbal
>> HoD School of Computing and Information Sciences,
>> Imperial College of Business Studies,
>> Lahore, Pakistan.
>>
>>
>>
>> ------------------------------------------------------------------------------
>> 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
