From e124d4198b72221eda94835e103c0d8cb1b59617 Mon Sep 17 00:00:00 2001
From: yezhengmao <yezhengmaolove@gmail.com>
Date: Mon, 8 May 2023 17:03:07 +0800
Subject: [PATCH] =?UTF-8?q?paxos=E8=8D=89=E6=A1=882?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 content/paxos.md | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/content/paxos.md b/content/paxos.md
index 0455d5b..9d19846 100644
--- a/content/paxos.md
+++ b/content/paxos.md
@@ -1,6 +1,6 @@
 +++
 title="Paxos算法详解"
-date="2023-05-02"
+date="2023-05-08"
 +++
 
 ## 前言
@@ -84,7 +84,12 @@ date="2023-05-02"
 > 若某轮提议达成一致，成为已决决议，则任意提议号大于该提议的决议都与其相同  
   
 证明（反证法）：  
-1. 
+1. 假设在已决决议提议之后存在提议的决议与已决决议不同，取这些提议中提议号最小的提议，记为提议甲。
+2. 提议甲中的法定节点集一定与已决决议投票节点集有交集（约束Ⅱ保证法定节点集之间有交集，已决决议保证法定节点集是投票节点集的子集）。
+3. 提议甲的法定节点集中一定存在节点，在大于等于已决决议提议号，小于提议甲提议号之间进行了投票（由2推出至少存在一个节点，即在已决决议提议中进行投票的节点）。取这些投票所对应的提议号距提议甲最近的一次决议，记为决议乙。
+4. 由约束Ⅲ的存在，决议甲的法定节点集在决议乙中进行了投票，则决议甲等于决议乙，两则与已决决议不等。
+5. 违法决议甲是不同于已决决议中拥有最小提议号的假设。
+
 ## 参考
 * Leslie, Lamport. "The part-time parliament." ACM Trans. on Computer Systems 16 (1998): 133-169.
 * Lamport, Leslie. "Paxos made simple." ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) (2001): 51-58.