For any $I\mathcal{POR}^{\lambda}$-formula $F$ and fresh variable $x$, we
define formulas $x\Vdash F$:

$\displaystyle x\Vdash F$ $\displaystyle:=F\vee T(x)\ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \text{(}F\text{ atomic)}$ $\displaystyle x\Vdash G\wedge H$
$\displaystyle:=x\Vdash G\wedge x\Vdash H$ $\displaystyle x\Vdash G\vee H$
$\displaystyle:=x\Vdash G\vee x\Vdash H$ $\displaystyle x\Vdash G\rightarrow
H$ $\displaystyle:=\forall y.(y\Vdash G\rightarrow x*y\Vdash H)$
$\displaystyle x\Vdash\exists y.G$ $\displaystyle:=\exists y.x\Vdash G$
$\displaystyle x\Vdash\forall y.G$ $\displaystyle:=\forall y.x\Vdash G.$

######  Lemma A.7.

If $F$ is provable in $I\mathcal{POR}^{\lambda}$ without using
$\mathbf{NP}$-induction, then $x\Vdash F$ is provable in
$I\mathcal{POR}^{\lambda}$.

###### Proof Sketch.

By induction on the structure of formulas of $I\mathcal{POR}^{\lambda}$ as in
[16]. ∎

######  Lemma A.8.

Let $F=\exists x\preceq\textsf{t}.G$, where $F$ is a $\Sigma^{b}_{0}$-formula.
Then, there is a term $\textsf{u}_{F}:s$ with $FV(\textsf{u}_{F})=FV(G)$ such
that $\vdash_{I\mathcal{POR}^{\lambda}}F\leftrightarrow T(\textsf{u}_{F})$.

###### Proof.

Since $G(x)$ is a $\Sigma^{b}_{0}$-formula, for all terms $\textsf{u}:s$,
$\vdash_{I\mathcal{POR}^{\lambda}}G(x)\leftrightarrow\textsf{u}_{x\preceq\textsf{t}\wedge
G}(x)=\mathsf{0}$, where $\textsf{t}_{x\preceq\textsf{t}\wedge G}$ has the
free variables of $t$ and $G$. Let $H(x)$ be a $\Sigma^{b}_{0}$-formula, it is
shown by induction on its structure that for any term $\textsf{v}:s$,
$\textsf{t}_{H(\textsf{v})}=\textsf{t}_{H}(\textsf{v})$. Then,
$\vdash_{I\mathcal{POR}^{\lambda}}\vdash F\leftrightarrow\exists
x.\textsf{t}_{x\preceq\textsf{u}\wedge G}(x)=\mathsf{0}\leftrightarrow\exists
x.T(\sharp(\lambda x.\textsf{t}_{x\preceq\textsf{t}\wedge G}(x)))$. So, we let
$\textsf{u}_{F}=\sharp(\lambda x.\textsf{t}_{x\preceq\textsf{u}\wedge G}(x))$.
∎

From which we deduce the following three properties: i.
$\vdash_{I\mathcal{POR}^{\lambda}}(x\Vdash F)\leftrightarrow(F\vee T(x))$; ii.
$\vdash_{I\mathcal{POR}^{\lambda}}(x\Vdash F)\leftrightarrow(F\rightarrow
T(x))$; iii. $\vdash_{I\mathcal{POR}^{\lambda}}(x\Vdash\neg\neg
F)\leftrightarrow(F\vee T(x))$, where $F$ is a $\Sigma^{b}_{1}$-formula.

######  Corollary 7 (Markov’s Principle).

If $F$ is a $\Sigma^{b}_{1}$-formula, then
$\vdash_{I\mathcal{POR}^{\lambda}}x\Vdash\neg\neg F\rightarrow F$.

To define the extension $(I\mathcal{POR}^{\lambda})^{*}$ of
$I\mathcal{POR}^{\lambda}$, we introduce PIND($F$) as:

$(F(\epsilon)\wedge(\forall x.(F(x)\rightarrow F(x\mathsf{0}))\wedge\forall
x.(F(x)\rightarrow F(x\mathsf{1}))))\rightarrow\forall x.F(x).$

Observe that if $F(x)$ is a formula of the form $\exists
y\preceq\textsf{t}.\textsf{u}=\textsf{v}$, then $z\Vdash$ PIND$(F)$ is of the
form PIND$(F(x)\vee T(z))$, which is _not_ an instance of the
$\mathbf{NP}$-induction schema.

######  Definition 21.

Let $(I\mathcal{POR}^{\lambda})^{*}$ be the theory extending
$\mathcal{POR}^{\lambda}$ with all instances of the induction schema
PIND$(F(x)\vee G)$, where $F(x)$ is of the form $\exists
y\preceq\textsf{t}.\textsf{u}=\textsf{v}$, and $G$ is an arbitrary formula
with $x\not\in FV(G)$.

The following Proposition relates derivability in $I\mathcal{POR}^{\lambda}$
and in $(I\mathcal{POR}^{\lambda})^{*}$.

######  Proposition 6.

For any $\Sigma^{b}_{1}$-formula $F$, if $\vdash_{I\mathcal{POR}^{\lambda}}F$,
then $\vdash_{(I\mathcal{POR}^{\lambda})^{*}}x\Vdash F$.

Finally, we extend realizability to $(I\mathcal{POR}^{\lambda})^{*}$ by
constructing a realizer fo PIND($F(x)\vee G$).

######  Lemma A.9.

Let $F(x):\exists y\preceq\textsf{t}.\textsf{u}=\mathsf{0}$ and $G$ be any
formula not containing free occurrences of $x$. Then, there exist terms
$\mathbf{t}$ such that $\vdash_{I\mathcal{POR}^{\lambda}}\mathbf{t}\
\circledR$ PIND$(F(x)\vee G)$.

So, by Theorem A.5, for any $\Sigma^{b}_{1}$-formula $F$ and formula $G$, with
$x\not\in FV(F)$, $\vdash_{I\mathcal{POR}^{\lambda}}$ PIND$(F(x)\vee G)$.

######  Corollary 8 ($\forall\mathbf{NP}$-Conservativity).

Let $F$ be a $\Sigma^{b}_{1}$-fromula. If
$\vdash_{I\mathcal{POR}^{\lambda}+EM}\forall x.\exists
y\preceq\textsf{t}.F(x,y)$, then $\vdash_{I\mathcal{POR}^{\lambda}}\forall
x.\exists y\preceq\textsf{t}.F(x,y)$.

We conclude the proof establishing the following Proposition 7.

######  Proposition 7.

Let $\forall x.\exists y\preceq\textsf{t}.F(x,y)$ be a closed term of
$I\mathcal{POR}^{\lambda}$+(Markov), where $F$ is a $\Sigma^{b}_{1}$-formula.
Then, there is a closed term of $\mathcal{POR}^{\lambda}$
$\textsf{t}:s\Rightarrow s$ such that
$\vdash_{I\mathcal{POR}^{\lambda}}\forall x.F(x,\textsf{t}x)$.

###### Proof.

If $\vdash_{I\mathcal{POR}^{\lambda}+(Markov)}\forall x.\exists y.F(x,y)$,
then by Proposition 2, also $\vdash_{I\mathcal{POR}^{\lambda}+(Markov)}\exists
y\preceq\textsf{t}.F(x,y)$. Moreover,
$\vdash_{(I\mathcal{POR}^{\lambda})^{*}}z\Vdash\exists
y\preceq\textsf{t}.F(x,y)$. Then, let us consider $G=\exists
y\preceq\textsf{t}.F(x,y)$. Taking $\textsf{v}=\textsf{u}_{G}$, by Lemma A.8,
we deduce $\vdash_{(I\mathcal{POR}^{\lambda})^{*}}G$ and, thus, by Lemma A.7
and A.9, we conclude that there exist $\mathbf{t},\mathbf{u}$ such that
$\vdash_{I\mathcal{POR}^{\lambda}}\mathbf{t},\mathbf{u}\ \circledR\ G$, which
implies $\vdash_{I\mathcal{POR}^{\lambda}}F(x,\mathbf{t}x)$ and so
$\vdash_{I\mathcal{POR}^{\lambda}}\forall x.(F(x),\mathbf{t}x)$. ∎

So, by Proposition 5, if $\vdash_{I\mathcal{POR}^{\lambda}+EM}\forall
x.\exists y\preceq\textsf{t}.F(x,y)$, being $F$ a closed
$\Sigma^{b}_{1}$-formula, then there is a closed term of $\mathcal{POR}$
$\textsf{t}:s\Rightarrow s$ such that
$\vdash_{I\mathcal{POR}^{\lambda}}\forall x.F(x,\textsf{t}x)$. Finally, we
conclude the desired Corollary 9.

######  Corollary 9.

Let ${R}\Sigma^{b}_{1}\text{-NIA}\vdash\forall x.\exists y\preceq t.F(x,y)$,
where $F$ is a $\Sigma^{b}_{1}$-formula with only $x,y$ free. For any
$f:\mathbb{S}\times\mathbb{O}\to\mathbb{S}$, if $\forall x.\exists y\preceq
t.F(x,y)$ represents $f$ so that:

  1. 1.

${R}\Sigma^{b}_{1}\text{-NIA}\vdash\forall x.\exists!y.F(x,y)$

  2. 2.

$\llbracket
F(\overline{\overline{\sigma_{1}}},\overline{\overline{\sigma_{2}}})\rrbracket=\\{\omega\
|\ f(\sigma_{1},\omega)=\sigma_{2}\\}$,

then $f\in\mathcal{POR}$.

##  Appendix B Proofs from Section 3

###  B.1 From $\mathbf{RFP}$ to $\mathcal{POR}$

The goal of this section is to establish a correspondence between
$\mathbf{RFP}$ and $\mathcal{POR}$. This passes through Proposition 8, which
assesses the equivalence between $\mathbf{RFP}$ and the intermediate class
$\mathbf{SFP}$ and Proposition 9, which concludes the proof showing the
equivalence between $\mathcal{POR}$ and $\mathbf{SFP}$. To establish
rigorously the results mentioned above, we fix some definitions. We start with
those of STMs and their configurations:

######  Definition 22 (Stream Turing Machine).

A _stream Turing machine_ is a quadruple
$M:=\langle{\mathcal{Q}},{q_{0}},{\Sigma},{\delta}\rangle$, where:

  * •

${\mathcal{Q}}$ is a finite set of states ranged over by ${q_{i}}$ and similar
meta-variables;

  * •

${q_{0}}\in{\mathcal{Q}}$ is an initial state;

  * •

${\Sigma}$ is a finite set of characters ranged over by ${c_{i}}$ _et simila_
;

  * •

${\delta}:{\hat{\Sigma}}\times{\mathcal{Q}}\times{{\hat{\Sigma}}}\times\mathbb{B}\longrightarrow{\hat{\Sigma}}\times{\mathcal{Q}}\times{\hat{\Sigma}}\times\\{{L},{R}\\}$
is a transition function describing the new configuration reached by the
machine.

$L$ and $R$ are two fixed and distinct symbols, e.g. ${0}$ and ${1}$,
${\hat{\Sigma}}={\Sigma}\cup\\{{\circledast}\\}$ and $\circledast$ represents
the _blank character_ , such that ${\circledast}\not\in{\Sigma}$. Without loss
of generality, in the following, we will use STMs with $\Sigma=\mathbb{B}$.

######  Definition 23 (Configuration of STM).

The _configuration of an STM_ is a quadruple
$\langle{\sigma},{q},{\tau},{\eta}\rangle$, where:

  * •

${\sigma}\in\\{{0},{1},\circledast\\}^{*}$ is the portion of the work tape on
the left of the head;

  * •

${q}\in\mathcal{Q}$ is the current state of the machine;

  * •

${\tau}\in\\{{0},{1},\circledast\\}^{*}$ is the portion of the work tape on
the right of the head;

  * •

${\eta}\in\mathbb{B}^{\mathbb{N}}$ is the portion of the oracle tape that has
not been read yet.

Thus, we give the definition of the family of reachability relations for STM
machines.

######  Definition 24 (Stream Machine Reachability Functions).

Given an STM $\mathscr{S}$ with transition function $\delta$, we denote with
$\vdash_{\delta}$ its standard step function and we call
$\\{\triangleright^{n}_{\mathscr{S}}\\}_{n}$ the smallest family of relations
for which:

$\displaystyle\langle\sigma,q,\tau,\eta\rangle$
$\displaystyle\triangleright^{0}_{M}\langle\sigma,q,\tau,\eta\rangle$
$\displaystyle\Big{(}\langle\sigma,q,\tau,\eta\rangle\triangleright^{n}_{M}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\eta^{\prime}\rangle\Big{)}\wedge\Big{(}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\eta^{\prime}\rangle$
$\displaystyle\vdash_{\delta}\langle\sigma^{\prime\prime},q^{\prime},\tau^{\prime\prime},\eta^{\prime\prime}\rangle\Big{)}\rightarrow\Big{(}\langle\sigma,q,\tau,\eta\rangle\triangleright^{n+1}_{M}\langle\sigma^{\prime\prime},q^{\prime}\tau^{\prime\prime},\eta^{\prime\prime}\rangle\Big{)}$

######  Definition 25 (STM Computation).

Given an STM,
$\mathscr{S}=\langle{\mathcal{Q}},{q_{0}},{\Sigma},{\delta}\rangle$,
$\eta:\mathbb{N}\longrightarrow\mathbb{B}$ and a function
$g:\mathbb{N}\longrightarrow\mathbb{B}$, we say that _$\mathscr{S}$ computes
$g$_, written $f_{\mathscr{S}}=g$ iff for every string $\sigma\in\mathbb{S}$,
and oracle tape ${\eta}\in\mathbb{B}^{\mathbb{N}}$, there are
$n\in\mathbb{N}$, ${\tau}\in\mathbb{S},{q^{\prime}}\in\mathcal{Q}$, and a
function ${\psi}:\mathbb{N}\longrightarrow\mathbb{B}$ such that:

$\langle{{\epsilon}},{q_{0}},{\sigma},{\eta}\rangle\
\triangleright^{n}_{\mathscr{S}}\
\langle{\gamma},{q^{\prime}},{\tau},{\psi}\rangle,$

