From b7b4f4ec21b96e82e79be4f23bfaf15fad0b3fb5 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 3 Sep 2024 09:01:50 -0700 Subject: [PATCH] Remove incomplete leftover. Signed-off-by: Markus Alexander Kuppe --- APApbft.tla | 3 --- 1 file changed, 3 deletions(-) diff --git a/APApbft.tla b/APApbft.tla index 3dd092e..70a8155 100644 --- a/APApbft.tla +++ b/APApbft.tla @@ -106,9 +106,6 @@ MsgsConstraint == /\ pp.n \in SeqNums /\ pp.d \in RequestDigests -\* THEOREM msgs \in Messages => MsgsConstraint -\* BY DEF Messages, MsgsConstraint, NewViewMessages, PrepareProof, PrepareMessages, ViewChangeMessages, CheckpointMessages, PrePrepareMessages, CommitMessages, ReplyMessages, RequestMessages - MlogsConstraintEmpty == /\ mlogs = [r \in R |-> [ request |-> {},