Axiomatization conjecture for Büchi arithmetic $_2$

Let $_2$ denote the first-order theory of Büchi arithmetic with the function $V_2$, and let axioms $(1)$–$(17)$ be the axioms and schemata described above, including the recursive definition of $V_2$ and the additional conditions on powers of $2$.

Axiomatization conjecture. The axioms and schemata $(1)$–$(17)$ axiomatize $_2$.

The preceding discussion explains that axioms $(1)$–$(14)$ alone are insufficient: the additional conditions $(15)$–$(17)$ all hold in the standard model but are not consequences of those earlier axioms. The conjecture asserts that adding them gives a complete axiomatization of Büchi arithmetic with base $2$.