Fixed arrow OCF

The arrow OCF has some issues, so I give a fixed version.

Let

• \(B_0(\beta)=\{0,\omega_1,\omega_2,\ldots,\omega_\omega\}\).
• \(B_{n+1}(\beta)=\{x,x+y,xy,x\uparrow^zy:x,y,z\in B_n(\beta)\land z<\beta\}\).
• \(B(\beta)=\beta\cap\bigcup_{n<\omega} B_n(\beta)\).

and

• \(C_0(\alpha,\beta)=\alpha+1\).
• \(C_{\epsilon+1}(\alpha,\beta)=\{x,x+y,xy,x\uparrow^zy:x,y\in C_\epsilon(\alpha,\beta)\land z\in B(\beta)\}\).
• If \(\epsilon\) is a limit, \(C_\epsilon(\alpha,\beta)=S\cup\operatorname{limits}(S)\), where \(S=\bigcup_{\zeta<\epsilon}C_\zeta(\alpha,\beta)\).

Then \(\alpha\uparrow^0\beta=1\) and \(\alpha\uparrow^{1+\gamma}\beta=\sup(C_\gamma(\alpha,\beta))\).