[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Proofs of integer properties
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.