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 i
Hi Chun,
via a subgoal, you can introduce an assumption for a concrete argument.
This should be what you need. I'm thinking of something like
First show that a CCS q exists with "q <> p"
`?q. q <> p` by ...
Then use this new q as an argument)
`(\t. t) q = (\t. p) q` by PROVE_TAC[]
Now you are
2ND CALL FOR PAPERS
The 7th ACM SIGPLAN International Conference
on Certified Programs and Proofs (CPP 2018)
co-located with POPL 2018
in cooperation with ACM SIGLOG
http://conf.researchr.org/track/CPP-2018/CPP-2018
8-9 January, 2018, Los
Hi Thomas,
Thanks! Now I got your points:
1. ``(λt. t) = (λt. p)`` cannot reduce to F unless the underlying type
has at least two distinct values (for datatypes with at least two constructors,
it’s easily provable by cases analysis, I think).
2. To prove two lambda-functions, sa
