Impossibility of gathering, a certification
We expand the Pactole Coq framework to use actual real numbers as robot positions. We certify correctness of Suzuki and Yamashita's impossibility result for two robots. We certify an even number of robots cannot gather if we allow initial multiplicity.
analysis of algorithms automatic theorem proving computational geometry distributed computing theory of computation