10,969 Pages

This is an English translation of my Japanese blog post. I created an ordinal notation associated to extended Buchholz's OCF. It is important, because the existence of an ordinal notation, which interprets the $$\in$$-relation into a recursive relation on formal strings, ensures the recursiveness of the system of fundamental sequences on the notation given as the pull-back of the canonical system of fundamental sequences and the computability of large numbers defined by Denis Maksudov using fast-growing hierarchy and extended Buchholz's OCF. For the issue on the computability of large numbers defined by fast-growing hierarchy and OCFs, see the following:

# Convention

I use ellipses only in three ways. One is the abbreviation $$A_1,\ldots,A_k$$ of an array of length $$k > 1$$ whose $$(i+1)$$-th entry is denoted by $$A_{i+1}$$ for any $$i \in \mathbb{N}$$ smaller than $$k$$, another one is the abbreviation $$A_2,\ldots,A_k$$ of an array of length $$k-1 > 1$$ whose $$(i+1)$$-th entry is denoted by $$A_{i+2}$$ for any $$i \in \mathbb{N}$$ smaller than $$k-1$$, and the other one is the abbreviation $$(\underbrace{c,\ldots,c}_{k})$$ of a constant array of length $$k > 1$$ with entry $$c$$. Therefore they do not cause any ambiguity.

I define sets $$T$$ and $$PT$$ of formal strings consisting of $$($$, $$)$$, $$\langle$$, $$\rangle$$, and commas in the following recursive way:

1. $$() \in T$$.
2. For any $$X_1,X_2 \in T$$, $$\langle X_1, X_2 \rangle \in T$$ and $$\langle X_1, X_2 \rangle \in PT$$.
3. For any $$X_1, \ldots, X_m \in PT$$ ($$2 \leq m < \infty$$), $$(X_1, \ldots, X_m) \in T$$.

I will define an ordinal notation $$OT$$ whose underlying subset is a recursive subset of $$T$$. In $$OT$$, $$()$$ plays a role of $$0$$, $$\langle \ , \ \rangle$$ plays a role of extended Buchholz's OCF, and $$( \ , \ldots, \ )$$ plays a role of the addition.

I denote by $$\underline{0} \in T$$ the formal strings $$()$$, by $$\underline{1} \in T$$ the formal strings $$\langle \underline{0}, \underline{0} \rangle$$, by $$\underline{n} \in T$$ the formal strings $$(\underbrace{\underline{1}, \ldots, \underline{1}}_{n})$$ for each $$n \in \mathbb{N}$$ greater than $$1$$, and by $$\underline{\omega} \in T$$ the formal strings $$\langle \underline{0}, \underline{1} \rangle$$.

# Ordering

For an $$(X,Y) \in T^2$$, I define the recursive $$2$$-ary relation $$X<Y$$ in the following recursive way:

1. If $$X=\underline{0}$$, then $$X<Y$$ is equivalent to $$Y \neq \underline{0}$$.
2. Suppose $$X = \langle X_1, X_2 \rangle$$ for some $$X_1,X_2 \in T$$.
1. If $$Y=\underline{0}$$, then $$X<Y$$ is false.
2. Suppose $$Y = \langle Y_1, Y_2 \rangle$$ for some $$Y_1,Y_2 \in T$$.
1. If $$X_1=Y_1$$, then $$X<Y$$ is equivalent to $$X_2<Y_2$$.
2. If $$X_1 \neq Y_1$$, then $$X<Y$$ is equivalent to $$X_1<Y_1$$.
3. If $$Y=(Y_1, \ldots, Y_{m'})$$ for some $$Y_1,\ldots,Y_{m'} \in PT$$ ($$2 \leq m' < \infty$$), then $$X<Y$$ is equivalent to $$X=Y_1$$ or $$X<Y_1$$.
3. Suppose $$X=(X_1, \ldots, X_m)$$ for some $$X_1,\ldots,X_m \in PT$$ ($$2 \leq m < \infty$$).
1. If $$Y=\underline{0}$$, then $$X<Y$$ is false.
2. If $$Y = \langle Y_1, Y_2 \rangle$$ for some $$Y_1,Y_2 \in T$$, then $$X<Y$$ is equivalent to $$X_1<Y$$.
3. Suppose $$Y=(Y_1, \ldots, Y_{m'})$$ for some $$Y_1,\ldots,Y_{m'} \in PT$$ ($$2 \leq m' < \infty$$).
1. Suppose $$X_1=Y_1$$.
1. If $$m = 2$$ and $$m' = 2$$, then $$X<Y$$ is equivalent to $$X_2<Y_2$$.
2. If $$m = 2$$ and $$m' > 2$$, then $$X<Y$$ is equivalent to $$X_2<(Y_2,\ldots,Y_{m'})$$.
3. If $$m > 2$$ and $$m' = 2$$, then $$X<Y$$ is equivalent to $$(X_2,\ldots,X_m)<Y_2$$.
4. If $$m > 2$$ and $$m' > 2$$, then $$X<Y$$ is equivalent to $$(X_2, \ldots, X_m)<(Y_2, \ldots, Y_{m'})$$.
2. If $$X_1 \neq Y_1$$, then $$X<Y$$ is equivalent to $$X_1<Y_1$$.

