IMO 1976 — Đề thi chính thức Câu hỏi 6

Với mọi số nguyên dương $n$, $u_{n+1}=u_n(u_{n-1}^2-2)-u_1$, $u_0=2$ và $u_1=2\frac12$. Chứng minh rằng
$$3\log_2[u_n]=2^n-(-1)^n,$$
trong đó $[x]$ là phần nguyên của $x$.