Tobias Grosser

The theorem ```lean4 ∀ (a b : BitVec w), (b ||| a) - (b ^^^ a) = b &&& a ```` is very similar to https://github.com/opencompl/ssa/pull/304 and is a useful...

- [ ] Consider writing the broken proof within comments to make it easier to audit. - [ ] Consider writing a summary at the bottom of the file of...

Complete lemmas that relate shifting with `&&& allOnes`

2

There is a second identity in this space; we currently only have proven one: ```lean4 x >>> n n := by ``` Also, what about sshiftRight?

Deep kernel reduction detected after `simp`

1

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...