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

自然数の演算(3)

問題点

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

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

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

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

$\begin{matrix} ( (a + b) * c + (a + b)) + d = (a + b) * (c') + d \\ (a * b + a) + (c * d + c) = a * (b') + c * (d') \end{matrix} \\ \implies (a + b) * (c') + ( (d * e + d) + (f * g + f)) \\ = ( (a + b) * c + (a + b)) + (d * (e') + f * (g'))$

(1) ここで $c = e = g$ とすると
$(a + b) * (c') + ( (d * c + d) + (f * c + f)) \\ = ( (a + b) * c + (a + b)) + (d * (c') + f * (c'))$

(2) ここで $'$ を ${}^\wedge$ に変換すると
$(a + b) * (c^\wedge) + ( (d * c + d) + (f * c + f)) \\ = ( (a + b) * c + (a + b)) + (d * (c^\wedge) + f * (c^\wedge))$

$c=0$ を代入すると
$(a + b) * (0^\wedge) + ( (d * 0 + d) + (f * 0 + f)) \\ = ( (a + b) * 0 + (a + b)) + (d * (0^\wedge) + f * (0^\wedge))$
$(a + b) * (0^\wedge) + ( (0 + d) + (0 + f)) \\ = ( 0 + (a + b)) + (d * (0^\wedge) + f * (0^\wedge))$
$(a + b) * (0^\wedge) + ( d + f ) = ( a + b ) + (d * (0^\wedge) + f * (0^\wedge))$

(3) ここで $0^\wedge$ を $c$ に変換すると
$(a + b) * c + ( d + f ) = ( a + b ) + (d * c + f * c)$

(4) ここで $a = d$ 、 $b = f$ とすると
$(a + b) * c + ( a + b ) = ( a + b ) + (a * c + b * c)$
$(a + b) * c = a * c + b * c$

現状では (1)、(2)、(3)、(4) ができません。

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

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

上記の議論と同様に
$(a + b) * (c') = (a + b) * c + (a + b)$
$(a * c + a) + (b * c + b) = a * (c') + b * (c')$
から
$(a + b) * (c') + ( (a * c + a) + (b * c + b) ) \\ = ( (a + b) * c + (a + b) ) + ( a * (c') + b * (c') )$
$'$ を ${}^\wedge$ に変換すると
$(a + b) * (c^\wedge) + ( (a * c + a) + (b * c + b) ) \\ = ( (a + b) * c + (a + b) ) + ( a * (c^\wedge) + b * (c^\wedge) )$
$c=0$ を代入すると
$(a + b) * (0^\wedge) + ( (a * 0 + a) + (b * 0 + b) ) \\ = ( (a + b) * 0 + (a + b) ) + ( a * (0^\wedge) + b * (0^\wedge) )$
$(a + b) * (0^\wedge) + (a + b) = (a + b) + ( a * (0^\wedge) + b * (0^\wedge) )$
$(a + b) * (0^\wedge) = a * (0^\wedge) + b * (0^\wedge)$
$0^\wedge$ を $c$ に変換すると
$(a + b) * c = a * c + b * c$

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

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

$(a + b) * c = a * c + b * c$ が成り立っているとすると
$a * (b * c + b) = a * (b * (c'))$ から $a * (b * c) + (a * b) = a * (b * (c'))$

$( (a * b) * c + a * b) + a * (b * (c')) = (a * b) * (c') + (a * (b * c) + (a * b))$
ここで $'$ を ${}^\wedge$ に変換すると
$( (a * b) * c + a * b) + a * (b * (c^\wedge)) = (a * b) * (c^\wedge) + (a * (b * c) + (a * b))$
$c=0$ を代入すると
$( (a * b) * 0 + a * b) + a * (b * (0^\wedge)) = (a * b) * (0^\wedge) + (a * (b * 0) + (a * b))$
ここで $0^\wedge$ を $c$ に変換すると
$( (a * b) * 0 + a * b) + a * (b * c) = (a * b) * c + (a * (b * 0) + (a * b))$
$a * b + a * (b * c) = (a * b) * c + a * b$
$a * (b * c) = (a * b) * c$

$0 * a = 0$

( $0$ のとき)定義より $0 * 0 = 0$ 。 $0 * a = 0$ と仮定すると、 $0 * a' = 0 * 0 + 0 = 0$ 。よって帰納法により成り立ちます。

以下のような議論ができる必要があります。

$0 * a' = 0 * a + 0 = 0 * a$ から $'$ を ${}^\wedge$ に変換すると $0 * a^\wedge = 0 * a$ となり、 $a = 0$ を代入すると $0 * 0^\wedge = 0 * 0 = 0$ 。 $0^\wedge$ を $a$ に変換すると $0 * a = 0$ 。

$a * b = b * a$

( $b=0$ のとき)定義より $a * 0 = 0$ 。上記の結果より $0 * a = 0$ 。よって $a * 0 = 0 * a$ 。 $a * b = b * a$ と仮定すると、定義より $a * b' = a * b + a$ 。 $b' * a = (b + 1) * a = b * a + 1 * a = b * a + a = a * b + a$ 。よって帰納法により成り立ちます。

以下のような議論ができる必要があります。

$a * b' = a * b + a$ 、 $b' * a = b * a + a$ より $a * b' + b * a = b' * a + a * b$ 。
$'$ を ${}^\wedge$ に変換すると $a * b^\wedge + b * a = b^\wedge * a + a * b$ 。
$b = 0$ を代入すると $a * 0^\wedge + 0 * a = 0^\wedge * a + a * 0$ 、 $a * 0^\wedge = 0^\wedge * a$ 。
$0^\wedge$ を $b$ に変換すると $a * b = b * a$ 。