Q calculates numerals and finite bounded cases

Use the seven Q axioms F1. Externally inducting on $b$ gives Q proofs of $\bar{a}+\bar{b}=\overline{a+b}$ and $\bar{a}\cdot \bar{b}=\overline{ab}$, by substituting the previous equality into the respective recursion axiom. Structural induction reduces each closed term to a numeral. For distinct numerals cancel their common successor prefix using injectivity; a remaining successor cannot equal zero. Hence Q proves the correct equality or inequality between any two closed terms.

We prove the bounded-case scheme externally on $n$. If $z+x=0$ and $x\mathrm{\ne }0$, predecessor gives $x=Sy$, so $z+x=S(z+y)\mathrm{\ne }0$, a contradiction. Hence $x\le 0\to x=0$. For the next bound, either $x=0$ or $x=Sy$. In the second case $z+x=S\bar{n}$ implies $z+y=\bar{n}$ by injectivity, hence $y\le \bar{n}$ and the earlier finite case scheme makes $x$ one of $\bar{1},\dots ,\overline{n+1}$. This is a finite derivation for each n.

For every fixed $k$, external induction proves $z+\bar{k}=S^{k}z$ and $Sz+\bar{k}=z+\overline{k+1}$. Repeatedly applying the predecessor axiom $n+1$ times gives the finite disjunction: $x=0$, ..., $x=\bar{n}$, or $x=S^{n+1}z$ for some $z$. In a numeral case, a numeral left-addend witness proves $x\le \bar{n}$ by step 1.1. In the last case, $z+\overline{n+1}=x$ proves $\overline{n+1}\le x$. This gives the second scheme without internal induction. The same calculation shows $\overline{n+1}\le x\to \bar{n}\le x$ by replacing z with Sz.

A numeral instance of $\le$ is true exactly when its first numeral is among those allowed by step 2.1. If it is, a numeral witness proves it; otherwise the finite disjunction and the unequal-numeral proofs refute it. Thus closed order atoms are decided as well. For a closed bounded quantifier first reduce its bounding term to $\bar{n}$, then use step 2.1 to replace the bounded variable by the finite list of possible numerals. Induction on the formula gives a proof or a refutation for each substituted matrix. Existential introduction proves a true existential; the finite case disjunction refutes a false one. Negation handles universal quantifiers; Boolean truth tables combine the remaining cases. The zero bound yields either a singleton test for <= or no candidates for <.