日記 2021/04/02 - ボケ日記

割り算の一意可能性

$\displaystyle{ \forall p \in \{p \in N | 2 \leq p \}; \forall a, b \in N; (b \neq 0 \rightarrow \exists ! x, y \in N; (a = b \times x + y \land y < b)) }$

を示した。
これによって、 $p$ -進法表記の一意可能性が示せて、 $p$ -進法表記ができるようになった。
例題に10進法での加減乗除の計算方法を考え、それが正しいことを示せとあったが、これが終わってない。
加算は繰り上がりを帰納的な関数で表現すればよく、減算は加算を使って求められる。乗算は累積帰納的な関数を使えばよく、除算は乗算から求められる。
あとはやるだけだけどやってない。