# Re: [Hol-info] How to reduce these lambda equations to F?

```Thanks!    Actually I was ever taught (by Thomas) to use FUN_EQ_THM to convert
relation equations (R = R’) into provable forms (!x y. R x y = R’ x y), but
when I was facing lambda functions I didn’t realize they’re essentially the
same thing.   (Using PAT_X_ASSUM I can precisely target on any single
assumptions, thus other assumptions won’t be affected)```
```
And I found that, once I got ``!x. x = prefix (label l) x``, actually the
`distinct` theorems generated by Datatype will directly lead it to False, no
need to call the “size” theorems and use arithmetic stuff, although the latter
idea also works.

—Chun

> Il giorno 07 ago 2017, alle ore 01:33, michael.norr...@data61.csiro.au ha
> scritto:
>
> I would use
>
>   fs[FUN_EQ_THM]
>
> to expand the assumptions to
>
>   !x. x = prefix (label l) x
>
> and
>
>   !x. x = p
>
> respectively.
>
> Of course, this is a blunt weapon, so you may not wish to use it if other
> assumptions are disrupted too much.
>
> Michael
>
> On 5/8/17, 04:25, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
>
>    Hi,
>
>    This is the first time I met the following goal, in which one of the
> assumptions should be able to reduce to F (then the goal is resolved):
>
>    R (λt. t)
>    ------------------------------------
>      4.  (λt. t) = (λt. prefix (label l) t)
>
>    The lambda function has the type of ``CCS -> CCS``, which CCS is my
> datatype defined by HOL’s Define command.  “prefix” is an constructor of CCS
> datatype.    I *know* the equation doesn’t hold, because the whatever input
> arguments, the resulting CCS on both side must have different “size”, simply
> because one is the sub-expression of the other.   But how can I actually
> reduce it to F?
>
>    The other case is a little different:
>
>    R (λt. t)
>    ------------------------------------
>      4.  (λt. t) = (λt. p)
>
>    The assumption "(λt. t) = (λt. p)” hold for only one case: when input of
> lambda function is exactly “p”.  For all other cases the left side doesn’t
> equal to the right side.  But from the view of two functions, they’re
> obviously not identical. But how can I actually reduce it to F?
>
>    Regards,
>
>    Chun Tian
>
>
>
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

```

signature.asc
Description: Message signed with OpenPGP using GPGMail

```------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
```_______________________________________________