I'm not sure what "works quite well". To clarify things, if
Action(t) == t = y
Capture(var, Action(_)) == \E t \in {var} : t = var /\ Action(t)
Then
Capture(x, Action)' = (\E t \in {x} : t = x /\ (t=y))'
= (\E t \in {x'} : t' = x' /\ (t'=y'))
= (\E t \in {x'} : t = x' /\ (t=y'))
The last equality holds because t' = t, since \E t introduces t as a constant.
Leslie
On Thursday, January 7, 2016 at 2:42:51 PM UTC-8, Ron Pressler wrote:
BTW, your suggestion of `\E t : t = x` works quite well. At first I defined:Capture(var, Action(_)) == \E t \in S : t = var /\ Action(t) \* S is a constant set known to contain the variable var
and it does the capture/lowering I want.
Then I tried:
Capture(var, Action(_)) == \E t \in {var} : t = var /\ Action(t)
and that works too! I guess that's because the quantification happens outside the priming, and so t is a fresh, bound symbol rather than an _expression_ involving a variable.
Thanks again!