intro i
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
f : Bool → Bool → Bool
f_stable : f false false = false
m n i : Nat
⊢ getBit (bitwise f m n) i = f (getBit m i) (getBit n i)