``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