I note that the relation $$<$$ itself is not a strict well-ordering, but is a total ordering. I abbreviate "$$X<Y$$ or $$X=Y$$" to $$X \leq Y$$.

# Fundamental Sequences

I define total recursive maps \begin{eqnarray*} \textrm{dom} \colon T & \to & T \\ X & \mapsto & \textrm{dom}(X) \\ & & \\ [ \ ] \colon T \times T & \to & T \\ (X,Y) & \mapsto & X[Y] \end{eqnarray*} in the following recursive way:

1. If $$X = \underline{0}$$, then $$\textrm{dom}(X) = \underline{0}$$ and $$X[Y] = \underline{0}$$.
2. Suppose $$X = \langle X_1, X_2 \rangle$$ for some $$X_1,X_2 \in T$$.
1. Suppose $$\textrm{dom}(X_2) = \underline{0}$$.
1. If $$\textrm{dom}(X_1) = \underline{0}$$, then $$\textrm{dom}(X) = X$$ and $$X[Y] = \underline{0}$$.
2. If $$\textrm{dom}(X_1) = \underline{1}$$, then $$\textrm{dom}(X) = X$$ and $$X[Y]=Y$$.
3. If $$\textrm{dom}(X_1) \notin \{\underline{0},\underline{1}\}$$, then $$\textrm{dom}(X) = \textrm{dom}(X_1)$$ and $$X[Y] = \langle X_1[Y] , \underline{0} \rangle$$.
2. If $$\textrm{dom}(X_2) = \underline{1}$$, then $$\textrm{dom}(X) = \underline{\omega}$$.
1. If $$Y = \underline{1}$$, then $$X[Y] = \langle X_1, X_2[\underline{0}] \rangle$$.
2. If $$Y = \underline{k}$$ ($$2 \leq k < \infty$$), then $$X[Y] = (\underbrace{\langle X_1, X_2[\underline{0}] \rangle, \ldots, \langle X_1, X_2[\underline{0}] \rangle}_{k})$$.
3. Otherwise, then $$X[Y] = \underline{0}$$.
3. If $$\textrm{dom}(X_2) = \underline{\omega}$$, then $$\textrm{dom}(X) = \underline{\omega}$$ and $$X[Y] = \langle X_1 , X_2[Y] \rangle$$.
4. Suppose $$\textrm{dom}(X_2) \notin \{\underline{0},\underline{1},\underline{\omega}\}$$.
1. If $$\textrm{dom}(X_2) < X$$, then $$\textrm{dom}(X) = \textrm{dom}(X_2)$$, and $$X[Y] = \langle X_1 , X_2[Y] \rangle$$.
2. Otherwise, $$\textrm{dom}(X) = \underline{\omega}$$.
1. Take a unique $$Z \in T$$ such that $$\textrm{dom}(X_2) = \langle Z, \underline{0} \rangle$$.
2. If $$Y = \underline{h}$$ ($$1 \leq h < \infty$$) and $$X[Y[\underline{0}]] = \langle X_1, \Gamma \rangle$$ for a unique $$\Gamma \in T$$, then $$X[Y]= \langle X_1, X_2[\langle Z[\underline{0}], \Gamma \rangle] \rangle$$.
3. Otherwise, $$X[Y] = \langle X_1, X_2[\langle Z[\underline{0}], \underline{0} \rangle] \rangle$$.
3. If $$X = (X_1, \ldots,X_m)$$ for some $$X_1,\ldots,X_m \in PT$$ ($$2 \leq m < \infty$$), $$\textrm{dom}(X)=\textrm{dom}(X_m)$$.
1. If $$X_m[Y] = \underline{0}$$ and $$m = 2$$, then $$X[Y]=X_1$$.
2. If $$X_m[Y] = \underline{0}$$ and $$m > 2$$, then $$X[Y]=(X_1, \ldots, X_{m-1})$$.
3. If $$X_m[Y] \in PT$$, then $$X[Y]=(X_1, \ldots, X_{m-1},X_m[Y])$$.
4. $$X_m[Y] = (Z_1, \ldots, Z_{m'})$$ for some $$Z_1, \ldots, Z_{m'} \in PT$$ ($$2 \leq m' < \infty$$), then $$X[Y]=(X_1, \ldots, X_{m-1}, Z_1, \ldots, Z_{m'})$$.

