The formal proof just takes the shortest exchange that leads to the correct result and drops the last message. Since the sender doesn't know it failed, the resu

The formal proof just takes the shortest exchange that leads to the correct result and drops the last message. Since the sender doesn't know it failed, the result must be incorrect. That's the gist of it, there are some technicalities of specifying what "correct" means.