Re: [tlaplus] [Dr. TLA+ Series] Paxos - Andrew Helwer (June 22nd, 10-11:30am PDT)

[fl <freder...@xxxxxxxxxxx>]

http://us2.metamath.org:88/downloads/inpreima2.pdf

Looking at it again several years later (I had written it in february 2012) I think it looks great.
I should read it again to know if it is true :)

What is poor is the trail of QEDs at the end. And it is also a bit too much detailed at one place:

it doesn't make sense for a human being.

Here is the source.

http://us2.metamath.org:88/downloads/inpreima2.tex
 
--
FL