and $\langle{\gamma},{q^{\prime}},{\tau},{\psi}\rangle$ is a final
configuration for $\mathscr{S}$ with $f_{\mathscr{S}}(\sigma,\eta)$ being the
longest suffix of ${\gamma}$ not including ${\circledast}$.

Similar notations are employed for all the families of Turing-like machines we
define in this paper. However, PTMs are an exception since they compute
distributions over $\mathbb{S}$ instead of functions
$\mathbb{S}\times\mathbb{O}\longrightarrow\mathbb{S}$.

######  Definition 26 (Probabilistic Turing Machines).

A Probabilistic Turing Machine (PTM) is a TM with two transition functions
$\delta_{0}$ and $\delta_{1}$ at each step of the computation, $\delta_{0}$ is
applied with probability $\frac{1}{2}$, otherwise $\delta_{1}$ is applied.
Given a PTM $\mathscr{M}$, a configuration $\langle\sigma,q,\tau\rangle$, we
define its semantics on configurations $\langle\sigma,q,\tau\rangle$ as the
following _sequence of random variables_ :

$\displaystyle\forall\eta\in\mathbb{B}^{\mathbb{N}}.X_{M,0}^{\langle\sigma,q,\tau\rangle}$
$\displaystyle:=\eta\mapsto\langle\sigma,q,\tau\rangle$
$\displaystyle\forall\eta\in\mathbb{B}^{\mathbb{N}}.X_{M,n+1}^{\langle\sigma,q,\tau\rangle}$
$\displaystyle:=\eta\mapsto\begin{cases}\delta_{b}(X_{M,n}^{\langle\sigma,q,\tau\rangle}(\eta))&\text{
if
}\eta(n)={b}\land\exists\langle\sigma^{\prime},q^{\prime}\tau^{\prime}\rangle.\delta_{b}(X_{M,n}^{\langle\sigma,q,\tau\rangle}(\eta))=\langle\sigma^{\prime},q^{\prime},\tau^{\prime}\rangle\\\
X_{M,n}^{\langle\sigma,q,\tau\rangle}(\eta)&\text{ if
}\eta(n)={b}\land\lnot\exists\langle\sigma^{\prime},q^{\prime}\tau^{\prime}\rangle.\delta_{b}(X_{M,n}^{\langle\sigma,q,\tau\rangle}(\eta))=\langle\sigma^{\prime},q^{\prime},\tau^{\prime}\rangle\\\
\end{cases}$

Intuitively, the variable $X_{\mathscr{M},n}^{\langle\sigma,q,\tau\rangle}$
maps each possible cylinder $\eta:\mathbb{N}\longrightarrow\mathbb{B}$ to the
configuration reached by the machine after exactly $n$ transitions where the
first transition step has employed $\delta_{\eta(0)}$, the second has employed
$\delta_{\eta(1)}$ and so on. We say that a PTM $\mathscr{M}$ computes
$Y_{\mathscr{M},\sigma}$ iff $\exists
t\in\mathbb{N}.\forall\sigma.X_{\mathscr{M},t}^{\langle\sigma,q_{0},\tau\rangle}$
is final. In such case, for every $\eta$, $Y_{\mathscr{M},\sigma}(\eta)$ is
the longest suffix of the leftmost element in
$X_{\mathscr{M},t}^{\langle\sigma,q_{0},\epsilon\rangle}(\eta)$, which does
not contain $\circledast$.

We start with the proof of the equivalence between the class of the PTM’s
polytime functions and that of the STMs’ polytime ones.

######  Proposition 8.

For any poly-time STM $\mathscr{S}$ there is a polytime PTM $\mathscr{M}$ such
that for every $\sigma\tau\in\mathbb{S}$:

$\mu(\\{\omega\in\mathbb{O}\mid
N(\sigma\omega)=\tau\\})=\text{Pr}[M(\sigma)=\tau]$

and viceversa.

###### Proof.

The claim can be restated as follows:

$\displaystyle\forall\sigma,\tau.\mu(\\{\eta\in\mathbb{B}^{\mathbb{N}}\ |\
N(\sigma,\eta)=\tau\\})$ $\displaystyle=\mu(M(\sigma)^{-1}(\tau))$
$\displaystyle\forall\sigma,\tau.\mu(\\{\eta\in\mathbb{B}^{\mathbb{N}}\ |\
N(\sigma,\eta)=\tau\\})$ $\displaystyle=\mu(\\{\eta\in\mathbb{B}^{\mathbb{N}}\
|\ Y_{M,\sigma}(\eta)=\tau\\}).$

Actually, we will show a stronger result: there is bijection
$I:\text{STMs}\longrightarrow\text{PTM}$ such that:

$\forall n\in\mathbb{N}.\\{\eta\in\mathbb{B}^{\mathbb{N}}\ |\
\langle\sigma,q_{0},\tau,\eta\rangle\triangleright^{n}_{\delta}\langle\tau,q,\psi,n\rangle\\}=\\{\eta\in\mathbb{B}^{\mathbb{N}}\
|\
X_{I(N),n}^{\langle\epsilon,q_{0},\sigma\rangle}(\eta)={\langle\tau,q,\psi\rangle}\\}$
(1)

which entails:

$\\{\eta\in\mathbb{B}^{\mathbb{N}}\ |\
N(\sigma,\eta)=\tau\\}=\\{\eta\in\mathbb{B}^{\mathbb{N}}\ |\
Y_{I(N),\sigma}(\eta)=\tau\\}.$ (2)

For this reason, it suffices to construct $I$ and prove that (1) holds. $I$
splits the function $\delta$ of $N$ in such a way that transition is assigned
to $\delta_{0}$ if it matches the character ${0}$ on the oracle-tape,
otherwise it is assigned to $\delta_{1}$. Observe that $I$ is bijective,
indeed, its inverse is a function as well, because it consists in a disjoint
union. Claim (1) can be shown by induction on the number of steps required by
$N$ to compute its output value, the proof is standard, so we omit it.

∎

######  Proposition 9.

For every $f:\mathbb{S}\times\mathbb{B}^{\mathbb{N}}\longrightarrow Ss$ in
$\mathbf{SFP}$, there is a function
$g:\mathbb{S}\times\mathbb{O}\longrightarrow\mathbb{S}$ in $\mathcal{POR}$
such that:

$\forall
x,y\in\mathbb{S}.\mu(\\{\omega\in\mathbb{O}|g(x,\omega)=y\\})=\mu(\\{\eta\in\mathbb{B}^{\mathbb{N}}|f(x,\eta)=y\\}).$

To prove the correspondence between the class of polytime STM computable
function and $\mathcal{POR}$, we pass through the class of _finite-stream_
TMs. These machines are defined analogously to STMs, but instead of an
infinite stream of bits $\eta$, they employ a finite sequence of random bits
as additional argument.

######  Lemma B.1.

For each $f\in\mathbf{SFP}$ with time-bound $p\in\mathsf{POLY}$, there is a
polytime _finite-stream_ TM computable function $h$ such that for any
$\eta\in\mathbb{B}^{\mathbb{N}}$ and $x,y\in\mathbb{S}$,

$f(x,\eta)=h(x,\eta_{p(|x|)}).$

###### Proof.

Assume that $f\in\mathbf{SFP}$. For this reason there is a polytime STM,
$\mathscr{S}=\langle{\mathcal{Q}},{q_{0}},{\Sigma},{\delta}\rangle$, such that
$f=f_{\mathscr{S}}$. Take the _Finite Stream Turing Machine_ (FSTM)
$\mathscr{S}^{\prime}$ which is defined identically to $\mathscr{S}$. It holds
that for any $k\in\mathbb{N}$ and some $\sigma,\tau,y^{\prime}\in\mathbb{S}$,

$\langle{{\epsilon}},{q_{0}^{\prime}},{x},{y}\rangle\triangleright^{k}_{\mathscr{S}}\langle{\sigma},{q},{\tau},{y^{\prime}}\rangle\
\ \ \Leftrightarrow\ \ \
\langle{\epsilon},q_{0}^{\prime},x,y\eta\rangle\triangleright^{k}_{\mathscr{S}^{\prime}}\langle{\sigma},{q},{\tau},{y^{\prime}\eta}\rangle.$

Moreover, $\mathscr{S}^{\prime}$ requires a number of steps which is exactly
equal to the number of steps required by $\mathscr{S}$, and thus the
complexity is preserved. We conclude the proof defining
$h=f_{\mathscr{S}^{\prime}}$. ∎

$c:=\langle\sigma,q,\tau,y\rangle$$s_{c}\in\mathbb{S}$$d:=\langle\sigma,q,\tau,y\rangle$$s_{d}\in\mathbb{S}$$\vdash_{\delta}$$\forall\omega.\mathit{step}(s_{c},e_{t}(\delta),\omega)=s_{d}$$e_{c}$$e_{c}$
Figure 1: Behavior of the function $\mathit{step}$.

The next step is to show that each polytime FSTM computable function $f$
corresponds to a function
$g:\mathbb{S}\times\mathbb{S}\times\mathbb{O}\longrightarrow\mathbb{S}$ of
$\mathcal{POR}$ which can be defined without recurring to $Q$.

######  Lemma B.2.

For any polytime FSTM computable function $f$ and $x\in\mathbb{S}$, there is
$g\in\mathcal{POR}$ such that $\forall x,y,\omega.f(x,y)=g(x,y,\omega).$
Moreover, if $f$ is defined without recurring to $Q$, $g$ can be defined
without $Q$ as well.

A formal proof of Lemma B.2 requires too much effort to be done extensively.
In this work, we will simply mention the high-level structure of the proof. It
relies on the following observations:

  1. 1.

It is possible to encode FSTMs, together with configurations and their
transition functions using strings, call these encodings
$e_{c}\in\mathcal{POR}$ and $e_{t}$. Moreover, there is a function
$\mathit{step}\in\mathcal{POR}$ which satisfies the simulation schema of
Figure 1. The proof of this result is done by explicit definition of the
functions $e_{c}$, $e_{t}$ and $\mathit{step}$, proving the correctness of
these entities with respect to the simulation schema above.

  2. 2.

For each $f\in\mathcal{POR}$ and $x,y\in\mathbb{S}$, if there is a term $t(x)$
in $\mathcal{RL}$ which bounds the size of $f(x,\omega)$ for each possible
input, then the function $m(z,x,\omega)=f^{|z|}(x,\omega)$ is in
$\mathcal{POR}$ as well, moreover, if $f$ is defined without recurring to $Q$,
also $m$ can be defined without recurring to $Q$. This is shown in Lemma B.3.

  3. 3.

Fixed a machine $M$, if $\sigma\in\mathbb{S}$ is a correct encoding of a
configuration of $M$, for every $\omega$, it holds that
$|\mathit{step}(\sigma,\omega)|\leq|\sigma|+c$, for $c\in\mathbb{N}$ fixed
once and forall.

  4. 4.

If $c:=e_{c}(\sigma,q,\tau,y,\omega)$ for some omega, then there is a function
$\mathit{dectape}$ such that
$\forall\omega\in\mathbb{O}.\mathit{dectape}(x,\omega)$ is the longest suffix
without occurrences of $\circledast$ of $\sigma$.

######  Lemma B.3.

For each
$f:\mathbb{S}^{k+1}\times\mathbb{O}\longrightarrow\mathbb{S}\in\mathcal{POR}$,
if there is a term $t\in\mathcal{RL}$ such that $\forall
x,\vec{z},\omega.f(x,\vec{z},\omega)|_{t}=f(x,\vec{z},\omega)$ then there is
also a function
$\mathit{sa}_{f,t}:\mathbb{S}^{k+2}\times\mathbb{O}\longrightarrow\mathbb{S}$
such that:

$\forall
x,n\in\mathbb{S},\omega\in\mathbb{O}.sa_{f,t}(x,n,\vec{z},\omega)=\underbrace{f(f(f(x,\vec{z},\omega),\vec{z},\omega),\ldots)}_{|n|\text{
times}}.$

Moreover, if $f$ is defined without recurring to $Q$, $sa_{f,t}$ can be
defined without $Q$ as well.

###### Proof.

Given $f\in\mathcal{POR}$ and $t\in\mathcal{L}_{\mathbb{PW}}$, let $sa_{f,t}$
be defined as follows:

$\displaystyle sa_{f,t}(x,{\epsilon},\vec{z},\omega)$ $\displaystyle:=x$
$\displaystyle sa_{f,t}(x,y{b},\vec{z},\omega)$
$\displaystyle:=f\big{(}sa_{f,t}(x,y,\omega),\vec{z},\omega\big{)}|_{t}$

The correctness of $\mathit{sa}$ comes as a direct consequence of its
definition by induction on $n$. ∎

Combining these results, we are able to prove Lemma B.2

###### Proof of Lemma B.2 (Sketch).

As a consequence of points (2) and (3), we obtain that:
$k(x,n,y,\omega)=\mathit{step}^{|n|}(x,y,\omega)$ belongs to $\mathcal{POR}$
and can be defined without recurring to $Q$. As a consequence of (1) we have
that:

$k^{\prime}(x,y,\omega):=k(e_{c}(x,q_{0},{\epsilon},y,\omega),y,\omega)$

belongs to $\mathcal{POR}$ as well and can be defined without recurring to
$Q$. Finally, as a consequence of (4) and $\mathcal{POR}$’s closure under
composition, there is a function $g$ which returns the longest prefix of the
leftmost projection of the output of $k^{\prime}$. This function is exactly:

$g(x,y,\omega):=dectape(k^{\prime}(x,y,\omega),\omega).$

∎

As another consequence of Lemma B.2, we show the result we were aiming to:
each function $f\in\mathbf{SFP}$ can be simulated by a function in
$g\in\mathcal{POR}$, using as an additional input a polynomial prefix of $f$’s
oracle.

######  Corollary 10.

For each $f\in\mathbf{SFP}$ and polynomial time-bound $p\in\mathsf{POLY}$,
there is a function $g\in\mathcal{POR}$ such that for any
$\eta:\mathbb{N}\longrightarrow\mathbb{B}$,
$\omega:\mathbb{N}\longrightarrow\mathbb{B}$ and $x\in\mathbb{S}$,

$f(x,\eta)=g\big{(}x,\eta_{p(|x|)},\omega\big{)}.$

