Theorem. add-lsb [blog/fenwick/thm/thm6]
Theorem. add-lsb [blog/fenwick/thm/thm6]
对于所有 $x : \text{Bits}$, $\text{add}(x, \text{lsb}(x)) = \text{atLSB}(\text{inc}, x)$ 且 $\text{subtract}(x, \text{lsb}(x)) = \text{atLSB}(\text{dec}, x)$。
(注:代码中 $\text{atLSB}$ 的定义为 at_lsb
)
证明 对 $x$ 进行简单的归纳即可。