Re: [tlaplus] Proofs of integer properties

[chris...@xxxxxxxxx]

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.