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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
