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

*From*: Saswata Paul <paulsaswata1@xxxxxxxxx>*Date*: Thu, 4 Jul 2019 23:48:46 -0700 (PDT)

In page 6 of the paper "How to write a proof" (http://lamport.azurewebsites.net/pubs/lamport-how-to-write.pdf), It has been stated that "Part 3 of the statement of step <5>2 is numbered <5>.2.3.

-- By that syntax, in the proof of irrationality given in Figure 5. (page 7), <1>1.1 should refer to gcd(m,n)=1. However, later in the proof of m^2=2(n^2), it says PROOF: <1>1.1 implies (m/n)^2 = 2. How can gcd(m,n)=1 imply (m/n)^2 = 2 ?

I think I am missing something subtle about the numbering of steps here (or my sleepless mind is making a silly mistake elsewhere). Any help is appreciated.

PS: the content of page 7 is given below:

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d8d12743-bb95-4bec-b8f8-2986de55e930%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**Re: [tlaplus] How to refer to steps in TLAPS proofs? (new to TLA+)***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Using pcal.trans to write to different file** - Next by Date:
**Re: [tlaplus] How to refer to steps in TLAPS proofs? (new to TLA+)** - Previous by thread:
**Re: [tlaplus] Using pcal.trans to write to different file** - Next by thread:
**Re: [tlaplus] How to refer to steps in TLAPS proofs? (new to TLA+)** - Index(es):