Selection products and restricted bar recursion

For $J_{R}X=(X\to R)\to X$, the applied binary product is The simple explicitly controlled product has the complete equations $$c={\epsilon }_n(\lambda x.q(x\ast {\mathsf{eps}}_{n+1}^{,l}(\epsilon )(q_x))),q_x(\beta )=q(x\ast \beta ).$$ For history-sensitive selectors, replace $n$ by the history $s$, use the test , and recurse at $s\ast c$; these are the dependent EPS equations.

Two stream operations must remain distinct. Shifting prefix concatenation is whereas prefix-preserving overwrite is restricted Spector recursion is $$c={\delta }_s(\lambda x.{\mathsf{SBR}}_{s\ast x}^{\omega }(\delta )),{\delta }_s:(X\to X^{\mathbb{N}})\to X.$$ The totality theorem assumes the decidable bar-induction principle $$\frac{\begin{array}{c}\mathrm{\forall }\alpha \mathrm{\exists }n.D([\alpha ](n))\mathrm{\forall }s.(D(s)\vee \mathrm{\neg }D(s)),\\ \mathrm{\forall }s.(D(s)\to Q(s))\mathrm{\forall }s.((\mathrm{\forall }x.Q(s\ast x))\to Q(s))\end{array}}{Q([])}.$$ Call this principle ${\mathrm{BI}}_{\mathrm{dec}}$. It is distinct from the relativized scheme ${\mathrm{BI}}_{\mathrm{rel}}$ used in the sourced reverse comparison. For the SBR proof, $D(s)$ is , and $Q(s)$ states totality of the recursive call.