Peterson's Algorithm total correctness proof in IPCL - A. A. Zhygallo (Problems in programming, 2016)