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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sat, 8 Nov 2014 06:46:47 -0800 (PST)*References*: <35991e2d-322c-456c-adb2-2cf4653a6e90@googlegroups.com>

But this one is unprovable (automatically I mean):

ASSUME NEW S, NEW T \in S

PROVE << T >> \in S

I hope it is unprovable manually as well, since it's false. See Section 16.1.9 in *Specifying Systems*.

Leslie

**Follow-Ups**:**Re: Missing theorem***From:*fl

**References**:**Missing theorem***From:*fl

- Prev by Date:
**Re: [tlaplus] Missing theorem** - Next by Date:
**Re: Missing theorem** - Previous by thread:
**Re: [tlaplus] Missing theorem** - Next by thread:
**Re: Missing theorem** - Index(es):