Now, we need to establish that there is a function $e\in\mathcal{POR}$ which
produces strings with the same distribution of the prefixes of the functions
in $\mathbb{S}^{\mathbb{N}}$. Intuitively, this function is very simple: it
extracts $|x|+1$ bits from $\omega$ and concatenates them in its output. The
definition of the function $e$ passes through a bijection
$\mathit{dyad}:\mathbb{N}\longrightarrow\mathbb{S}$, called _dyadic
representation_ of a natural number. Thus, the function $e$ can simply create
the strings ${1}^{0},{1}^{1},\ldots,{1}^{k}$, and sample the function $\omega$
on the coordinates
$\mathit{dy}({1}^{0}),\mathit{dy}({1}^{1}),\ldots,\mathit{dy}({1}^{k})$,
concatenating the result in a string.

######  Definition 27.

The function $\mathit{dyad}:\mathbb{N}\longrightarrow\mathbb{S}$ associates
each $n\in\mathbb{N}$ to the string obtained stripping the left-most bit from
the binary representation of $n+1$.

######  Remark B.1.

There is a $\mathcal{POR}$ function
$\mathit{dy}:\mathbb{S}\times\mathbb{O}\longrightarrow\mathbb{S}$ such that
$\forall\sigma\in\mathbb{S}.\forall\omega\in\mathbb{O}.\mathit{dy}(\sigma,\omega)=\mathit{dyad}({1}^{|\sigma|})$.

The construction of this function is not much interesting to the aim of our
proof, so we omit it.

######  Definition 28.

Let $e:\mathbb{S}\times\mathbb{O}\longrightarrow\mathbb{S}$ be defined as
follows:

$\displaystyle e({\epsilon},\omega)$ $\displaystyle={\epsilon};$
$\displaystyle e(x{b},\omega)$
$\displaystyle=e(x,\omega)Q\big{(}\mathit{dy}(x,\omega),\omega\big{)}|_{x{b}}.$

######  Lemma B.4 (Correctness of $e$).

For any $\sigma\in\mathbb{S}$ and $i\in\mathbb{N}$, if $|\sigma|=i+1$, for any
$j\leq i\in\mathbb{N}$ and $\omega\in\mathbb{O}$, $(i)$
$e(\sigma,\omega)(j)=\omega(\mathit{dy}({1}^{j},\omega))$ and $(ii)$ the
length of $e(\sigma,\omega)$ is exactly $i+1$.

###### Proof.

Both claims are proved by induction on $\sigma$. The latter is trivial,
whereas the former requires some more effort:

  * ${\epsilon}$

The claim comes from vacuity of the premise $|\sigma|=i+1$.

  * $\tau{b}$

It holds that:
$e(\tau{b},\omega)(j)=e(\tau,\omega)Q\big{(}\mathit{dy}(\tau,\omega),\omega\big{)}=e(\tau,\omega)\omega\big{(}\mathit{dy}(\tau,\omega)\big{)}.$
By $(ii)$, for $j=i+1$, the $j$-th element of $e(\tau{b},\omega)$ is exactly
$Q\big{(}\mathit{dy}(\tau,\omega),\omega\big{)}$, which is equal to
$\omega(\mathit{dy}(\tau,\omega))$, in turn equal to
$\omega(\mathit{dy}({1}^{j},\omega))$ (by Remark B.1). For smaller values of
$j$, the first claim is a consequence of the definition of $e$ together with
IH.

∎

######  Definition 29.

We define $\sim_{\mathit{dy}}$ as the smallest relation in
$\mathbb{O}\times\mathbb{B}^{\mathbb{N}}$ such that:

$\eta\sim_{\mathit{dy}}\omega\leftrightarrow\forall
n\in\mathbb{N}.\eta(n)=\omega(\mathit{dy}({1}^{n+1},\omega)).$

######  Lemma B.5.

It holds that:

  * •

$\forall\eta\in\mathbb{B}^{\mathbb{N}}.\exists!\omega\in\mathbb{O}.\eta\sim_{\mathit{dy}}\omega$;

  * •

$\forall\omega\in\mathbb{O}.\exists!\eta\in\mathbb{B}^{\mathbb{N}}.\eta\sim_{\mathit{dy}}\omega$.

###### Proof.

The proofs of the two claims are very similar. Since _dyad_ is a bijection,
applying Remark B.1, we obtain the existence of an $\omega$ which is in
relation with $\eta$. Now suppose that there are $\omega_{1},\omega_{2}$ both
in relation with $\eta$ but they are different. Then, there is a
$\sigma\in\mathbb{S}$, such that $\omega_{1}(\sigma)\neq\omega_{2}(\sigma)$
and, by Remark B.1,
$\mathit{dy}(\sigma,\omega_{1})=\mathit{dy}(\sigma,\omega_{2})$ which entails
that $\eta(k)\neq\eta(k)$ for some $k$, that is a contradiction. ∎

######  Corollary 11.

The relation $\sim_{\mathit{dy}}$ is a bijection.

###### Proof.

Consequence of Lemma B.5. ∎

######  Lemma B.6.

$\eta\sim_{\mathit{dy}}\omega\to\forall
n\in\mathbb{N}.\eta_{n}=e(1^{n+1},\omega).$

###### Proof.

By contraposition: suppose $\eta_{n}\neq
e({\underline{n}}_{\mathbb{N}},\omega).$ As a consequence of the correctness
of $e$ (Lemma B.4), there is an $i\in\mathbb{N}$ such that
$\eta(i)\neq\omega(\mathit{dy}({\underline{i}}_{\mathbb{N}},\omega))$, which
is a contradiction. ∎

We can finally conclude the proof of Proposition 9.

###### Proof of Proposition 9.

From Corollary 10, we know that there is a function
$f^{\prime}\in\mathcal{POR}$, and a $p\in\mathsf{POLY}$ such that:

$\forall x,y\in\mathbb{S}.\forall\eta.\forall\omega.y=\eta_{p(x)}\to
f(x,\eta)=f^{\prime}(x,y,\omega).$ ($*$)

Fixed an $\overline{\eta}\in\\{\eta\in\mathbb{B}^{\mathbb{N}}\ |\
f(x,\eta)=y\\}$, its image with respect to $\sim_{\mathit{dy}}$ is in
$\\{\omega\in\mathbb{O}\ \mid\
f^{\prime}(x,e(p^{\prime}(\mathit{s}(x,\omega),\omega),\omega),\omega)=y\\},$
where $\mathit{s}$ is the $\mathcal{POR}$-function computing ${1}^{|x|}$.
Indeed, by Lemma B.6, it holds that
$\overline{\eta}_{p(x)}=e(p(\mathit{size}(x,\omega),\omega)$, where
$p^{\prime}$ is the $\mathcal{POR}$-function computing the polynomial $p$,
defined without recurring to $Q$. By $(*)$, we prove the claim. It also holds
that, given a fixed $\overline{\omega}\in\\{\omega\in\mathbb{O}\ |\
f^{\prime}(x,e(p^{\prime}(\mathit{size}(x,\omega),\omega),\omega),\omega)=y\\}$,
its pre-image with respect to $\sim_{\mathit{dy}}$ is in
$\\{\eta\in\mathbb{B}^{\mathbb{N}}\ |\ f(x,\eta)=y\\}$. The proof is analogous
to the one we showed above. Now, since $\sim_{\mathit{dy}}$ is a bijection
between the two sets: $\mu\big{(}\\{\eta\in\mathbb{B}^{\mathbb{N}}\ |\
f(x,\eta)=y\\}\big{)}=\mu\big{(}\\{\omega\in\mathbb{O}\ |\
f^{\prime}(x,e(p(\mathit{size}(x,\omega),\omega),\omega),\omega)=y\\}\big{)},$
which concludes the proof. ∎

###  B.2 From $\mathcal{POR}$ to $\mathbf{SFP}$

We start defining the imperative language $\mathbf{SIFP_{{\mathbf{RA}}}}$ and
proving its polytime programs equivalent to $\mathcal{POR}$. To do so, we
first introduce the definition of $\mathbf{SIFP_{{\mathbf{RA}}}}$ and its
_big-step_ semantics.

######  Definition 30 (Correct programs of $\mathbf{SIFP_{{\mathbf{RA}}}}$).

The language of $\mathbf{SIFP_{{\mathbf{RA}}}}$ programs is
${\mathcal{L}({\mathsf{Stm}_{\mathbf{RA}}})}$, i.e. the set of strings
produced by the non-terminal symbol $\mathsf{Stm}_{\mathbf{RA}}$ defined by:

$\displaystyle\mathsf{Id}$ $\displaystyle::=X_{i}\ |\ Y_{i}\ |\ S_{i}\ |\ R\
|\ Q\ |\ Z\ |\ T\qquad i\in\mathbb{N}$ $\displaystyle\mathsf{Exp}$
$\displaystyle::=\epsilon\ |\ \mathsf{Exp}.\mathtt{0}\ |\
\mathsf{Exp}.\mathtt{1}\ |\ \mathsf{Id}\ |\
\mathsf{Exp}\sqsubseteq\mathsf{Id}\ |\ \mathsf{Exp}\land\mathsf{Id}\ |\
\lnot\mathsf{Exp}$ $\displaystyle\mathsf{Stm}_{\mathbf{RA}}$
$\displaystyle::=\mathsf{Id}\leftarrow\mathsf{Exp}\ |\
\mathsf{Stm}_{\mathbf{RA}};\mathsf{Stm}_{\mathbf{RA}}\ |\
\mathtt{while}(\mathsf{Exp})\\{\mathsf{Stm}\\}_{\mathbf{RA}}\ |\
\mathtt{Flip(}\mathsf{Exp}\mathsf{)}$

The _big-step_ semantics associated to the language of the
$\mathbf{SIFP_{{\mathbf{RA}}}}$ programs relies on the notion of _Store_ ,
which for us is a function
$\Sigma:\mathsf{Id}\rightharpoonup\\{\mathtt{0},\mathtt{1}\\}^{*}$.

We define the updating of a store $\Sigma$ with a mapping from
$y\in\mathsf{Id}$ to $\tau\in\\{\mathtt{0},\mathtt{1}\\}^{*}$ as:

$\Sigma[y\leftarrow\tau](x):=\begin{cases}\tau&\text{if }x=y\\\
\Sigma(x)&\text{otherwise.}\end{cases}$

######  Definition 31 (Semantics of $\mathbf{SIFP}$ expressions).

The semantics of an expression $E\in{\mathcal{L}({\mathsf{Exp}})}$ is the
smallest relation
$\rightharpoonup:{\mathcal{L}({\mathsf{Exp}})}\times(\mathsf{Id}\longrightarrow\\{\mathtt{0},\mathtt{1}\\}^{*})\times\mathbb{O}\times\\{\mathtt{0},\mathtt{1}\\}^{*}$
closed under the following rules:

$\langle\epsilon,\Sigma\rangle\rightharpoonup\epsilon$
$\langle\epsilon,\Sigma\rangle\rightharpoonup\epsilon$ $\langle
e,\Sigma\rangle\rightharpoonup\sigma$ $\langle
e.\mathtt{0},\Sigma\rangle\rightharpoonup\sigma\frown\mathtt{0}$ $\langle
e,\Sigma\rangle\rightharpoonup\sigma$ $\langle
e.\mathtt{1},\Sigma\rangle\rightharpoonup\sigma\frown\mathtt{1}$

$\langle e,\Sigma\rangle\rightharpoonup\sigma$ $\Sigma(\mathsf{Id})=\tau$
$\sigma\subseteq\tau$ $\langle
e\sqsubseteq\mathsf{Id},\Sigma\rangle\rightharpoonup\mathtt{1}$ $\langle
e,\Sigma\rangle\rightharpoonup\sigma$ $\Sigma(\mathsf{Id})=\tau$
$\sigma\not\subseteq\tau$ $\langle
e\sqsubseteq\mathsf{Id},\Sigma\rangle\rightharpoonup\mathtt{0}$

$\Sigma(\mathsf{Id})=\sigma$
$\langle\mathsf{Id},\Sigma\rangle\rightharpoonup\sigma$
$\mathsf{Id}\not\in\mathit{dom}(\Sigma)$
$\langle\mathsf{Id},\Sigma\rangle\rightharpoonup\epsilon$ $\langle
e,\Sigma\rangle\rightharpoonup\mathtt{0}$ $\langle\lnot
e,\Sigma\rangle\rightharpoonup\mathtt{1}$ $\langle
e,\Sigma\rangle\rightharpoonup\sigma$ $\sigma\neq\mathtt{0}$ $\langle\lnot
e,\Sigma\rangle\rightharpoonup\mathtt{0}$

$\langle e,\Sigma\rangle\rightharpoonup\mathtt{1}$
$\Sigma(\mathsf{Id})=\mathtt{1}$ $\langle
e\land\mathsf{Id},\Sigma\rangle\rightharpoonup\mathtt{1}$ $\langle
e,\Sigma\rangle\rightharpoonup\sigma$ $\Sigma(\mathsf{Id})=\tau$
$\sigma\neq\mathtt{1}\land\tau\neq\mathtt{1}$ $\langle
e\land\mathsf{Id},\Sigma\rangle\rightharpoonup\mathtt{0}$

######  Definition 32 (big-step Operational Semantics of
$\mathbf{SIFP_{{\mathbf{RA}}}}$).

The semantics of a program $P\in{\mathcal{L}({\mathsf{Stm}_{\mathbf{RA}}})}$
is the smallest relation
$\triangleright\subseteq{\mathcal{L}({\mathsf{Stm}_{\mathbf{RA}}})}\times(\mathsf{Id}\longrightarrow\\{\mathtt{0},\mathtt{1}\\}^{*})\times\mathbb{O}\times(\mathsf{Id}\longrightarrow\\{\mathtt{0},\mathtt{1}\\}^{*})$
closed under the following rules:

$\langle e,\Sigma\rangle\rightharpoonup\sigma$ $\langle\mathsf{Id}\leftarrow
e,\Sigma,\omega\rangle\triangleright\Sigma[\mathsf{Id}\leftarrow\sigma]$
$\langle s,\Sigma,\omega\rangle\triangleright\Sigma^{\prime}$ $\langle
t,\Sigma^{\prime},\omega\rangle\triangleright\Sigma^{\prime\prime}$ $\langle
s;t,\Sigma,\omega\rangle\triangleright\Sigma^{\prime\prime}$

