I am doing some literature review regarding Buchi's problem. In particular, I am reading the relevant section in this survey paper by Mazur (Questions of Decidability and Undecidability in Number Theory) where it is stated that Buchi proved that there is no finite algorithm which decides the solubility of an arbitrary system of diagonal quadratic form equations
$$A \begin{bmatrix} x_1^2 \\ \vdots \\ x_n^2 \end{bmatrix} = \mathbf{b},$$
where $A \in M_{m \times n}(\mathbb{Z})$ and $\mathbf{b} \in \mathbb{Z}^m$ (Mazur called this Buchi's conjecture), provided that the following statement, known as Buchi's problem (see the Wikipedia page above), holds: there exists a positive integer $m_0$ such that if $x_1^2, \cdots, x_n^2$ is a sequence of squares satisfying
$$\displaystyle x_{j+2}^2 - 2 x_{j+1}^2 + x_j^2 = 2$$
for $j = 1, \cdots, n-2$, then either $n \leq m_0$ or there exists an integer $x$ such that $x_i = x + i$ for $i = 1, \cdots, n$.
Mazur had cited Buchi's collected works. Unfortunately, I cannot access this from where I am. Does anyone know of an original reference where Buchi proved this implication?
