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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Sat, 8 Nov 2014 06:54:22 -0800 (PST)*References*: <35991e2d-322c-456c-adb2-2cf4653a6e90@googlegroups.com> <f8c6c35f-2070-4f3a-bfe1-172ef6b5a1c5@googlegroups.com>

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

Yes I see: the semantics doesn't specify if S and << S >> are equal or not.

Thank you.

By the way Z3 accepts

ASSUME NEW S, NEW T \in S

PROVE << T >> \in [ 1..1 -> S ]

But not Isabelle nor CVC3.

--

FL

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

**Re: Missing theorem***From:*Leslie Lamport

- Prev by Date:
**Re: Missing theorem** - Next by Date:
**Re: Proofs of integer properties** - Previous by thread:
**Re: Missing theorem** - Next by thread:
**Temporal logic** - Index(es):