$\langle e,\Sigma\rangle\rightharpoonup\mathtt{1}$ $\langle
s,\Sigma,\omega\rangle\triangleright\Sigma^{\prime}$
$\langle\mathtt{while}(e)\\{s\\},\Sigma^{\prime},\omega\rangle\triangleright\Sigma^{\prime\prime}$
$\langle\mathtt{while}(e)\\{s\\},\Sigma,\omega\rangle\triangleright\Sigma^{\prime\prime}$
$\langle e,\Sigma\rangle\rightharpoonup\sigma$ $\sigma\neq\mathtt{1}$
$\langle\mathtt{while}(e)\\{s\\},\Sigma,\omega\rangle\triangleright\Sigma$

$\langle e,\Sigma\rangle\rightharpoonup\sigma$ $\omega(\sigma)=b$
$\langle\mathtt{Flip(}e\mathsf{)},\Sigma,\omega\rangle\triangleright\Sigma[R\leftarrow
b]$

This semantics allows us to associate each $\mathbf{SIFP_{{\mathbf{RA}}}}$
program to the function it evaluates:

######  Definition 33 (Function evaluated by a $\mathbf{SIFP_{{\mathbf{RA}}}}$
program).

We say that the function evaluated by a correct
$\mathbf{SIFP_{{\mathbf{RA}}}}$ program $P$ is
$\mathcal{\llbracket}\cdot\rrbracket:{\mathcal{L}({\mathsf{Stm}_{{\mathbf{RA}}}})}\longrightarrow(\mathbb{S}^{n}\times\mathbb{O}\longrightarrow\mathbb{S})$,
defined as below333Instead of the infix notation for $\triangleright$, we will
use its prefixed notation. So, the notation express the store associated to
the $P$, $\Sigma$ and $\omega$ by $\triangleright$. Moreover, notice that we
employed the same function symbol $\triangleright$ to denote two distinct
functions: the _big-step_ operational semantics of
$\mathbf{SIFP_{{\mathbf{RA}}}}$ programs and the _big-step_ operational
semantics of $\mathbf{SIFP_{{\mathbf{LA}}}}$ programs:

$\llbracket P\rrbracket:=\lambda
x_{1},\ldots,x_{n},\omega.\triangleright(\langle P,[][X_{1}\leftarrow
x_{1}],\ldots,[X_{n}\leftarrow x_{n}],\omega\rangle)(R).$

Observe that, among all the different registers, the register $R$ is meant to
contain the value computed by the program at the end of its execution,
similarly the $\\{X_{i}\\}_{i\in\mathbb{N}}$ registers are used to store the
function’s inputs. The correspondence between $\mathcal{POR}$ and
$\mathbf{SIFP_{{\mathbf{RA}}}}$ can be stated as follows:

######  Lemma B.7 (Implementation of $\mathcal{POR}$ in
$\mathbf{SIFP_{{\mathbf{RA}}}}$).

For every function $f\in\mathcal{POR}$, there is a polytime
$\mathbf{SIFP_{{\mathbf{RA}}}}$ program $P$ such that: $\forall x_{1},\ldots
x_{n}.\llbracket
P\rrbracket(x_{1},\ldots,x_{n},\omega)=f(x_{1},\ldots,x_{n},\omega)$.
Moreover, if $f$ can be defined without recurring to $Q$, then $P$ does not
contain any $\mathtt{Flip(}e\mathsf{)}$ statement.

The proof of this result is quite simple: it relies on the fact that it is
possible to associate to each $\mathcal{POR}$ function an equivalent polytime
program, and on the observation that it is possible to compose them and to
implement bounded recursion on notation in $\mathbf{SIFP_{{\mathbf{RA}}}}$
with a polytime overhead.

###### Proof Sketch of Lemma B.7.

For each function $f\in\mathcal{POR}$ we define a program ${\mathfrak{L}_{f}}$
such that
$\llbracket{\mathfrak{L}_{f}}\rrbracket(x_{1},\ldots,x_{n})=f(x_{1},\ldots,x_{n})$
The correctness of ${\mathfrak{L}_{f}}$ is given by the following invariant
properties:

  * •

The result of the computation is stored in $R$.

  * •

The inputs are stored in the registers of the group $X$.

  * •

The function ${\mathfrak{L}_{\cdot}}$ does not change the values it accesses
as input.

We define the function ${\mathfrak{L}_{f}}$ as follows:
${\mathfrak{L}_{E}}:=R\leftarrow\epsilon$;
${\mathfrak{L}_{S_{0}}}:=R\leftarrow X_{0}.\mathtt{0}$;
${\mathfrak{L}_{S_{1}}}:=R\leftarrow X_{0}.\mathtt{1}$;
${\mathfrak{L}_{{P}^{n}_{i}}}:=R\leftarrow X_{i}$;
${\mathfrak{L}_{C}}:=R\leftarrow X_{1}\sqsubseteq X_{2}$;
${\mathfrak{L}_{Q}}:=\mathtt{Flip(}X_{1}\mathsf{)}$. The correctness of these
base cases is trivial. Moreover, it is simple to see that the only translation
containing $\mathtt{Flip(}e\mathsf{)}$ for some
$e\in{\mathcal{L}({\mathsf{Exp}})}$ is the translation of $Q$. The encoding of
the composition and of the bounded recursion are a little more convoluted: the
proof of their correctness requires a conspicuous amount of low-level
definitions and technical results, whose presentation is not the aim of this
work. ∎

The next step is to sow that every $\mathbf{SIFP_{{\mathbf{RA}}}}$ program is
equivalent to a $\mathbf{SIFP_{{\mathbf{LA}}}}$ program in the sense of Lemma
B.8.

######  Lemma B.8.

For each total program $P\in\mathbf{SIFP_{{\mathbf{RA}}}}$ there is a
$Q\in\mathbf{SIFP_{{\mathbf{LA}}}}$ such that:

$\forall x,y.\mu\left(\\{\omega\in\mathbb{B}^{\mathbb{S}}|\llbracket
P\rrbracket(x,\omega)=y\\}\right)=\mu\left(\\{\eta\in\mathbb{B}^{\mathbb{N}}|\llbracket
Q\rrbracket(x,\eta)=y\\}\right).$

Moreover, if $P$ is polytime $Q$ is polytime, too.

Before delving into the details of the proof of this Lemma, we must define the
language $\mathbf{SIFP_{{\mathbf{LA}}}}$ together with its standard semantics:

######  Definition 34 ($\mathbf{SIFP_{{\mathbf{LA}}}}$).

The language of the $\mathbf{SIFP_{{\mathbf{LA}}}}$ programs is
${\mathcal{L}({\mathsf{Stm}_{\mathbf{LA}}})}$, i.e. the set of strings
produced by the non-terminal symbol $\mathsf{Stm}_{\mathbf{LA}}$ described as
follows:

$\mathsf{Stm}_{\mathbf{LA}}::=\mathsf{Id}\leftarrow\mathsf{Exp}\ |\
\mathsf{Stm}_{\mathbf{LA}};\mathsf{Stm}_{\mathbf{LA}}\ |\
\mathtt{while}(\mathsf{Exp})\\{\mathsf{Stm}\\}_{\mathbf{LA}}\ |\
\mathtt{RandBit()}\\\ $

######  Definition 35 (Big Step Operational Semantics of
$\mathbf{SIFP_{{\mathbf{LA}}}}$).

The semantics of a program $P\in{\mathcal{L}({\mathsf{Stm}_{\mathbf{LA}}})}$
is the smallest relation
$\triangleright\subseteq\left({\mathcal{L}({\mathsf{Stm}_{\mathbf{LA}}})}\times(\mathsf{Id}\longrightarrow\\{\mathtt{0},\mathtt{1}\\}^{*})\times\mathbb{B}^{\mathbb{N}}\right)\times\left((\mathsf{Id}\longrightarrow\\{\mathtt{0},\mathtt{1}\\}^{*})\times\mathbb{B}^{\mathbb{N}}\right)$
closed under the following rules:

$\langle e,\Sigma\rangle\rightharpoonup\sigma$ $\langle\mathsf{Id}\leftarrow
e,\Sigma,\eta\rangle\triangleright\langle\Sigma[\mathsf{Id}\leftarrow\sigma],\eta\rangle$
$\langle
s,\Sigma,\eta\rangle\triangleright\langle\Sigma^{\prime},\eta^{\prime}\rangle$
$\langle
t,\Sigma^{\prime},\eta\rangle\triangleright\langle\Sigma^{\prime\prime},\eta^{\prime\prime}\rangle$
$\langle
s;t,\Sigma,\eta\rangle\triangleright\langle\Sigma^{\prime\prime},\eta^{\prime\prime}\rangle$

$\langle e,\Sigma\rangle\rightharpoonup\mathtt{1}$ $\langle
s,\Sigma,\eta\rangle\triangleright\langle\Sigma^{\prime},\eta^{\prime}\rangle$
$\langle\mathtt{while}(e)\\{s\\},\Sigma^{\prime},\eta\rangle\triangleright\langle\Sigma^{\prime\prime},\eta^{\prime\prime}\rangle$
$\langle\mathtt{while}(e)\\{s\\},\Sigma,\eta\rangle\triangleright\langle\Sigma^{\prime\prime},\eta^{\prime\prime}\rangle$

$\langle e,\Sigma\rangle\rightharpoonup\sigma$ $\sigma\neq\mathtt{1}$
$\langle\mathtt{while}(e)\\{s\\},\Sigma,\eta\rangle\triangleright\langle\Sigma,\eta\rangle$
$\langle\mathtt{RandBit()}\Sigma,\mathtt{b}\eta\rangle\triangleright\langle\Sigma[R\leftarrow\mathtt{b}],\eta\rangle$
$\langle\mathtt{RandBit()},\Sigma,\mathtt{b}\eta\rangle\triangleright\langle\Sigma[R\leftarrow\mathtt{b}],\eta\rangle$

In particular, we prove Lemma B.8 showing that $\mathbf{SIFP_{{\mathbf{RA}}}}$
can be simulated in $\mathbf{SIFP_{{\mathbf{LA}}}}$ with respect to two novel
_small-step_ semantic relations
(${\leadsto_{\mathbf{LA}}},{\leadsto_{\mathbf{RA}}}$) derived splitting the
_big-step_ semantics into small transitions, one per each $\cdot;\cdot$
instruction. Intuitively, the idea behind this novel semantics is to enrich
the _big-step_ operational semantic with some pieces of information necessary
to build a proof that it is possible to each $\mathbf{SIFP_{{\mathbf{LA}}}}$
instruction by meas of a sequence of $\mathbf{SIFP_{{\mathbf{RA}}}}$
instructions preserving the distribution of the values in the register $R$,
i.e. that storing the result. In particular we enrich the configurations of
$\mathbf{SIFP_{{\mathbf{LA}}}}$’s and $\mathbf{SIFP_{{\mathbf{RA}}}}$’s
_small-step_ operational semantics with a list $\Psi$ containing pairs
$(x,b)$. In the case of $\mathbf{SIFP_{{\mathbf{LA}}}}$, this list is meant to
keep track of the calls to the primitive $\mathtt{Flip(}x\mathsf{)}$ and their
result $b$. While, on the side of $\mathbf{SIFP_{{\mathbf{RA}}}}$, the $x$-th
call of the primitive $\mathtt{RandBit()}$ causes the pair $(x,b)$ to be added
on top of the list.

This is done to keep track of the accesses to the random tapes done by the
simulated and the simulator programs. On the side of
$\mathbf{SIFP_{{\mathbf{RA}}}}$ it is possible to show that this table is
stored in a specific register. This register plays an important role in the
simulation of the $\mathtt{Flip(}e\mathsf{)}$ instructions. In particular,
this is done as follows:

  * •

At each simulated query $\mathtt{Flip(}e\mathsf{)}$, the destination program
looks up the associative table;

  * •

If it finds the queried coordinate $e$ within a pair $(e,b)$, it returns $b$,
otherwise:

    * –

It reduces $\mathtt{Flip(}e\mathsf{)}$ to a call of $\mathtt{RandBit()}$ which
outputs either $\mathtt{b}={0}$ or $\mathtt{b}={1}$.

    * –

It records the pair $\langle e,\mathtt{b}\rangle$ in the associative table and
stores $\mathtt{b}$ in $R$.

Even in this case the construction of the proof is convoluted, but we believe
that it is not too much of a problem to see, at least intuitively, that this
kind of simulation preserves the distributions of strings computed by the
original program. This concludes Lemma B.8.

The next step is to show that $\mathbf{SIFP_{{\mathbf{LA}}}}$ can be reduced
to $\mathbf{SFP_{\mathbf{OD}}}$: the class corresponding to $\mathbf{SFP}$
defined on a variation of the Stream Machines which are capable to read
characters from the oracle tape _on-demand_ , i.e. only on those states
$q\in\mathcal{Q}_{\natural}\subseteq\mathcal{Q}$. The transition function of
the $\mathbf{SFP_{\mathbf{OD}}}$ is a function
$\delta:{\hat{\mathbb{B}}}\times{\mathcal{Q}}\times{\left({\hat{\mathbb{B}}\cup\\{\natural\\}}\right)}\times\mathbb{B}\longrightarrow{\hat{\mathbb{B}}}\times{\mathcal{Q}}\times{\hat{\mathbb{B}}}\times\\{{L},{R}\\}$
which for all the states in $\mathcal{Q}_{\natural}$ is labeled with the
symbol $\natural$ instead of a Boolean value. This peculiarity will be
employed in Definition 36 to distinguish those configurations causing the
oracle tape to shift to the others.

We do not show the reduction from $\mathbf{SIFP_{{\mathbf{LA}}}}$ to
$\mathbf{SFP_{\mathbf{OD}}}$ extensively because this kind of reductions are
cumbersome and, in literature, it is common to avoid their formal definition
on behalf of a more readable presentation. For this reason, we only describe
informally but exhaustively how to build the _on-demand_ stream machine which
corresponds to a generic program
$P\in{\mathcal{L}({\mathsf{Stm}_{\mathbf{LA}}})}$. The correspondence between
$\mathbf{SFP_{\mathbf{OD}}}$ is expressed by the following Proposition:

