使用Coq交互式定理证明器对FLP不可能定理进行形式化
模型是仿照。
其他建设性证明： : 10.1.1.221.7907& rep1&type= ， : ，但这是第一个公开源代码！ lemma3的证明也不同于以前的所有证明。
纸快来了！ 希望将其发表在同行评审的期刊上。
##模型与公理
消息完全被跳过了（因此仅出于更好的理解而需要它们，而为了证明起见，我们只能讨论系统的状态转换）。
Process是原始文件中的自动机。 就我们的目的而言，枚举具有一些自然数的状态，并在数字中也编码过程标识符就足够了，因此存在双向注入式映射（process_id，state）<-> nat。
Definition Process := nat.
那么配置只是进程列表：
Definition Configuration := list Process.
事件也用自然数枚举，具有
