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

*From*: chris...@xxxxxxxxx*Date*: Thu, 6 Nov 2014 10:17:27 -0800 (PST)*References*: <27780607-9e0a-4101-92fa-ccbb15043611@googlegroups.com> <CAAWQ4M6-JOS8MEGzULKSDbiDPvfXEvWJ0304JHn9paEg5zueGg@mail.gmail.com>

Hi, yes this is the cause of my problems.

I appreciate your response and Stephan's. My proof now works.

One thing I don't fully understand is after I reduced Init to x = R * N, the proof was still polluted somewhere by the use of ^ instead of /\ even though it should have been left unexpanded as Init == XNat ^ XChooseRN and not affected proof involving x. But anyway a relatively straightforward mistake. Now I can go on to make more interesting mistakes, thanks.

I appreciate your response and Stephan's. My proof now works.

One thing I don't fully understand is after I reduced Init to x = R * N, the proof was still polluted somewhere by the use of ^ instead of /\ even though it should have been left unexpanded as Init == XNat ^ XChooseRN and not affected proof involving x. But anyway a relatively straightforward mistake. Now I can go on to make more interesting mistakes, thanks.

**References**:**Proofs of integer properties***From:*chris . . .

**Re: [tlaplus] Proofs of integer properties***From:*TLA Plus

- Prev by Date:
**Re: [tlaplus] Proofs of integer properties** - Next by Date:
**Re: Proofs of integer properties** - Previous by thread:
**Re: [tlaplus] Proofs of integer properties** - Next by thread:
**Re: Proofs of integer properties** - Index(es):