######  Proposition 10.

For every $P\in{\mathcal{L}({\mathsf{Stm}_{\mathbf{LA}}})}$ there is a
$M_{P}\in\mathbf{SFP}$ such that for every $x\in\mathbb{S}$ and
$\eta\in\mathbb{B}^{\mathbb{S}}$, $P(x,\eta)=P(x,\eta)$. Moreover, if $P$ is
polytime, then $M_{P}$ is polytime.

###### Proof.

The construction relies on the fact that it is possible to implement a
$\mathbf{SIFP_{{\mathbf{LA}}}}$ program by means of a multi-tape _on-demand
stream machine_ which uses a tape to store the values of each register, plus
an additional tape containing the partial results obtained during the
evaluation of the expressions and another tape containing $\eta$. We denote
the tape used for storing the result coming from the evaluation of the
expressions with $e$.

The machine works thanks to some invariant properties:

  * •

On each tape, the values are stored to the immediate right of the head.

  * •

The result of the last expression evaluated is stored on the $e$ tape to the
immediate right of the head.

The value of a $\mathbf{SIFP}$ expression can be easily computed using the $e$
tape. We show it by induction on the syntax of the expression:

  * •

Each access to the value stored in a register basically consist in a copy of
the content of the corresponding tape to the $e$ tape, which is a simple
operation, due to the invariant properties properties mentioned above.

  * •

Concatenations ($f.\mathtt{0}$ and $f.\mathtt{1}$) are easily implemented by
the addition of a character at the end of the $e$ tape which contains the
value of $f$, as stated by the induction hypothesis on the invariant
properties.

  * •

The binary expressions are non-trivial, but since one of the two operands is a
register identifier, the machine can directly compare $e$ with the tape which
corresponding to the identifier, and to replace the content of $e$ with the
result of the comparison, which in all cases ${0}$ or ${1}$.

All these operations can be implemented without consuming any character on the
oracle tape and with linear time with respect to the size of the expression’s
value. To each statement $s_{i}$, we assign a sequence of machine states,
$q_{s_{i}}^{I},q_{s_{i}}^{1},q_{s_{i}}^{2},\ldots,q_{s_{i}}^{F}$.

  * •

Assignments consist in a copy of the value in $e$ to the tape corresponding to
the destination register and a deletion of the value on $e$ by replacing its
symbols with $\circledast$ characters. This can be implemented without
consuming any character on the oracle tape.

  * •

The sequencing operation $s;t$ can be implemented inserting in $\delta$ a
composed transition from $q_{s}^{F}$ to $q_{t}^{I}$, which does not consume
the oracle tape.

  * •

A $\mathtt{while}($){s}tatement $s:=\mathtt{while}(f)\\{t\\}$ requires the
evaluation of $f$ and then passing to the evaluation of $t$, if
$f\rightharpoonup\mathtt{1}$, or stepping to the next transition if it exists
and $f\not\rightharpoonup\mathtt{1}$. After the evaluation of the body, the
machine returns to the initial state of this statement, namely: $q_{s}^{I}$.

  * •

A $\mathtt{RandBit()}$ statement is implemented consuming a character on the
tape and copying its value on the tape which corresponds to the register $R$.

The following invariant properties hold at the beginning of the execution and
are kept true throughout $M_{P}$’s execution. In particular, if we assume $P$
to be polytime, after the simulation of each statement, it holds that:

  * •

The length of the non blank portion of the first tapes corresponding to the
register is polynomially bounded because their contents are precisely the
contents of $P$’s registers, which are polynomially bounded as a consequence
of the hypotheses on their polynomial time complexity.

  * •

The head of all the tapes corresponding to the registers point to the leftmost
symbol of the string thereby contained.

It is well-known that the reduction of the number of tapes on a polytime
Turing Machine comes with a polynomial overhead in time; for this reason, we
can conclude that the polytime _multi-tape_ on-demand stream machine we
introduced above can be _shrinked_ to a polytime _canonical_ on-demand stream
machine. This concludes the proof. ∎

It remains to show that each on-demand stream machine can be reduced to an
equivalent STM.

######  Lemma B.9.

For every
$\mathscr{S}=\langle\mathcal{Q},\mathcal{Q}_{\natural},\Sigma,\delta,q_{0}\rangle\in\mathbf{SFP_{\mathbf{OD}}}$,
the machine
$\mathscr{S}^{\prime}=\langle\mathcal{Q},\Sigma,H(\delta),q_{0}\rangle\in\mathbf{SFP}$
is such that for every $n\in\mathbb{N}$, for every configuration of
$\mathscr{S}$ $\langle\sigma,q,\tau,\eta\rangle$ and for every
$\sigma^{\prime},\tau^{\prime}\in\mathbb{S},q\in\mathcal{Q}$:

$\mu\left(\\{\eta\in\mathbb{B}^{\mathbb{N}}|\exists\eta^{\prime}.\langle\sigma,q,\tau,\eta\rangle\triangleright^{n}_{\delta}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\eta^{\prime}\rangle\\}\right)=\mu\left(\\{\chi\in\mathbb{B}^{\mathbb{N}}|\exists\chi^{\prime}.\langle\sigma,q,\tau,\xi\rangle\triangleright^{n}_{H(\delta)}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\chi^{\prime}\rangle\\}\right).$

Even in this case, the proof relies on a reduction. In particular, we show
that given an on-demand stream machine $\mathscr{S}$ it is possible to build a
stream machine $\mathscr{S}^{\prime}$ which is equivalent to $\mathscr{S}$.
Intuitively, the encoding from an _on-demand_ stream machine $\mathscr{S}$ to
an ordinary stream machine takes the transition function $\delta$ of
$\mathscr{S}$ and substitutes each transition not causing the oracle tape to
shift — i.e. tagged with $\natural$ — with two distinct transitions, so to
match both $\mathtt{0}$ and $\mathtt{1}$ on the tape storing $\omega$. This
causes the resulting machine to reach the same target state with the same
behavior n the work tape, and to shift to the right the head on the oracle
tape.

######  Definition 36 (Encoding from On-Demand to Canonical Stream Machines).

We define the encoding from an On-Demand Stream Machine to a Canonical Stream
Machine as below:

$H:=\langle\mathbb{Q},\Sigma,\delta,q_{0}\rangle\mapsto\left\langle\mathbb{Q},\Sigma,\bigcup\Delta_{H}(\delta),q_{0}\right\rangle.$

where $\Delta_{H}$ is defined as follows:

$\displaystyle\Delta_{H}(\langle p,c_{r},{0},q,c_{w},d\rangle)$
$\displaystyle:=\\{\langle p,c_{r},{0},q,c_{w},d\rangle\\}$
$\displaystyle\Delta_{H}(\langle p,c_{r},{1},q,c_{w},d\rangle)$
$\displaystyle:=\\{\langle p,c_{r},{1},q,c_{w},d\rangle\\}$
$\displaystyle\Delta_{H}(\langle p,c_{r},\natural,q,c_{w},d\rangle)$
$\displaystyle:=\\{\langle p,c_{r},{0},q,c_{w},d\rangle,\langle
p,c_{r},{1},q,c_{w},d\rangle\\}.$

###### Proof of Lemma B.9.

The definition of $\triangleright^{n}_{\delta}$ allows us to rewrite the
statement
$\exists\eta^{\prime}.\langle\sigma,q,\tau,\eta\rangle\triangleright^{n}_{\delta}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\eta^{\prime}\rangle$
as:

$\displaystyle\exists\eta^{\prime},\eta^{\prime\prime}\in\mathbb{B}^{\mathbb{N}}.\exists
c_{1},\ldots,c_{k}.$ $\displaystyle\langle\sigma,q,\tau,c_{1}c_{2}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{n_{1}}_{\delta}\langle\sigma_{1},q_{i_{1}},\tau_{1},c_{1}c_{2}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{1}_{\delta}\langle\sigma_{1}^{\prime},q_{i_{1}}^{\prime},\tau_{1},c_{2}\ldots
c_{k}\eta^{\prime}\rangle\land$
$\displaystyle\langle\sigma_{1}^{\prime},q_{i_{1}}^{\prime},\tau_{1},c_{2}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{n_{2}}_{\delta}\langle\sigma_{2},q_{i_{2}},\tau_{2},c_{2}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{1}_{\delta}\langle\sigma_{2}^{\prime},q_{i_{2}}^{\prime},\tau_{2}^{\prime},c_{3}\ldots
c_{k}\eta^{\prime}\rangle\land$
$\displaystyle\langle\sigma_{2}^{\prime},q_{i_{2}}^{\prime},\tau_{2}^{\prime},c_{3}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{n_{3}}_{\delta}\ldots\triangleright^{n_{k+1}}_{\delta}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\eta^{\prime}\rangle.$

The claim can be rewritten as follows:
$\begin{aligned}
&\exists\eta^{\prime\prime},c_{1},\ldots,c_{k}\in\mathbb{B}.\exists
n_{1},\ldots,n_{k+1}\in\mathbb{N}.\forall\xi_{1},\ldots,\xi_{k+1}\in\mathbb{S}.|\xi_{1}|=n_{1}\land\ldots|\xi_{k+1}|=n_{k+1}\land\\\
&\langle\sigma,q,\tau,c_{1}c_{2}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{n_{1}}_{\delta}\langle\sigma_{1},q_{i_{1}},\tau_{1},c_{1}c_{2}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{1}_{\delta}\langle\sigma_{1}^{\prime},q_{i_{1}}^{\prime},\tau_{1},c_{2}\ldots
c_{k}\eta^{\prime}\rangle\land\\\
&\langle\sigma_{1}^{\prime},q_{i_{1}}^{\prime},\tau_{1},c_{2}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{n_{2}}_{\delta}\langle\sigma_{2},q_{i_{2}},\tau_{2},c_{2}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{1}_{\delta}\langle\sigma_{2}^{\prime},q_{i_{2}}^{\prime},\tau_{2}^{\prime},c_{3}\ldots
c_{k}\eta^{\prime}\rangle\land\\\
&\langle\sigma_{2}^{\prime},q_{i_{2}}^{\prime},\tau_{2}^{\prime},c_{3}\ldots
c_{k}\eta^{\prime}\rangle\triangleright^{n_{3}}_{\delta}\ldots\triangleright^{n_{k+1}}_{\delta}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\eta^{\prime}\rangle\\\
&\Longleftrightarrow\\\ &\langle\sigma,q,\tau,\xi_{1}c_{1}\xi_{2}c_{2}\ldots
c_{k}\xi_{k+1}\eta^{\prime\prime}\rangle\triangleright^{n_{1}}_{H(\delta)}\langle\sigma_{1},q_{i_{1}},\tau_{1},c_{1}\xi_{2}c_{2}\ldots
c_{k}\xi_{k+1}\eta^{\prime\prime}\rangle\triangleright^{1}_{H(\delta)}\langle\sigma_{1}^{\prime},q_{i_{1}}^{\prime},\tau_{1},\xi_{2}c_{2}\ldots
c_{k}\xi_{k+1}\eta^{\prime\prime}\rangle\land\\\
&\langle\sigma_{1}^{\prime},q_{i_{1}}^{\prime},\tau_{1},\xi_{2}c_{2}\ldots
c_{k}\xi_{k+1}\eta^{\prime\prime}\rangle\triangleright^{n_{2}}_{H(\delta)}\langle\sigma_{2},q_{i_{2}},\tau_{2},c_{2}\ldots
c_{k}\xi_{k+1}\eta^{\prime\prime}\rangle\triangleright^{1}_{H(\delta)}\langle\sigma_{2}^{\prime},q_{i_{2}}^{\prime},\tau_{2}^{\prime},\xi_{3}c_{3}\ldots
c_{k}\xi_{k+1}\eta^{\prime\prime}\rangle\land\\\
&\langle\sigma_{2}^{\prime},q_{i_{2}}^{\prime},\tau_{2}^{\prime},\xi_{3}c_{3}\ldots
c_{k}\eta^{\prime\prime}\rangle\triangleright^{n_{3}}_{H(\delta)}\ldots\triangleright^{n_{k+1}}_{H(\delta)}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\eta^{\prime\prime}\rangle.\end{aligned}$
Intuitively, this holds because it suffices to take the $n_{i}$s as the length
of longest sequence of non-shifting transitions of the on-demand stream
machine and the correspondence can be proven by induction on the number of
steps of each formula in the conjunction. Thus, we can express the sets of the
claim as follows:

$\displaystyle\\{\eta\in\mathbb{B}^{\mathbb{N}}|\exists\eta^{\prime}.\langle\sigma,q,\tau,\eta\rangle\triangleright^{n}_{\delta}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\eta^{\prime}\rangle\\}$
$\displaystyle=\\{\eta\in\mathbb{B}^{\mathbb{N}}|\forall 0\leq
i<k.\eta(i)=c_{i}\rangle\\}$
$\displaystyle\\{\chi\in\mathbb{B}^{\mathbb{N}}|\exists\chi^{\prime}.\langle\sigma,q,\tau,\xi\rangle\triangleright^{n}_{H(\delta)}\langle\sigma^{\prime},q^{\prime},\tau^{\prime},\chi^{\prime}\rangle\\}$
$\displaystyle=\\{\chi\in\mathbb{B}^{\mathbb{N}}|\forall 1\leq i\leq
k.\chi(n_{i}+i)=c_{i}\land\chi(0)=c_{1}\rangle\\}.$

The conclusion comes because both these sets are cylinders with the same
measure. ∎

######  Proposition B.10 (From $\mathcal{POR}$ to $\mathbf{SFP}$).

For any $f:\mathbb{S}^{k}\times\mathbb{B}^{\mathbb{S}}\to\mathbb{S}$ in
$\mathcal{POR}$ there exists a function
$f^{\sharp}:\mathbb{S}^{k}\times\mathbb{B}^{\mathbb{N}}\to\mathbb{S}$ such
that for all $n_{1},\dots,n_{k},m\in\mathbb{S}$,

$\mu\big{(}\\{\eta\in\mathbb{B}^{\mathbb{N}}\mid
f(n_{1},\dots,n_{k},\eta)=m\\}\big{)}=\mu\big{(}\\{\omega\in\mathbb{O}\mid
f^{\sharp}(n_{1},\dots,n_{k},\omega)=m\\}\big{)}.$

