ビジュアルプログラミング(8) - エレファント・ビジュアライザー調査記録

自然数の演算(2)

$a + b = b + a$ を示します。

他にも

$(a * b) * c = a * (b * c)$
$a * b = b * a$
$a * (b + c) = a * b + a * c$
$(a + b) * c = a * c + b * c$

が成り立つのですが、これを示すには機能が不足しているかもしれません。

(2-1) $(a + b)^\wedge = a + b^\wedge$

$\begin{matrix} a + b' = (a + b)' \\ a + b = a + b \end{matrix} \implies (a + b)' = a + b' \\ \implies (a + b)^\wedge = a + b^\wedge$

(2-2) $a + 0^\wedge = (a + 0)^\wedge$

$\begin{matrix} (a + b)^\wedge = a + b^\wedge \\ 0 = 0 \end{matrix} \implies a + 0^\wedge = (a + 0)^\wedge$

(2-3) $a + 0^\wedge = a^\wedge$

$\begin{matrix} a + 0^\wedge = (a + 0)^\wedge \\ a + 0 = a \end{matrix} \implies a + 0^\wedge = a^\wedge$

(2-4) $a = 0 + a$

$\begin{matrix} a + 0^\wedge = a^\wedge \\ 0 = 0 \end{matrix} \implies 0^\wedge = 0 + 0^\wedge \\ \implies a = 0 + a$

(2-5) $(a + 0)' = a + 0'$

$\begin{matrix} a + b' = (a + b)' \\ 0 = 0 \end{matrix} \implies (a + 0)' = a + 0'$

(2-6) $a + 0' = a'$

$\begin{matrix} (a + 0)' = a + 0' \\ a + 0 = a \end{matrix} \implies a + 0' = a'$

(2-7) $a'' = a' + 0'$

$\begin{matrix} a + 0' = a' \\ a' = a' \end{matrix} \implies a'' = a' + 0'$

(2-8) $a'' = a' + 1$

$\begin{matrix} a'' = a' + 0' \\ 1 = 0' \end{matrix} \implies a'' = a' + 1$

(2-9) $a' = a + 1$

$\begin{matrix} a + 0' = a' \\ 1 = 0' \end{matrix} \implies a' = a + 1$

(2-10) $a^\wedge + 1 = (a + 1)^\wedge$

$\begin{matrix} a'' = a' + 1 \\ a' = a + 1 \end{matrix} \implies a' + 1 = (a + 1)' \\ \implies a^\wedge + 1 = (a + 1)^\wedge$

(2-11) $(0 + 1)^\wedge = 0^\wedge + 1$

$\begin{matrix} a^\wedge + 1 = (a + 1)^\wedge \\ 0 = 0 \end{matrix} \implies (0 + 1)^\wedge = 0^\wedge + 1$

(2-12) $0^\wedge + 1 = 1^\wedge$

$\begin{matrix} (0 + 1)^\wedge = 0^\wedge + 1 \\ 0 + a = a \end{matrix} \implies 0^\wedge + 1 = 1^\wedge$

(2-13) $1 + a = a + 1$

$\begin{matrix} a + 0^\wedge = a^\wedge \\ 0^\wedge + 1 = 1^\wedge \end{matrix} \implies 1 + 0^\wedge = 0^\wedge + 1 \\ \implies 1 + a = a + 1$

(3-1) $(a + 1) + b = a + b'$

$\begin{matrix} a + (b + c) = (a + b) + c \\ a' = 1 + a \end{matrix} \implies (a + 1) + b = a + b'$

(3-2) $a + b^\wedge = a^\wedge + b$

$\begin{matrix} (a + 1) + b = a + b' \\ a' = a + 1 \end{matrix} \implies a + b' = a' + b \\ \implies a + b^\wedge = a^\wedge + b$

(3-3) $0 + a^\wedge = 0^\wedge + a$

$\begin{matrix} a + b^\wedge = a^\wedge + b \\ 0 = 0 \end{matrix} \implies 0 + a^\wedge = 0^\wedge + a$

(3-4) $a + b = b + a$

$\begin{matrix} 0 + a^\wedge = 0^\wedge + a \\ 0 + a = a \end{matrix} \implies 0^\wedge + a = a + 0^\wedge \\ \implies a + b = b + a$

【電子復刻版】bit 1988年04月号(通巻230号)

共立出版

Amazon

【電子復刻版】bit 1989年04月号(通巻242号)

共立出版

Amazon

新しいプログラミング・パラダイム

共立出版

Amazon

岩波講座ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論

作者:哲雄, 井田
岩波書店

Amazon