(2021-06-18) 東方巨大数

集合 \( T \) を次のように定義する。

1. \( 0 \in T \)
2. \( a \in T \land b \in T \longrightarrow \left( a + b \right) \in T \)
3. \( 1 \in T \)
4. \( a \in T \land b \in T \longrightarrow {I}_{a} \! \left( b \right) \in T \)
5. \( a \in T \land b \in T \longrightarrow {\psi}_{a} \! \left( b \right) \in T \)

\( t \in T \) に対して、 \( \left| t \right| \in T \) を次のように定義する。

1. \( t \) で場合分けする。
   1. \( t = 0 \) である。
      1. \( \left| 0 \right| = 0 \) である。
   2. \( {a}_{t} \in T \) と \( {b}_{t} \in T \) が存在して、 \( t = {a}_{t} + {b}_{t} \) である。
      1. \( {a}_{t} \) で場合分けする。
         1. \( {a}_{t} = 0 \) である。
            1. \( \left| 0 + {b}_{t} \right| = \left| {b}_{t} \right| \) である。
         2. \( {a}_{{a}_{t}} \in T \) と \( {b}_{{a}_{t}} \in T \) が存在して、 \( {a}_{t} = {a}_{{a}_{t}} + {b}_{{a}_{t}} \) である。
            1. \( \left| \left( {a}_{{a}_{t}} + {b}_{{a}_{t}} \right) + {b}_{t} \right| = \left| {a}_{{a}_{t}} + \left( {b}_{{a}_{t}} + {b}_{t} \right) \right| \) である。
         3. \( {a}_{t} = 1 \) である。
            1. \( {\left| 1 \right|}_{\! 1} \) で場合分けする。
               1. \( {\left| 1 \right|}_{\! 1} = ( ) \) である。
                  1. \( \left| {b}_{t} \right| \) で場合分けする。
                     1. \( \left| {b}_{t} \right| < {\psi}_{{I}_{1} \left( 0 \right)} \! \left( 0 \right) \) である。
                        1. \( \left| 1 + {b}_{t} \right| = 1 + \left| {b}_{t} \right| \) である。
                     2. \( \left| {b}_{t} \right| \geq {\psi}_{{I}_{1} \left( 0 \right)} \! \left( 0 \right) \) である。
                        1. \( \left| 1 + {b}_{t} \right| = \left| {b}_{t} \right| \) である。
         4. \( {a}_{{a}_{t}} \in T \) と \( {b}_{{a}_{t}} \in T \) が存在して、 \( {a}_{t} = {I}_{{a}_{{a}_{t}}} \! \left( {b}_{{a}_{t}} \right) \) である。
            1. \( {\left| {I}_{{a}_{{a}_{t}}} \! \left( {b}_{{a}_{t}} \right) \right|}_{\! I} \) で場合分けする。
               1. \( {\left| {I}_{{a}_{{a}_{t}}} \! \left( {b}_{{a}_{t}} \right) \right|}_{\! I} = ( {a}_{{a}_{{a}_{t}}, {b}_{{b}_{{a}_{t}}} ) \) である。
                  1. \( \left| {b}_{t} \right| \) で場合分けする。
                     1. \( \left| {b}_{t} \right| < {\psi}_{{I}_{1} \left( 0 \right)} \! \left( 0 \right) \) である。
                        1. \( \left| 1 + {b}_{t} \right| = 1 + \left| {b}_{t} \right| \) である。
                     2. \( \left| {b}_{t} \right| \geq {\psi}_{{I}_{1} \left( 0 \right)} \! \left( 0 \right) \) である。
                        1. \( \left| 1 + {b}_{t} \right| = \left| {b}_{t} \right| \) である。
         5. \( {a}_{{a}_{t}} \in T \) と \( {b}_{{a}_{t}} \in T \) が存在して、 \( {a}_{t} = {\psi}_{{a}_{{a}_{t}}} \! \left( {b}_{{a}_{t}} \right) \) である。
            1. TODO
   3. \( t = 1 \) である。
      1. \( \left| 1 \right| = 1 \) である。
   4. \( {a}_{t} \in T \) と \( {b}_{t} \in T \) が存在して、 \( t = {I}_{{a}_{t}} \! \left( {b}_{t} \right) \) である。
      1. TODO
   5. \( {a}_{t} \in T \) と \( {b}_{t} \in T \) が存在して、 \( t = {\psi}_{{a}_{t}} \! \left( {b}_{t} \right) \) である。
      1. TODO