appendix sectionnotation

Selection products and bar recursion

notation	meaning	owner
notation	meaning	owner
$J_{R} X = (X \to R) \to X$ , $P_{m} (\vec{ε})$	selection-function type and right-associated finite product	chapter 67
$[α] (n)$ , $s * x$ , $s * α$	stream prefix, list append, and shifting stream prefix	chapter 67
$put (s, α)$	prefix-preserving stream update, which does not shift indices	chapter 67
${eps}_{n}^{, l}$ , ${EPS}_{s}^{, l}$	simple and history-sensitive explicitly controlled products	chapter 67
${SBR}_{s}^{ω}$ , ${BI}_{dec}$ , ${BI}_{rel}$ , $SPEC$	restricted Spector recursion, decidable and relativized bar induction, and Spector’s stopping condition	chapter 67
${DNS}_{N}$ , ${cAC}_{N}$	countable double-negation shift and negatively translated countable choice	chapter 67