\left[\!| 0 |\!\right]_{bin} = 0_{\mathbb{N}} et \left[\!| 1 |\!\right]_{bin} = 1_{\mathbb{N}}
\left[\!| 0 |\!\right]_{nat} = \left[\!| 0 |\!\right]_{bin} = 0_{\mathbb{N}}
\left[\!| 1 |\!\right]_{nat} = \left[\!| 1 |\!\right]_{bin} = 1_{\mathbb{N}}
\left[\!| n 0 |\!\right]_{nat} = 2 \times \left[\!| n |\!\right]_{nat}+\left[\!| 0 |\!\right]_{bin} = 2 \times \left[\!| n |\!\right]_{nat}
\left[\!| n 1 |\!\right]_{nat} = 2 \times \left[\!| n |\!\right]_{nat}+\left[\!| 1 |\!\right]_{bin} = 2 \times \left[\!| n |\!\right]_{nat} + 1
avec '+' et 'x' les opérations habituelles de \mathbb{N}
Montrons que
à completer