Remove incomplete leftover.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
heidihoward · Sep 3, 2024 · b7b4f4e · b7b4f4e
1 parent f3f979e
commit b7b4f4e
Showing 1 changed file with 0 additions and 3 deletions.
diff --git 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 |-> {},