[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 7 Jan 2016 14:56:17 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com> <20d67976-47a3-440d-942e-51f3b035554e@googlegroups.com> <393668fc-f7ac-49ad-9f04-598c39d1a771@googlegroups.com> <c6c1cac0-c5d4-46c0-b236-31b9ba2d7d0d@googlegroups.com>

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!

**Follow-Ups**:**Re: Tagged formulas***From:*Ron Pressler

**References**:**Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Leslie Lamport

**Re: Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Ron Pressler

- Prev by Date:
**Re: Tagged formulas** - Next by Date:
**Re: TLA+ Toolbox 1.5.2 release** - Previous by thread:
**Re: Tagged formulas** - Next by thread:
**Re: Tagged formulas** - Index(es):