I will construct a resursive subset $$OT \subset T$$ of standard forms closed under $$\{[\underline{n}] \mid n \in \mathbb{N}\}$$ such that $$[ \ ]$$ restricted to $$\{X \in OT \mid X < \langle \underline{1}, \underline{0} \rangle\} \times \{\underline{n} \mid n \in \mathbb{N}\}$$ forms a recursive system of fundamental sequences with respect to $$<$$.

# Standard Form

For an $$(X,Y,Z) \in T^3$$, I define a recursive $$3$$-ary relation $$G(X,Y) \triangleleft Z$$ in the following recursive way:

1. If $$Y = \underline{0}$$, then $$G(X,Y) \triangleleft Z$$ is true.
2. Suppose $$Y = \langle W_1, W_2 \rangle$$ for some $$W_1,W_2 \in T$$.
1. If $$X \leq W_1$$, then $$G(X,Y) \triangleleft Z$$ is equivalent to $$W_2 < Z$$, $$G(X,W_1) \triangleleft Z$$, and $$G(X,W_2) \triangleleft Z$$.
2. If $$W_1 < X$$, then $$G(X,Y) \triangleleft Z$$ is true.
3. If $$Y = (W_1,\ldots,W_{m'})$$ for some $$W_1,\ldots,W_{m'} \in PT$$ ($$2 \leq m' < \infty$$), then $$G(X,Y) \triangleleft Z$$ is equivalent to $$G(X,W_{i+1}) \triangleleft Z$$ for any $$i \in \mathbb{N}$$ smaller than $$m'$$.

I define a recursive subset $$OT \subset T$$ in the following recursive way:

1. $$\underline{0} \in OT$$.
2. For any $$X_1,X_2 \in T$$, $$\langle X_1, X_2 \rangle \in OT$$ is equivalent to $$X_1 \in OT$$, $$X_2 \in OT$$, and $$G(X_1,X_2) \triangleleft X_2$$.
3. For any $$X_1, \ldots, X_m \in PT$$ ($$2 \leq m < \infty$$), $$(X_1, \ldots, X_m) \in OT$$ is equivalent to $$X_{i+1} \in OT$$ for any $$i \in \mathbb{N}$$ smaller than $$m$$ and $$X_{i+2} \leq X_{i+1}$$ for any $$i \in \mathbb{N}$$ smaller than $$m-1$$.

I denote by $$\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}}$$ the least $$\Omega$$ fixed point. I define a map \begin{eqnarray*} o \colon T & \to & \Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}} \\ X & \mapsto & o(X) \end{eqnarray*} in the following inductive way:

1. If $$X = \underline{0}$$, then $$o(X) = 0$$.
2. If $$X = \langle Y_1, Y_2 \rangle$$ for some $$Y_1,Y_2 \in T$$, then $$o(X) = \psi_{o(Y_1)}(o(Y_2))$$, where $$\psi$$ is extended Buchholz's OCF.
3. If $$X = (Y_1,\ldots,Y_m)$$ for some $$Y_1,\ldots,Y_m \in PT$$ ($$2 \leq m < \infty$$), then $$o(X) = \sum_{i=1}^{m} o(Y_i)$$, where $$\sum$$ denotes the ordered sum.

By the construction, $$(OT,<)$$ forms an ordinal notation, and the restriction of $$o$$ gives isomorphisms \begin{eqnarray*} (OT,<) & \to & (C_0(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}}),\in) \\ (\{X \in OT \mid X < \langle \underline{1}, \underline{0} \rangle\},<) & \to & (C_0(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}}) \cap \Omega,\in) \end{eqnarray*} of strictly well-ordered sets.

# FGH

I define a total recursive map \begin{eqnarray*} f \colon OT \times \mathbb{N} & \to & \mathbb{N} \\ (X,n) & \mapsto & f_X(n) \end{eqnarray*} in the following recursive way:

1. If $$\textrm{dom}(X) = \underline{0}$$, then $$f_X(n) = n+1$$.
2. If $$\textrm{dom}(X) = \underline{1}$$, then $$f_X(n) = f_{X[\underline{0}]}^n(n)$$.
3. Otherwise, $$f_X(n) = f_{X[\underline{n}]}(n)$$.

For an $$n \in \mathbb{N}$$, I define an $$X_n \in OT$$ in the following recursive way:

1. If $$n = 0$$, then $$X_n = \underline{0}$$.
2. If $$n > 0$$, then $$X_n = \langle X_{n-1} , \underline{0} \rangle$$.

