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

*From*: sglaser@xxxxxxxxxxx*Date*: Thu, 18 Apr 2019 15:11:55 -0700*Cc*: Jam <wawrzynchonewicz@xxxxxxxxx>, Leslie Lamport <tlaplus.ll@xxxxxxxxx>*References*: <ec8df666-5129-4c3d-a2f5-c7ccb8b0c2da@googlegroups.com> <d9af7387-c0b7-4799-aa4f-94702a176c82@googlegroups.com>

I think you want something like:

**RECURSIVE** union_set2(_, _)

union_set2(x, y) ==

**IF** x = {}

**THEN** y

**ELSE** **CHOOSE** a \in x :

**IF** \E b \in y : **UNION** a = **UNION** b

**THEN** union_set2(x \ a, y)

**ELSE** union_set2(x \ a, y \cup {a})

union_set(x) == union_set2(x, {})

On Apr 18, 2019, 3:01 PM -0700, Leslie Lamport <tlaplus.ll@xxxxxxxxx>, wrote:

-- --In constructing the second set, you have removed from s the element {{3}, {2,4}} the union of the elements of that set is the set {2,3,4}. That set is not in s, since s has no 3-element sets, so it does not satisfy your condition for an element to be removed from s. Therefore, what you have written makes no sense to me.You seem to want to define an operator Op such that Op(s) equals the second set. By talking about "removing elements", I presume you meant that Op(s) should be a subset of s. Hence, I believe that the definition you want should be expressible asOp(t) == CHOOSE u \in SUBSET t : P(t, u)for some formula P(t, u). This definition of Op may not satisfy you because to evaluate it, TLC must compute all elements of SUBSET t and evaluate P(t,u) for all the elements u of SUBSET t until it finds one that evaluates to TRUE. However, it will at least tell people what operator Op you want.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:

**References**:**[tlaplus] Removing "equivalents" from a set***From:*Jam

**[tlaplus] Re: Removing "equivalents" from a set***From:*Leslie Lamport

- Prev by Date:
**[tlaplus] Re: Removing "equivalents" from a set** - Next by Date:
**[tlaplus] Re: Removing "equivalents" from a set** - Previous by thread:
**[tlaplus] Re: Removing "equivalents" from a set** - Next by thread:
**Re: [tlaplus] Re: Removing "equivalents" from a set** - Index(es):