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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 20 Aug 2019 08:50:14 +0200*References*: <dd8d25b8-90ac-4fb2-b919-4fcf6325f6c3@googlegroups.com> <8ea5175a-a86e-4565-8ebc-da9e5eb7d97c@googlegroups.com> <CAHeFUE83VQFednaFqZBB3uk5oA3wD5WeSbgmYwf8Q8i8u9G7Bg@mail.gmail.com> <CAHeFUE-i97gYL22W+zZOOYyS+uMr-8i9pq_F=p+wcdZPvgvvPA@mail.gmail.com>

Section 6.2 states:
Thus, Phase2b(a)!(X) represents /\ X.type = "2a" /\ X.bal >= maxBal[a] /\ Send([type |-> "2b", bal |-> X.bal, val |-> X.val, acc |-> a]) /\ maxVBal' = [maxVBal EXCEPT ![a] = X.bal] /\ maxBal' = [maxBal EXCEPT ![a] = X.bal] /\ maxVal' = [maxVal EXCEPT ![a] = X.val] The step in the proof that you originally refer to
introduces the name `m' for the message for which action Phase2b(a) is performed, adds the assumption `m \in msgs' to the set of hypotheses that are actively used, and by referring to <2>1 inside the proof one invokes the above conjunction (with X replaced by m) without having to retype it. Hope this helps, Stephan
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A8DAE3C3-661B-4F08-BF9B-7551E4ED2D09%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Usage of the ! operator***From:*Saswata Paul

**References**:**[tlaplus] Usage of the ! operator***From:*Saswata Paul

**[tlaplus] Re: Usage of the ! operator***From:*Leslie Lamport

**Re: [tlaplus] Usage of the ! operator***From:*Saswata Paul

**Re: [tlaplus] Usage of the ! operator***From:*Saswata Paul

- Prev by Date:
**Re: [tlaplus] Any instructions on when and how to explicitly specify backend provers in TLAPS proofs?** - Next by Date:
**Re: [tlaplus] TLA+, Event B comparison** - Previous by thread:
**Re: [tlaplus] Usage of the ! operator** - Next by thread:
**Re: [tlaplus] Usage of the ! operator** - Index(es):