Confused about beta-reduction/shifting in untyped $\lambda$-calculus with de Bruijn terms
I figured it out - I was messing up the $\beta$-reduction in the first step by applying the substitution to $(\lambda. 0_1)_0$ instead of just $0_1$. This is the correct sequence of reduction steps:


$(\lambda. 0_1)_0\ (\lambda. 0_1)_0$
(by def. of $\beta$-reduction) $\rightarrow\ \uparrow^{-1}([0 \mapsto\ \uparrow^1((\lambda. 0_1)_0)] 0_1)$
(by def. of $\uparrow$) $\rightarrow\ \uparrow^{-1}([0 \mapsto (\lambda. 0_2)_1] 0_1)$
(by def. 1 of substitution) $\rightarrow\ \uparrow^{-1}((\lambda. 0_2)_1)$
(by def. of $\uparrow$) $\rightarrow\ (\lambda. 0_1)_0$