The totality of $$f$$ immediately follows from the well-foundedness of $$(OT,<)$$ and the fact that the restriction of $$[ \ ]$$ to $$OT \times \{\underline{n} \mid n \in \mathbb{N}\}$$ forms a recursive system of fundamental sequences. By the construction, the total computable function \begin{eqnarray*} F \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & f_{\langle \underline{0}, X_n \rangle}(n) \end{eqnarray*} precisely coincides with $$f_{\psi_0(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}})}(n)$$ in FGH with respect to extended Buchholz's OCF and the canonical fundamental sequences.

# Demonstration

I abbreviate $$f_X$$ to $$X$$ for each $$X \in OT$$. I compute $$F(0),F(1),F(2),\ldots$$.

\begin{eqnarray*} F(0) & = & \langle \underline{0}, X_0 \rangle(0) \\ & = & \langle \underline{0}, \underline{0} \rangle(0) \\ & = & \underline{1}(0) \\ & = & \underline{0}^0(0) \\ & = & 0 \\ & & \\ F(1) & = & \langle \underline{0}, X_1 \rangle(1) \\ & = & \langle \underline{0}, \langle X_0 , \underline{0} \rangle \rangle(1) \\ & = & \langle \underline{0}, \langle \underline{0} , \underline{0} \rangle \rangle(1) \\ & = & \langle \underline{0}, \underline{1} \rangle(1) \\ & = & [\langle \underline{0}, \underline{1} \rangle|\underline{1}](1) \\ & = & (\langle \underline{0}, \underline{0} \rangle)(1) \\ & = & (\underline{1})(1) \\ & = & \underline{0}^1(1) \\ & = & 1+1 \\ & = & 2 \\ & & \\ F(2) & = & \langle \underline{0}, X_2 \rangle(2) \\ & = & \langle \underline{0}, \langle X_1, \underline{0} \rangle \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{1}, \underline{0} \rangle \rangle(2) \\ & = & [\langle \underline{0}, \langle \underline{1}, \underline{0} \rangle \rangle|\underline{2}](2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, \langle \underline{0}, \underline{0} \rangle \rangle] \rangle] \rangle(2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, \underline{0} \rangle] \rangle] \rangle] \rangle(2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\underline{1}] \rangle] \rangle] \rangle(2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, \underline{1} \rangle] \rangle] \rangle(2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, \langle \underline{0}, \underline{1} \rangle \rangle] \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, \langle \underline{0}, \underline{1} \rangle \rangle \rangle(2) \\ & = & [\langle \underline{0}, \langle \underline{0}, \langle \underline{0}, \underline{1} \rangle \rangle \rangle|\underline{2}](2) \\ & = & \langle \underline{0}, [\langle \underline{0}, \langle \underline{0}, \underline{1} \rangle \rangle|\underline{2}] \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, [\langle \underline{0}, \underline{1} \rangle|\underline{2}] \rangle \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, (\langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle) \rangle \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, (\underline{1},\underline{1}) \rangle \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, \underline{2} \rangle \rangle(2) \\ & = & [\langle \underline{0}, \langle \underline{0}, \underline{2} \rangle \rangle|\underline{2}](2) \\ & = & \langle \underline{0}, [\langle \underline{0}, \underline{2} \rangle|\underline{2}] \rangle(2) \\ & = & \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \langle \underline{0}, \underline{1} \rangle) \rangle(2) \\ & = & [\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \langle \underline{0}, \underline{1} \rangle) \rangle|\underline{2}](2) \\ & = & \langle \underline{0}, [(\langle \underline{0}, \underline{1} \rangle, \langle \underline{0}, \underline{1} \rangle)|\underline{2}] \rangle(2) \\ & = & \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle) \rangle(2) \\ & = & \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}, \underline{1}) \rangle(2) \\ & = & [\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}, \underline{1}) \rangle|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle)(2) \\ & = & [(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle)(2) \\ & = & [(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, [\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle|\underline{2}])(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, [(\langle \underline{0}, \underline{1} \rangle)|\underline{2}] \rangle)(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle) \rangle)(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1},\underline{1}) \rangle)(2) \\ & = & [(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1},\underline{1}) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, [\langle \underline{0}, (\underline{1},\underline{1}) \rangle|\underline{2}])(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(2) \\ & = & [(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \langle \underline{0}, (\underline{1}) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, [\langle \underline{0}, (\underline{1}) \rangle|\underline{2}])(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle)(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1}, \underline{1})(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})^2(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)^2(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)[(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, [\langle \underline{0}, (\underline{1}) \rangle|\underline{2}])(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle)(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \underline{1}, \underline{1})(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \underline{1})^2(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle)^2(2) \\ & = & \cdots \end{eqnarray*}

Community content is available under CC-BY-SA unless otherwise noted.