###### Proof.

This result is a consequence of Lemma B.7, Lemma B.8, Proposition 10 and Lemma
B.9. ∎

##  Appendix C Proofs from Section 5

###  C.1 The Randomized Algorithm

Let us first describe the randomized algorithm $\mathtt{PZT}$ in more detail:

  1. 1.

If the input $x$ is not the output of a circuit, reject it. Otherwise, let $n$
be its arity, $d$ its degree and $m$ its size. Set $i$ to $1$.

  2. 2.

Check whether $m$ is smaller than some constant value $\varrho\in\mathbb{N}$.

     * •

If so, walk the table $T$ looking for a pair $(x_{j},y_{j})$ where $x_{j}=x$;
set $o_{i}=0$ if $y_{j}=1$, set $o_{i}=1$, otherwise.

     * •

Otherwise, proceed as follows. Choose $r_{1},\ldots,r_{n}$ uniformly and
independently in $\\{0,\ldots,2^{m+3}-1\\}\subseteq\mathbb{N}$. Let $k$ be a
random value in $\\{1,\ldots,2^{2m}\\}\subseteq\mathbb{N}$. Finally, evaluate
the result of $x$, seen as a circuit, on $r_{1},\ldots,r_{n}\mod k$, with
result $o_{i}$.

  3. 3.

If $i<s$, then increase $i$ by $1$ and go back to $2$.

  4. 4.

If for all $i$, $1\leq i\leq s$, $o_{i}=0$ output $\epsilon$; otherwise,
output ${0}$.

Let us now discuss the formula $G$ that represents $\mathtt{PZT}$. To do so,
we introduce a set of basic predicates, which will be employed for the
definition of $G$:

$\displaystyle\mathit{Circ}(x)$ $\displaystyle:=\text{$x$ is the encoding of a
circuit with a single output}$ $\displaystyle\mathit{Eval}(x,k,y,t)$
$\displaystyle:=\text{When fed with inputs encoded by $y$, $x$ produces in
output $t$ modulo $k$}$ $\displaystyle\mathit{NumVar}(x,n)$
$\displaystyle:=\text{$x$ is the encoding of an arithmetic circuit with $n$
variables}$ $\displaystyle\mathit{Degree}(x,d)$ $\displaystyle:=\text{The
degree of the arithmetic circuit encoded by $x$ is $d$}$ $\displaystyle
T(x,y)$
$\displaystyle:=\bigvee_{\overline{x}\in\bigcup_{i=0}^{\varrho}\\{0,1\\}^{i}}\left(x=\overline{x}\land
y=y_{\overline{x}}\right)$ $\displaystyle K(r,z)$ $\displaystyle:=\text{$z$ is
a uniformly chosen random string in $\\{0,1\\}^{|r|}$}.$

All these predicates characterize polytime random functions; for this reason,
we can assume without lack of generality that they are
$\Sigma^{b}_{1}$-formulæ of $\mathcal{RL}$. Using some of these predicates, it
is possible to define a formula $G_{1}$ which executes one evaluation of the
polynomial $x$:
$\begin{aligned} &G_{1}(x,m,n,d,z,y):=\left[m\leq\varrho\land T(x,1)\to
y=0\land T(x,0)\to y=1\right]\lor\Big{[}(m>\varrho)\ \land\\\
&\big{(}\left(y=0\land\exists
z_{0},z_{1}.|z_{0}|=2m\land|z_{1}|=n\cdot(m+3)\land z_{0}\cdot
z_{1}=z\land\exists t\preceq z.\left(\mathit{Eval}(x,z_{0},z_{1},t)\land t\neq
0\right)\right)\lor\\\ &\left(y=1\land\exists
z_{0},z_{1}.|z_{0}|=2m\land|z_{1}|=n\cdot(m+3)\land z_{0}\cdot
z_{1}=z\land\mathit{Eval}(x,z_{0},z_{1},0)\right)\big{)}\Big{]}.\end{aligned}$

######  Remark C.1.

The formula $G_{1}$ is a $\Sigma^{b}_{1}$ predicate of $\mathcal{RL}$ which
characterizes one iteration of the algorithm PZT.

Differently from the original algorithm, the formula $G_{1}$ employs an
additional parameter $z$ as a _source of randomness_ to determine the values
of $r_{i},\ldots,r_{n}$ and $k$. This way, we are able to isolate the
randomization part in a small portion of the formula we are building, i.e.
that one where we determine the value of $z$ by means of the predicate
$\mathtt{Flip}$.

Thanks to this construction, $G_{1}$ is a $\Sigma^{b}_{1}$ formula realizing
some $\mathtt{Flip}$-free $\mathcal{POR}$ function $g_{1}$. We can leverage
this fact to define another $\mathtt{Flip}$-free function
$\iota_{g_{1}}(x,n,d,y,z,i)$ which iterates the function $g_{1}$ $i$ times
with the $i$-th $(n(m+3)+2m)$-long sub-string of $z$ as source of randomness —
i.e. as argument for $g$’s $z$ — and returns $\epsilon$ if and only if all
these executions of $g$ returned $1$, otherwise it returns $0$.

This proves that there is a $\mathtt{Flip}$-free $\Sigma^{b}_{1}$ formula
$G^{v}$ realizing that function provable under ${R}\Sigma^{b}_{1}\text{-NIA}$
— and even $S^{0}_{1}$. A picture of the proof of the existence of $G^{v}$ is
given in Figure 2. Intuitively, the formula $G_{v}$ characterizes steps 2-7 of
the PZT algorithm.

$G_{1}$${G_{v}}$$g_{1}$$\iota_{g_{1}}$Realizability$\mathcal{POR}$
closureRepresentability Figure 2: Summary of the proof of the existence of
${G^{v}}$

In order to define $G$, we will only need to compose $G_{v}$ with another sub-
formula which characterizes the first step of the PZT algorithm. This is quite
simple because we only need to encode the generation of the values of
$d,n,m,z$ and to fix a number of iterations, as we will show in section C.2,
${37m}$ is an appropriate choice. Thus, the $\Sigma^{b}_{1}$ formula $G$ can
be defined as follows:
$\begin{aligned} &G(x,y):=\exists m\preceq
x.|x|=m\land\Big{[}\big{(}(\mathit{Circ}(x)\land\exists n\preceq 2^{m}.\exists
d\preceq 2^{m}.\exists z.|z|={37m}\cdot(n(m+3)+2m)\land\\\
&\mathit{NumVar}(x,n)\land\mathit{Degree}(x,d)\land
K(1^{{37m}\cdot(n(m+3)+2m)},z)\land{G^{v}}(x,m,n,d,y,z,{37m})\big{)}\lor\big{(}\lnot\mathit{Circ}(x)\land
y=0\big{)}\Big{]}.\end{aligned}$

###  C.2 Proving the Error Bound

Within this section, we argument that:

$\mathsf{I\Delta}_{0}+\mathrm{Exp}\vdash\forall x.\forall
y.\mathsf{TwoThirds}[G(x,y)\leftrightarrow H(x,y)],$

which is equivalent to showing that:

$\mathsf{I\Delta}_{0}+\mathrm{Exp}\vdash\forall x.\forall
y.\mathsf{Threshold}[\mathsf{NoFlip}[G](x,y,z)\leftrightarrow H(x,y)].$

In turn, it is possible to obtain a formula equivalent to
$\mathsf{NoFlip}[G](x,y,z)$ by removing the quantification over $z$ and the
randomization its value by means of $K$. Doing so, we are able to obtain an
equivalent claim:

$\displaystyle\mathsf{I\Delta}_{0}+\mathrm{Exp}\vdash$ $\displaystyle\forall
x.\forall y.\exists m,d,n\preceq
1^{|x|}.|x|=m\land\mathit{NumVar}(x,n)\land\mathit{Degree}(x,d)$
$\displaystyle\exists^{\frac{2}{3}2^{{37m}\cdot(n(m+3)+2m)}}z.|z|={37m}\cdot(n(m+3)+2m)\land(G^{v}(x,n,d,z,y)\leftrightarrow
H(x,y)).$

It also is easy to observe $\exists^{\geq h}z.|z|=k\land
P(z)\Leftrightarrow|\\{z\in\mathbb{B}^{k}\mid P(z)\\}|\geq h$. This allows to
replace the threshold quantification with a formula of
$\mathsf{I\Delta}_{0}+\mathrm{Exp}$ measuring the cardinality of some finite
set. Therefore, we can reduce out goal to showing Lemma C.1 using only the
instruments provided by $\mathsf{I\Delta}_{0}+\mathrm{Exp}$:

######  Lemma C.1.

For every encoding of a polynomial circuit $x$, for every $y\in\mathbb{B}$,
whereas $x$ has $n$ variables, size $m$ and degree $d$, it holds that:

$|\\{z\in\mathbb{B}^{{37m}\cdot(n(m+3)+2m)}\mid(G^{v}(x,n,d,z,y)\leftrightarrow
H(x,y))\\}|\geq\frac{2}{3}\cdot 2^{{37m}\cdot(n(m+3)+2m)}.$

Since $G$ and $H$ characterize two decisional functions, the claim of Lemma
C.1 can be restated in the following way:
$\begin{aligned}
|\\{z\in\mathbb{B}^{{37m}\cdot(n(m+3)+2m)}\mid(G^{v}(x,n,d,z,0)\land
H(x,0))\lor(G^{v}(x,n,d,z,\epsilon)\land
H(x,\epsilon))\\}|\geq\frac{2}{3}\cdot
2^{{37m}\cdot(n(m+3)+2m)}.\end{aligned}$
Thus, it is possible Lemma C.1 as a consequence of (${\dagger}$ ‣ 6) and
(${\ddagger}$ ‣ 6) which, respectively, can be stated as Lemmas C.2 and C.3.

######  Lemma C.2 (Claim (${\dagger}$ ‣ 6)).

For every $z\in\mathbb{B}^{{37m}\cdot(n(m+3)+2m)}$, every encoding of a
polynomial circuit $x$, every $y\in\mathbb{B}$, whereas $x$ has $n$ variables,
size $m$ and degree $d$, it holds that $G^{v}(x,n,d,z,0)\to H(x,0)$.

###### Proof.

This result is a consequence of the compatibility of $\bmod k$ with respect to
addition, multiplication ad inverse in $\mathbb{Z}$. Precisely: for every
$n,m,k\in\mathbb{Z}$ with $k\geq 2$, it holds that:

  1. 1.

$(n\odot m)\mod k=\left((n\mod k)\odot(m\mod k)\right)\mod k$ for
$\odot\in\\{+,\cdot\\}$.

  2. 2.

$(-n)\mod k=-(n\mod k)$.

  3. 3.

$n\mod k\neq 0\to n\neq 0$.

These claims are shown as follows:

  1. 1.

In this case, we will only show the case for $+$, that of $\cdot$ is
analogous. The proof goes by induction on the recursion parameter, e.g. $x$.
The case $x=0$ is trivial. For the inductive case, let $x=ak+b$ and $y=ck+d$
for $b,d<k$, the existence and uniqueness of this decomposition can be shown
by induction on $x$. The IH tells that $(x\mod k+y\mod k)\mod k=b+d\mod k$.

$\displaystyle(x+1\mod k+y\mod k)\mod k$ $\displaystyle=(x+1\mod k+d)\mod k$
$\displaystyle=(b+1\mod k+d)\mod k$

Now, if $b<k-1$, then $(b+1\mod k+d)\mod k=b+1+d\mod k=ak+b+1+ck+d\mod
k=x+1+y\mod k$. If $b=k-1$

$\displaystyle(x+1\mod k+y\mod k)\mod k$ $\displaystyle=(d)\mod k$
$\displaystyle=(b+1+ak+ck+d)\mod k$ $\displaystyle=x+1+y\mod k$

  2. 2.

This proof goes by cases on $n$. The case where $n=0$ is trivial. The case
$n+1$ relies on the uniqueness of the decomposition of $n=ak+b$, which allows
us to show that $-((ak+b+1)\mod k)=-((b+1)\mod k)$. If $0\leq b<k-1$, then it
is equal to $-b-1$, otherwise it is equal to $0$. On the other hand,
$(-ak-b-1)\mod k=(-b-1)\mod k$ and still, if $0\leq b<k-1$, then this is equal
to $-b-1$, otherwise it is equal to $0$.

  3. 3.

The counter-nominal is trivial: $n=0\rightarrow n\mod k=0$.

Leveraging points 1 and 2, we show that the evaluation of a polynomial $x$ as
performed by the predicate $\mathit{Eval}$ on input $\vec{r}$ is equal to
$x(\vec{r})\mod k$, the assumption $G^{v}(x,n,d,\vec{r}k,0)$ allows us to
conclude the premise of point 3, thus an application of point 3, allows us to
conclude that $\mathbb{Z}\models p(\vec{x})\neq 0$, by the definition of $H$,
we conclude that $H(x,0)$ holds. ∎

######  Lemma C.3 (Claim (${\ddagger}$ ‣ 6)).

For every encoding of a polynomial circuit $x$, every $y\in\mathbb{B}$,
whereas $x$ has $n$ variables, size $m$ and degree $d$, it holds that:

$|\\{z\in\mathbb{B}^{{37m}\cdot(n(m+3)+2m)}\mid G^{v}(x,n,d,z,\epsilon)\to
H(x,\epsilon)\\}|\geq\frac{2}{3}\cdot 2^{{37m}\cdot(n(m+3)+2m)}.$

###  C.3 Proof of Lemma C.3

Lemma C.3 is shown finding an upper bound to the probability of error of the
algorithm, i.e. to the number of values for $z$ causing
$G^{v}(x,n,d,z,\epsilon)\to H(x,\epsilon)$. Intuitively, there are two
possible causes of error within the algorithm underlying the formula $G$.

  1. 1.

if the outcome of the evaluation of the polynomial on $\vec{r}$ is some value
$y\neq 0$ and $k$ divides $y$, then the algorithm will reject its input even
though $x$ belongs to the language.

  2. 2.

if the values $\vec{r}$ are a solution of the _non-identically zero_
polynomial, then the algorithm will reject $x$, even though it belongs to the
language.

The bound to the first error is found in section C.3.1, while a bound to the
probability of the second error is found in section C.3.2. Lemma C.3 can be
shown combining these results.

####  C.3.1 Estimation of the Error, Case 1

######  Proposition 11 (Argument in [3]).

There is some $\varrho\in\mathbb{N}$ such that for every $m\in\mathbb{N}$
greater than $\varrho$, every $0\leq y<2^{({m+3})\cdot 2^{m}}$:

$|\\{k\in\\{1,\ldots,2^{2m}\\}\mid\\}\mid k\text{ is not \emph{a prime not
dividing} }y\\}|\leq 2^{2m}-\frac{2^{2m}}{16m}$

