Ordinal Notation Associated to Extended Buchholz's OCF

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:

1. New Issue on Traditional Analyses
2. Googological Open Problems on OCFs#Ordinal Notation
3. Relation between an OCF and an Ordinal Notation%Caution

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*}