I think the following proof found in a textbook is circular, since the proof for case n=n'0 assumes the case n=n'1 and vice versa. Am I missing something?
Proof that the semantic function N is a total function from binary strings into the integers:
Let N be defined thusly:
N(0) = 0; N(1) = 1; N(n0) = 2*N(n); N(n1) = 2*N(n) + 1;
For any n, there is one and only on integer mapped to by N(n), that is to say, N is a total function from binary strings into the integers. (A)
In the case n = 0, there is only one way to evaluate N(n) and that is with N(n) = N(0) = 0; hence (A) clearly holds. The proof for the case n = 1 is similar.
In the case n = n'0, we have only one way to evaluate N(n) and that is with N(n) = N(n'0) = 2*N(n'). Assuming by induction that (A) holds for N(n'), (A) clearly holds for N(n). The proof for n = n'1 is similar.
In the second part of the proof, for the case n = n'0 you have to assume for induction that * holds for n = n'1, and vice versa. Does this not lead to a circular dependency in the proof?