桁上げ伝播加算器の正しさ

定理 4.2（「コンピュータアーキテクチャとCPUの構造」§4）・ ✓公理まで証明済み

$n \ge 1$ とし、 $a_i, b_i \in \{0,1\}$ （ $0 \le i \le n-1$ ）と $c_0 \in \{0,1\}$ を任意に与えます。定義 4.1 の漸化式で $s_i, c_{i+1}$ （ $0 \le i \le n-1$ ）を定めるとき、整数の等式

\sum_{i=0}^{n-1} (a_i + b_i) 2^i + c_0 \;=\; c_n 2^n + \sum_{i=0}^{n-1} s_i 2^i

が成り立ちます。すなわち、 $a$ と $b$ を $n$ ビット 2 進数と見た和に $c_0$ を加えた値が、 $s$ を $n$ ビット 2 進数、 $c_n$ を最上位ビットとする $n+1$ ビットの数に一致します。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 0 件、定義なども含めて 1 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

証明で明示的に参照している定理は、まだありません。