Closed tobiasgrosser closed 1 month ago
Proofing theorem bb {a b : BitVec w} { n : Nat} :(a >>> n <<< n) &&& (b <<< n) = (a &&& b <<< n) should be sufficient to close bv_InstCombineShift__476.
theorem bb {a b : BitVec w} { n : Nat} :(a >>> n <<< n) &&& (b <<< n) = (a &&& b <<< n)
bv_InstCombineShift__476
Proofing
theorem bb {a b : BitVec w} { n : Nat} :(a >>> n <<< n) &&& (b <<< n) = (a &&& b <<< n)should be sufficient to closebv_InstCombineShift__476.