1 Stern の数列

\({\rm fusc}\) は次の漸化式を満たす関数として仮定します（存在は示しません）。\(0, 1, 1, 2, 1, 3, 2, 3, 1, 4, \ldots\) と続く数列です。
word(s,s)F … \(\mathrm{fusc}\)
fusc𝕄 … \(\begin{cases} \mathrm{fusc} ( 0 ) = 0 \\ \mathrm{fusc} ( 1 ) = 1 \\ n \in \mathbb{M} \Longrightarrow \mathrm{fusc} ( 2 \cdot n ) = \mathrm{fusc} ( n ) \\ n \in \mathbb{M} \Longrightarrow \mathrm{fusc} ( 2 \cdot n + 1 ) = \mathrm{fusc} ( n ) + \mathrm{fusc} ( n \textit{+1} ) \end{cases}\)
Lfusc … \(n \in \mathbb{M} \Longrightarrow \mathrm{fusc} ( n ) \in \mathbb{M} , ( n \neq 0 \Longrightarrow \mathrm{fusc} ( n ) \neq 0 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，fusc𝕄

Calkin–Wilf：どの \(a, b\)（\(b \neq 0\)）も、ある \(n\) と \(g\) で \(a = g\,{\rm fusc}(n)\)、\(b = g\,{\rm fusc}(n+1)\) と書ける。
\(a+b\) についての強い帰納法：\(a = 0\) なら \(n = 0\)。\(b \le a\) なら \((a-b, b)\) から \(2n+1\) へ、\(a < b\) なら \((a, b-a)\) から \(2n\) へ（互除法を逆にたどる）。
LCW … \(a , b \in \mathbb{M} , b \neq 0 \Longrightarrow \exists n \in \mathbb{M} . \exists g \in \mathbb{M} . a = g \cdot \mathrm{fusc} ( n ) , b = g \cdot \mathrm{fusc} ( n \textit{+1} )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，fusc𝕄