unfold bitwise
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
⊢ getBit
      (if m = 0 then if f false true = true then n else 0
      else
        if n = 0 then if f true false = true then m else 0
        else
          let n' := m / 2;
          let m' := n / 2;
          let b₁ := m % 2 = 1;
          let b₂ := n % 2 = 1;
          let r := bitwise f n' m';
          if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r)
      zero =
    f (getBit m zero) (getBit n zero)