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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Fri, 1 Jul 2016 01:33:45 -0700 (PDT)*References*: <3192db97-2a0c-4dc0-aac8-094340086a00@googlegroups.com> <d797b2a6-562d-4d2d-b515-3b7c601a7265@googlegroups.com> <1d27fd25-ac61-4660-ba06-2045cc5730af@googlegroups.com>

On Monday, June 23, 2014 at 3:59:50 PM UTC-7 I corrected my earlier email and wrote that the formula should be

<2>1. Inv /\
[][Next]_vars => []Inv

The formula you are looking for is the statement of LEMMA InductiveInvariance.

Leslie

On Friday, July 1, 2016 at 12:55:05 AM UTC-7, kaie wrote:

On Tuesday, June 24, 2014 at 5:44:33 AM UTC+10, Leslie Lamport wrote:[...]

The [] in the formula is spurious, and it should read

<2>1. Inv /\ [Next]_vars => Inv

Not sure why it's missing but I believe there ought to be prime at the very end:<2>1. Inv /\ [Next]_vars => Inv'

to make it interesting (and sufficiently strong for the following invariant proof).

Kai

**References**:**Parsing Error in Consensus.tla***From:*Christian Spann

**Re: Parsing Error in Consensus.tla***From:*Leslie Lamport

**Re: Parsing Error in Consensus.tla***From:*ka...@xxxxxxxxxxxxxxx

- Prev by Date:
**Re: Parsing Error in Consensus.tla** - Next by Date:
**Re: Formal methods for the application programmer** - Previous by thread:
**Re: Parsing Error in Consensus.tla** - Next by thread:
**Re: Parsing Error in Consensus.tla** - Index(es):