From 2059f291a9289869978692c1b083e5193c2a09f1 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 7 Oct 2024 18:44:18 +0100 Subject: [PATCH] fixed name, indentation and generalized thm --- Proofs/SHA512/SHA512_block_armv8_rules.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Proofs/SHA512/SHA512_block_armv8_rules.lean b/Proofs/SHA512/SHA512_block_armv8_rules.lean index f30314ab..d7c79a93 100644 --- a/Proofs/SHA512/SHA512_block_armv8_rules.lean +++ b/Proofs/SHA512/SHA512_block_armv8_rules.lean @@ -138,8 +138,8 @@ theorem truncate_of_concat_is_lsb_64 (x y : BitVec 64) : BitVec.zeroExtend 64 (x ++ y) = y := by bv_check "lrat_files/Sha512_block_armv8_rules.lean-truncate_of_concat_is_lsb_64-106-2.lrat" -theorem zeroExtend_append_eq (w : Nat) (x y : BitVec w) : - BitVec.zeroExtend w (x ++ y) = y := by +theorem zeroExtend_append_eq_right {w v : Nat} {x : BitVec w} {y : BitVec v} : + BitVec.zeroExtend v (x ++ y) = y := by ext simp only [truncate_append, Nat.le_refl, ↓reduceDIte, zeroExtend_eq]