This probability depends on the range bounding $k$ and on the number of
evaluations taken in exam. The proof of this result relies on the following
observations:

  1. (_a_)

Thanks to the Prime Number Theorem, there is some $m^{\prime}$ such that, for
every $m\geq m^{\prime}$, the number of primes in $\\{1,\ldots,2^{2m}\\}$ is
at least $K=\frac{2^{2m}}{4\cdot 2m}$.

  2. (_b_)

For sufficiently big $m$, the number of primes in $\mathbb{Z}$ dividing $0\leq
y<2^{({m+3})\cdot 2^{m}}$ is smaller than $L=3m\cdot 2^{m}$.

  3. (_c_)

For every $n\in\mathbb{N}$, it holds that $3(2n+201)\leq 2^{n+96}$.

  4. (_d_)

For every $m\geq 100$, said $L$ the number of primes dividing $y$, it holds
that $L\leq\frac{K}{2}=\frac{2^{2m}}{16m}$. This is shown by induction using
(_c_).

As we anticipated, points $(a)$, $(b)$, $(d)$ hold only for sufficiently big
values of $m$. For this reason, we define $\varrho$ as the greatest of these
values.

##### Point (_a_)

We exploit here the fact, proved in [17], that the PNT is provable in
$\mathsf{I\Delta}_{0}+\mathrm{Exp}$; the formulation of the PNT can be
paraphrased as follows:

$\forall x\in\mathbb{N}.\forall q\in\mathbb{Q}^{+}.\exists
a_{x},z_{x}.z_{q}\leq
x\Rightarrow\left|\frac{\pi(x)\log_{a_{x}}^{*}(x)}{x}-1\right|\leq q$

Where $\pi(x)$ is the number of primes in $\\{1,\ldots,x\\}$ and
$\log_{a}^{*}(x)$ is a _good approximation_ of $\log_{2}(x)$, i.e. $\forall
x.\log_{2}(x)\leq 2\log_{a_{x}}^{*}(x)\leq 4\log_{2}(x)$. This can be used to
deduce that:

$z_{q}\leq
x\Rightarrow\frac{x}{\log_{a_{x}}^{*}(x)}\left(1-q\right)\leq\pi(x)\leq\frac{x}{\log_{a_{x}}^{*}(x)}\left(1+q\right),$

Thus, fixing $q=\frac{1}{2}$ we obtain the following claim:

$z_{q}\leq
x\Rightarrow\frac{x}{4\cdot\log_{2}(x)}\leq\frac{x}{2\log_{a_{x}}^{*}(x)}\leq\pi(x)$

We have shown that:

$\forall x.\pi(x)=|\\{p\in\\{1,\ldots,x\\}\mid p\text{ is
prime}\\}|\geq\frac{x}{4\cdot\log_{2}(x)}.$

For sake of readability, we name $\Pi(x)$ the set $\\{p\in\\{1,\ldots,x\\}\mid
p\text{ is prime}\\}$.

##### Point(_b_)

To this aim, it suffices to observe that $y$ is the product of
$q_{1},\ldots,q_{L}$ primes where $L\leq|y|=\log(2^{(m+3)2^{m}})$. This is a
consequence of the following version of the Fundamental Theorem of Arithmetic.

######  Theorem C.4.

$\mathsf{I\Delta}_{0}+\mathrm{Exp}\vdash\forall n\geq
2.\mathit{prime}(n)\lor\exists S,s.\mathit{card}(S,s)\land
s\leq|n|\land\forall q\in S.\mathit{prime}(q)\land q|n$.

###### Proof.

We observe that the predicates $\in,|,\mathit{prime},\mathit{card}$ can be
easily modeled in the language of arithmetic. Then we go by induction on $n$
to show the claim, observing that the formula
$A(n)=\mathit{prime}(n)\lor\exists S,s.\mathit{card}(S,s)\land
s\leq|n|\land\forall q\in S.\mathit{prime}(q)\land q|n$ is $\Delta^{0}_{1}$.
The base case is trivial since $2$ is prime and can be divided only by $2$, so
the cardinality of $S$ is smaller than $|2|$. For the inductive case suppose
that $n+1$ is prime, in this case the claim is trivial, otherwise, if $n+1$ is
not prime, there are $a,b\in\mathbb{N}$, $ab=n+1$, thus we can apply the IH on
$a,b$, building $S$ as the union of $S_{a},S_{b}$. ∎

Thus, $L\leq|y|={(3+m)\cdot 2^{m}}={3\cdot 2^{m}+m\cdot 2^{m}}\leq{3m\cdot
2^{m}}$ — the last step is for $m\geq 1$, and is shown by induction. To sum
up:

$\forall 0\leq y\leq 2^{(m+3)2^{m}}.|\\{p\in\mathbb{Z}\mid q\text{ divides
}y\\}|\leq{3m\cdot 2^{m}}.$

For simplicity’s sake, we omit the proof of $(c)$ and $(d)$, which are
standard by induction.

###### Proof of Proposition 11.

From $(d)$ we can deduce that $|\\{p\in\Pi(2^{2m})\mid p\text{ does not divide
}y\\}|\\\ >\frac{2^{2m}}{4\cdot 2m}$. Thus, the claim is a trivial consequence
of the following observation, which concludes the proof:

${|\\{1,\ldots,2^{2m}-1\\}\setminus\\{p\in\Pi(2^{2m})\mid p\text{ does not
divide }y\\}|}\leq\\\ 2^{2m}-{|\\{p\in\Pi(2^{2m})\mid p\text{ does not divide
}y\\}|}$

∎

####  C.3.2 Estimation of Error, case 2

The goal of this section is to show that for every non-zero $n$-variate
polynomial $p$ of degree $d$ and every set $S\subseteq\mathbb{Z}$, $S$
contains sufficiently many witnesses of the fact that $p$ is a non-zero
polynomial.

######  Remark C.2.

We here implicitly assume an encoding of polynomials as finite strings of
coefficients, so that a unary polynomial $p(x)=\sum_{i=0}^{i<k}a_{i}x^{i}$
translates into (a suitable encoding of) the string
$(a_{0},a_{1},\dots,a_{k-1})$. Observe that the property “$\forall
x.p(x)=q(x)$” is decidable: once $p$ and $q$ are translated into strings of
coefficients it is enough to check equality of these strings. For this reason
we can suppose that all statements of the form “$\mathbb{Z}\models\forall
x.p(x)=q(x)$” or “$\mathbb{Z}\models\exists x.p(x)\neq q(x)$” are encoded via
$\Delta^{0}_{1}$-formulas.

######  Lemma C.5 (Schwartz-Zippel).

For every _$n$ -variate_ polynomial $p$, for every $S\subseteq\mathbb{Z}$,
said $d$ the degree of $p$, it holds that:

${|\\{(x_{1},\ldots,x_{n})\in S^{n}\ |\ \mathbb{Z}\models
p(x_{1},\ldots,x_{n})=0\\}|}\leq d|S|^{n-1}$

The proof of this result is by induction on the number of variables and the
degree of the polynomial $p$. It relies on a weak statement of the Fundamental
Theorem of Algebra, proved below (Corollary 12), stating that each univariate
polynomial has at most $d$ roots in $\mathbb{Z}$, where $d$ is the degree of
the polynomial. We start by defining the notion of non-zero univariate
polynomial:

######  Definition 37.

We say that $p\in\mathsf{POLY}$ is a univariate _irreducible_ polynomial if
and only if it is univariate, and $\mathbb{Z}\models\forall x.p(x)\neq 0$.
Moreover, we say that $p\in\mathsf{POLY}$ is a _non-zero_ polynomial if and
only if $\mathbb{Z}\models\exists x.p(x)\neq 0$.

This notion extends naturally to multivariate polynomials. The first step of
the proof is to show that each univariate polynomial in $\mathbb{Z}$ can be
expressed as the product of $\prod_{i=0}^{i<k}(x-\overline{x}_{i})q(x)$ for
$k$ smaller than the degree of $d$. This result relies itself on the proof of
the correctness of the polynomial division algorithm, in particular on the
following properties:

######  Remark C.3.

  1. 1.

Let $p$ be an univariate polynomial in normal form with coefficients in
$\mathbb{Z}$ and let $\overline{x}$ be a solution of $p$, The division
algorithm applied on $p,(x-\overline{x})$ outputs a polynomial $q$ with no
remainder.

  2. 2.

Let $p$ be an univariate polynomial in normal form with coefficients in
$\mathbb{Z}$ and let $r$ be a non-zero polynomial in normal form with degree
smaller than that of $p$. If $q$ is obtained with remainder $0$ applying the
division algorithm to $p$ and $q$, it holds that $rq=p$.

  3. 3.

The degree of $r=p/q$ plus the degree of $q$ is equal to the degree of $p$.

Although these results may seem very simple, for our purpose it is important
to ensure that they can be established within
$\mathsf{I\Delta}_{0}+\mathrm{Exp}$. This is true, because the algorithm
performing polynomial division is polytime and thus its totality, as well as
its correctness, can be proved in $\mathsf{I\Delta}_{0}+\mathrm{Exp}$.

Now, we want to prove that each uni-variate non-zero polynomial of degree $d$
has at most $d$ roots in $\mathbb{Z}$. We start by showing that it is always
possible to express it as a product of simpler polynomials.

######  Lemma C.6.

For every univariate polynomial $p$, if $p$ has $k$ distinct roots
$\overline{x}_{0},\dots,\overline{x}_{k-1}$, then there is a polynomial $q$
such that $\mathit{deg}(q)=\mathit{deg}(p)-k$ and

$\mathbb{Z}\models\forall x.p(x)=\prod_{i=0}^{i<k}(x-\overline{x}_{i})q(x).$

###### Proof.

We want to show that for all polynomial $p$, degree $d$, natural number $k<d$
and integers $x_{1},\dots,x_{d}$, if $p$ is unary, has degree $d$ and
$\overline{x}_{1},\dots,\overline{x}_{k}$ are distinct roots of $p$, then
there is a polynomial $q$ of degree at most $\mathit{deg}(p)-k$ such that
$p(x)=\prod_{i=0}^{i<k}(x-\overline{x}_{i})q(x)$. Using Remark C.2, this can
be encoded as a formula of the form $\forall p.\forall d.\forall s.C(p,d)$,
where $C(p,d)$ only contains bounded quantifications, and $s$ is a bound on
the values of the roots $\overline{x}_{i}$. We will prove $\forall p.\forall
d.\forall s.C(p,d)$ by induction on $d$:

  * •

If $d=0$, then the claim also holds trivially.

  * •

If $d>0$ and $k=0$, then again the claim holds trivially. If $k>0$, then
polynomial division yields $p(x)\simeq(x-\overline{x}_{k})p^{\prime}(x)$, with
$\mathit{deg}(p^{\prime}(x))=d-1$ and
$\overline{x}_{1},\dots,\overline{x}_{k-1}$ roots of $p^{\prime}(x)$. Then, by
IH, we deduce $C(p^{\prime},d-1)$, that is,
$p^{\prime}(x)=\prod_{i=0}^{i<k-1}(x-\overline{x}_{i})q(x)$, and thus
$p(x)=\prod_{i=0}^{i<k}(x-\overline{x}_{i})q(x)$ as desired.

∎

######  Corollary 12.

For every $S\subseteq\mathbb{Z}$ and for every non-zero univariate polynomial,
it holds that:

$|\\{x\in S\ |\ \mathbb{Z}\models p(x)=0\\}|\leq\mathit{deg}(p).$

###### Proof of Lemma C.5.

The proof is by induction on $n$:

  * •

The claim for $n=1$ coincides with Corollary 12.

  * •

In the general case, we take the normal form of $p$, call that polynomial
$p^{\prime}$. It holds that

$\mathbb{Z}\models\forall\vec{x}.p(\vec{x})=p^{\prime}(\vec{x}),$

then we go by induction on $d$, we can factorize $x_{1}$ from each monomial of
$p$ and show that

$\exists k.\mathbb{Z}\models\forall
x_{1},\ldots,x_{n}.p^{\prime}(x_{1},\ldots,x_{n})=\sum_{i=0}^{k}x_{1}^{i}\cdot
p_{i}(x_{2},\ldots,x_{n})$

Where $p_{k}$ is non-zero. Applying the IH on $d$ to $p_{k}$, we obtain that:

$\\{(x_{2},\ldots,x_{n})\in S^{n-1}\ |\ \mathbb{Z}\models
p_{k}(x_{2},\ldots,x_{n})=0\\}\leq(d-k)|S|^{n-2}$

Fix some $(y_{2},\ldots,y_{n})\in S^{n-1}$ and assume that
$p_{k}(y_{2},\ldots,y_{n})\neq 0$. In this case, the polynomial
$\overline{p}_{y_{2},\ldots,y_{n}}(x):=\sum_{i=0}^{k}x^{i}\cdot
p_{i}(y_{2},\ldots,y_{n})$ is not identically zero because it is a normal form
and a normal form is identically zero if and only if all its coefficients are
different from zero, but the coefficient of $x^{k}$ is different from $0$ for
construction. Thus, we can apply the IH on $n$, showing that:

$\forall(y_{2},\ldots,y_{n})\in S^{n-1}.|\\{x\in
S\mid\mathbb{Z}\models\overline{p}_{y_{2},\ldots,y_{n}}(x)=0\\}|\leq k,$ ($*$)

We continue by observing that

$\forall(y_{2},\ldots,y_{n})\in S^{n-1}.\\{x\in
S\mid\mathbb{Z}\models\overline{p}_{y_{2},\ldots,y_{n}}(x)=0\\}=\\{x\in
S\mid\mathbb{Z}\models p(x,y_{2},\ldots,y_{n})=0\\},$

