From 27d49820432e1f32c37f7ea7c24dfb3605149e44 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Fri, 16 Jan 2026 16:17:17 +0100 Subject: [PATCH] fixed failing proof in byzpaxos/VoteProof Signed-off-by: Stephan Merz --- specifications/byzpaxos/VoteProof.tla | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/specifications/byzpaxos/VoteProof.tla b/specifications/byzpaxos/VoteProof.tla index c313093c..31baf8b6 100644 --- a/specifications/byzpaxos/VoteProof.tla +++ b/specifications/byzpaxos/VoteProof.tla @@ -1076,10 +1076,10 @@ THEOREM VT4 == TypeOK /\ VInv2 /\ VInv3 => <3>1. S # {} BY <1>6 <3>2. PICK c \in S : \A d \in S : c >= d - <4>2. IsFiniteSet(S) + <4>1. IsFiniteSet(S) BY FS_Interval, FS_Subset, 0 \in Int, b-1 \in Int, Zenon - <4>3. QED - BY <3>1, <4>2, FiniteSetHasMax + <4>. QED + BY <3>1, <4>1, S \in SUBSET Int, FiniteSetHasMax <3>3. /\ c \in 0 .. (b-1) /\ \E a \in Q : ~DidNotVoteIn(a,c) /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteIn(a, d)