From d3ded59080b1a93a1556487593281603506f6d6b Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Thu, 27 Jun 2024 10:51:20 +0200 Subject: [PATCH] Update specs/quint/specs/proofs-in-blocs/proofs.qnt Co-authored-by: Daniel --- specs/quint/specs/proofs-in-blocs/proofs.qnt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/quint/specs/proofs-in-blocs/proofs.qnt b/specs/quint/specs/proofs-in-blocs/proofs.qnt index 37f723b7c..3a6530df6 100644 --- a/specs/quint/specs/proofs-in-blocs/proofs.qnt +++ b/specs/quint/specs/proofs-in-blocs/proofs.qnt @@ -82,7 +82,7 @@ var num_unproven_blocks: StrandInfo // If a block contains transactions then it is at the very beginning, or the block also contains a proof -def transactionNeedsProofInv = +def payloadImpliesProofInv = chain.last().txs implies chain.last().height < numStrands or chain.last().proof != None // The number of proofs of empty blocks in a recursive proof is bounded by maxMissingProofs