for the definition of $\overline{p}$. We can conclude that
$\begin{gathered}\\{(x_{1},\ldots,x_{n})\in S^{n}\ |\ \mathbb{Z}\models
p(x_{1},\ldots,x_{n})=0\\}=\\\\[5.59721pt] \\{(x_{1},\ldots,x_{n})\in S^{n}\
|\ \mathbb{Z}\models p(x_{1},\ldots,x_{n})=0\land
p_{k}(x_{2},\ldots,x_{n})=0\\}\cup\\\ \\{(x_{1},\ldots,x_{n})\in S^{n}\ |\
\mathbb{Z}\models p(x_{1},\ldots,x_{n})=0\land p_{k}(x_{2},\ldots,x_{n})\neq
0\\}=\\\\[5.59721pt] \\{(x_{1},\ldots,x_{n})\in S^{n}\ |\ \mathbb{Z}\models
p(x_{1},\ldots,x_{n})=0\land p_{k}(x_{2},\ldots,x_{n})=0\\}\cup\\\
\\{(x_{1},\ldots,x_{n})\in S^{n}\ |\ \mathbb{Z}\models
p(x_{1},\ldots,x_{n})=0\land p_{k}(x_{2},\ldots,x_{n})\neq
0\land\overline{p}_{x_{2},\ldots,x_{n}}(x_{1})=0\\}\subseteq\\\\[5.59721pt]
\\{(x_{1},\ldots,x_{n})\in S^{n}\ |\ \mathbb{Z}\models
p_{k}(x_{2},\ldots,x_{n})=0\\}\cup\\{(x_{1},\ldots,x_{n})\in S^{n}\ |\
\mathbb{Z}\models\overline{p}_{x_{2},\ldots,x_{n}}(x_{1})=0\\}=\\\\[5.59721pt]
S\times\\{(x_{2},\ldots,x_{n})\in S^{n-1}\ |\
\mathbb{Z}\models\overline{p}_{x_{2},\ldots,x_{n}}(x_{1})=0\\}\cup\\{(x_{1},\ldots,x_{n})\in
S^{n}\ |\
\mathbb{Z}\models\overline{p}_{x_{2},\ldots,x_{n}}(x_{1})=0\\}\end{gathered}$
This result can be lifted to sizes, obtaining the claim.

∎

###### Proof of Lemma C.3.

We omit the case for $|x|<\varrho$, since the conclusion is trivial. The claim
is equivalent to the following one:
$\left|\left\\{z=\left(\begin{matrix}x_{1,1}&\ldots&x_{n,1}&k_{1}\\\
x_{1,2}&\ldots&x_{n,2}&k_{2}\\\ \vdots&\vdots&\ddots&\vdots\\\
x_{1,{37m}}&\ldots&x_{n,{37m}}&k_{r}\end{matrix}\right)\in\left(\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\right)^{37m}\mid
G^{v}(p,m,n,d,\epsilon,z,{37m})\land
H(p,0)\right\\}\right|\leq\frac{1}{3}2^{{37m}\cdot(n(m+3)+2m)}$
The set on the left is:
$\left\\{\left(\begin{matrix}x_{1,1}&\ldots&x_{n,1}&k_{1}\\\
x_{1,2}&\ldots&x_{n,2}&k_{2}\\\ \vdots&\vdots&\ddots&\vdots\\\
x_{1,{37m}}&\ldots&x_{n,{37m}}&k_{r}\end{matrix}\right)\in\left(\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\right)^{37m}\mid\\\
\forall 1\leq j\leq 48m.\mathbb{Z}\models
p(\vec{x}_{j})=0\lor(\mathbb{Z}\models p(\vec{x}_{j})\neq 0\land k_{j}\text{
does divide }p(\vec{x}_{j}))\right\\}$
Thus, it is equal to:

$\\{(x_{1},\ldots,x_{n},k)\in\left(\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\right)\mid\\\
\mathbb{Z}\models p(\vec{x})=0\lor(\mathbb{Z}\models p(\vec{x})\neq 0\land
k\text{ does divide }p(\vec{x}))\\}^{37m}\subseteq$
$\big{(}\\{(x_{1},\ldots,x_{n},k)\in\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\mid\mathbb{Z}\models
p(\vec{x})=0\\}\cup\\\
\\{(x_{1},\ldots,x_{n},k)\in\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\mid\mathbb{Z}\models
p(\vec{x})\neq 0\land k\text{ does divide }p(\vec{x})\\}\big{)}^{37m}$

Thus, its size is smaller than:

$\displaystyle\big{(}|$
$\displaystyle\\{(x_{1},\ldots,x_{n},k)\in\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\mid\mathbb{Z}\models
p(\vec{x})=0\\}|+$ $\displaystyle|$
$\displaystyle\\{(x_{1},\ldots,x_{n},k)\in\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\mid\mathbb{Z}\models
p(\vec{x})\neq 0\land k\text{ does divide }p(\vec{x})\\}|\big{)}^{37m}.$

Our goal is equivalent to showing the ratio between that value and
$2^{{37m}\cdot(n(m+3)+2m)}$ is smaller than $\frac{1}{3}$. Which, in turn,
resolves to:
$\begin{aligned}
\Bigg{(}&\frac{|\\{(x_{1},\ldots,x_{n},k)\in\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\mid\mathbb{Z}\models
p(\vec{x})=0\\}|}{2^{n(m+3)+2m}}+\\\
&\frac{|\\{(x_{1},\ldots,x_{n},k)\in\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\mid\mathbb{Z}\models
p(\vec{x})\neq 0\land k\text{ does divide
}p(\vec{x})\\}|}{2^{n(m+3)+2m}}\Bigg{)}^{37m}\leq\frac{1}{3}.\end{aligned}$
From Lemma C.5 and point $(e)$, it is smaller than:
$\begin{aligned} \Bigg{(}&\frac{2^{m}\cdot 2^{(m+3)\cdot(n-1)}\cdot
2^{2m}}{2^{n(m+3)+2m}}+\\\
&\frac{|\\{(x_{1},\ldots,x_{n},k)\in\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\mid\mathbb{Z}\models
p(\vec{x})\neq 0\land k\text{ does divide
}p(\vec{x})\\}|}{2^{n(m+3)+2m}}\Bigg{)}^{37m}=\\\
\Bigg{(}&\frac{1}{8}-h+\frac{|\\{(x_{1},\ldots,x_{n},k)\in\\{0,2^{m+3}-1\\}^{n}\times\\{1,2^{2m}\\}\mid\mathbb{Z}\models
p(\vec{x})\neq 0\land k\text{ does divide
}p(\vec{x})\\}|}{2^{n(m+3)+2m}}\Bigg{)}^{37m}\leq\end{aligned}$
Applying Proposition 11, we can find an upper bound to this value, which is:

$\displaystyle\Bigg{(}$
$\displaystyle\frac{1}{8}-h+\left(1-\frac{1}{8}+h\right)\frac{2^{n(m+3)+2m}-\frac{2^{n(m+3)+2m}}{16m}}{2^{n(m+3)+2m}}d\Bigg{)}^{37m}=$
$\displaystyle\Bigg{(}$
$\displaystyle\frac{1}{8}-h+\left(\frac{7}{8}+h\right)\frac{2^{n(m+3)+2m}-\frac{2^{n(m+3)+2m}}{16m}}{2^{n(m+3)+2m}}\Bigg{)}^{37m}=$
$\displaystyle\Bigg{(}$
$\displaystyle\frac{1}{8}-h+\left(\frac{7}{8}+h\right)\left(1-\frac{1}{16m}\right)\Bigg{)}^{37m}=\Bigg{(}\frac{1}{8}-h+\frac{7}{8}-\frac{7}{8\cdot
16m}+h-\frac{h}{16m}\Bigg{)}^{37m}=$ $\displaystyle\Bigg{(}$ $\displaystyle
1-\frac{7}{8\cdot
16m}-\frac{h}{16m}\Bigg{)}^{37m}=\Bigg{(}1-\frac{1}{16m}\left(\frac{7}{8}+h\right)\Bigg{)}^{37m}\leq\Bigg{(}1-\frac{1}{\frac{8}{7}16m}\Bigg{)}^{37m}\leq$
$\displaystyle\leq\Bigg{(}$ $\displaystyle
1-\frac{1}{\frac{8}{7}16m}\Bigg{)}^{{\frac{8}{7}16m}}\cdot\Bigg{(}1-\frac{1}{\frac{8}{7}16m}\Bigg{)}^{{\frac{8}{7}16m}}\leq\frac{1}{4}$

The very last observation is a consequence that $\forall n\geq
2.\left(1+\frac{1}{n}\right)^{n}\geq 2$. This, in turn, is done expanding the
binomial $\left(1+\frac{1}{n}\right)^{n}$ and obtaining:

$\displaystyle\left(1+\frac{1}{n}\right)^{n}$
$\displaystyle=\sum_{k=0}^{n}\frac{n!}{(n-k)!k!}\frac{1}{n^{k}}=\sum_{k=0}^{n}\frac{1}{k!}\prod_{i=1}^{k-1}\left(1-\frac{i}{n^{k}}\right)=1+1+\sum_{k=2}^{n}\frac{1}{k!}\prod_{i=1}^{k-1}\left(1-\frac{i}{n^{k}}\right)$

Where the derivation is justified by:

  * •

The binomial expansion, namely: $\forall
a,b,n.(a+b)^{n}=\sum_{k=0}^{n}\frac{n!}{k!(n-k)!}a^{n-k}b^{k}$. The proof is
by induction on $n$. We will omit the details, which can be found in many
text-books.

  * •

$\forall k.k!\geq 2^{k}$. The proof is by induction. The base case is trivial,
the inductive one is done as follows: $(k+1)!=k!(k+1)\geq 2^{k}(k+1)$. Now we
go by cases on $k$: if it is $0$, the claim is trivial, otherwise we observe
that $(k+1)\geq 2$ and thus $2^{k}(k+1)\geq 2^{k+1}$.

  * •

$\forall n.\sum_{k=1}^{n}2^{-k}=1-2^{-n}$, which is shown by induction on $n$.
The base case is trivial. The inductive one is done as
follows:$\sum_{k=1}^{n+1}2^{-k}=\sum_{k=1}^{n}2^{-k}+2^{-n-1}=1-2^{-n}+2^{-n-1}=1-2^{-n-1}$.

These proof are completely syntactic thus, modulo an encoding for rational
numbers and for their operations, they can be done in $\mathsf{PA}$ without
much effort. The proof proceeds observing that

$\left(1+\frac{1}{n}\right)^{n}=\left(1+\frac{1}{n}\right)^{-1\cdot-1\cdot
n}=\left(\frac{n}{n+1}\right)^{-n}=\left(1-\frac{1}{n}\right)^{-n}.$

Therefore, $\forall n\geq 4.\left(1-\frac{1}{n}\right)^{n}\leq\frac{1}{2}$,
and so:

$\Bigg{(}1-\frac{1}{\frac{8}{7}16m}\Bigg{)}^{{\frac{8}{7}16m}}\cdot\Bigg{(}1-\frac{1}{\frac{8}{7}16m}\Bigg{)}^{{\frac{8}{7}16m}}\leq\frac{1}{4}.$

∎

As we have shown, even last result can be proved in $\mathsf{PA}$, using an
encoding of finite sets and standard arithmetic on $\mathbb{N}$.

###  C.4 Closure of $\mathbf{BPP}_{\mathsf{T}}$ under polytime reduction

We assume $\mathsf{T}$ is any theory containing
${R}\Sigma^{b}_{1}\text{-NIA}+\mathrm{Exp}$. The statement of Proposition 1
can be given more precisely as:

######  Proposition 12.

For every language $L\in\mathbf{BPP}_{\mathsf{T}}$ and every language
$M\in\mathbb{B}^{*}$, if there is an polytime function
$r_{M,L}:\mathbb{S}\longrightarrow\mathbb{S}$, such that for every string in
$\sigma\in\mathbb{S}$, $x\in M\leftrightarrow r(x)\in L$, then $M$ is in
$\mathbf{BPP}_{\mathsf{T}}$.

###### Proof.

Assume that $L\in\mathbf{BPP}_{\mathsf{T}}$, and let $G_{L}$ be the
$\Sigma^{b}_{1}$ $\mathcal{RL}$ formula characterizing $L$ as required in
Definition 10. Since $r_{M,L}$ is poly-time, there is a $\Sigma^{b}_{1}$
$\mathtt{Flip}$-free formula of $\mathcal{RL}$ $R$ characterizing $r_{M,L}$ as
well. This has a consequence that the formula $C(x,y):=\exists w\leq
t(x).R(x,w)\land G_{L}(w,y)$ characterizes the composition of the reduction
$r_{M,L}$ and the function $\chi_{L}$. The function $C(x,y)$ is still a
$\Sigma^{b}_{1}$ formula, and characterizes a function deciding $M$ due to the
hypothesis on the correctness of the reduction $r_{M,L}$. Form this conclusion
and $\mathrm{Lang}(G_{L})=L$, we deduce $\mathrm{Lang}(C)=M$, we only need to
show point (2) of Definition 10 for $C$:

$\displaystyle\mathsf{T}$ $\displaystyle\vdash\forall
x.\exists!y.\mathsf{TwoThirds}[C]$ $\displaystyle\mathsf{T}$
$\displaystyle\vdash\forall x.\exists!y.\mathsf{TwoThirds}[\exists w\leq
t(x).R(x,w)\land G_{L}(w,y)]$ $\displaystyle\mathsf{T}$
$\displaystyle\vdash\forall
x.\exists!y.\mathsf{Threshold}[\mathsf{NoFlip}[\exists w\leq t(x).R(x,w)\land
G_{L}(w,y)]]$ $\displaystyle\mathsf{T}$ $\displaystyle\vdash\forall x.\exists
w\leq
t(x).R(x,w)\land\exists!y.\mathsf{Threshold}[\mathsf{NoFlip}[G_{L}(w,y)]]$

This is a consequence of a $\Sigma^{b}_{1}$ $\mathtt{Flip}$-free formula of
$\mathcal{RL}$ and the hypothesis on $G_{L}$. ∎