Hi all,
let's say you have an event with two variables:
e = ANY a,b WHERE ...
and you want to refine to an event without those variables:
e = ANY c WHERE ...
then is not possible inside the witness of a to use the variable b (and vice versa).
error msg: "identifier b has not been declared"
It's very annoying if one want to really use the refinement.
I attach a archive as example.
see you soon
Logged In: YES
user_id=1371449
Originator: NO
This is not a bug. Mentioning b would be formally wrong. One-point rule! However, I agree that a generalisation of the witnesses as currently implemented would be very useful. We are working on this - the price will be an extra proof obligation to guarantee the existence of such generalised witnesses.