ordinal-exponentiation.txt

z^z'

z^ω = ω
z^(ω ^(1 + α) * z') = z^(ω * ω^α * z') = (z^ω)^(ω^α * z') = ω^(ω^α * z')
(ω^α)^α' = ω^(α*α')

(ω * ω^α * x) ^ (ω * ω^β * y) = ω^((1+α) * ω^(1+β) * y)
x ^ (ω * ω^β * y) = (x^ω)^(ω^β * y) = ω^(ω^β * y)
(ω * ω^α * x) ^ y = ω * ω^α * ω * ω^α * ... ω * ω^α * x
                  = ω^((1+α)*y) * x
x ^ y

k > 0
(ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^0 * x_k) ^ ω
  ?= ω^(α_0*ω)

(1 + ω) = ω ==>

(ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^0 * x_k) * ω^(α_0*ω)
ω^(α_0 + α_0*ω)

(ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^0 * x_k) ^ (ω * ω^β * y)
  = 

(ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k + z) ^ y 
  = (ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k + z) * (ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k + z) * ...  * (ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k + z)
  = (ω^(α_0+α_0) * x_0 + ω^(α_0+α_1) * x_1 + ... + ω^(α_0+α_k) * x_k + ω^α_0 * x_0 * z + ω^α_1 * x_1 + ... + ω^α_k * x_k + z) * ...  * (ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k)
  = ω^(α_0+α_0+...+α_0) * x_0 + ω^(α_0+α_0+...+α_1) * x_1 + ... + ω^(α_0+α_0+...+α_k) * x_k + 
    ω^(α_0+...+α_0) * x_0 * z+ ω^(α_0+...+α_1) * x_1 + ... + ω^(α_0+...+α_k) * x_k + 
    ...
    ω^(α_0+α_0) * x_0 * z + ω^(α_0+α_1) * x_1 + ... + ω^(α_0+α_k) * x_k + 
    ω^α_0 * x_0 * z + ω^α_1 * x_1 + ... + ω^α_k * x_k + 
    z
  = ω^(α_0*y) * x_0 + ω^(α_0*(y-1)+α_1) * x_1 + ... + ω^(α_0*(y-1)+α_k) * x_k + 
    ω^(α_0*(y-1)) * x_0 * z+ ω^(α_0*(y-2)+α_1) * x_1 + ... + ω^(α_0*(y-2)+α_k) * x_k + 
    ...
    ω^(α_0*2) * x_0 * z + ω^(α_0+α_1) * x_1 + ... + ω^(α_0+α_k) * x_k + 
    ω^α_0 * x_0 * z + ω^α_1 * x_1 + ... + ω^α_k * x_k + 
    z

(ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k) ^ y 
  = (ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k) * (ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k) * ...  * (ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k)
  = (ω^(α_0+α_0) * x_0 + ω^(α_0+α_1) * x_1 + ... + ω^(α_0+α_k) * x_k) * ...  * (ω^α_0 * x_0 + ω^α_1 * x_1 + ... + ω^α_k * x_k)
  = (ω^(α_0+α_0+...+α_0) * x_0 + ω^(α_0+α_0+...+α_1) * x_1 + ... + ω^(α_0+α_0+...+α_k) * x_k)
  = (ω^(α_0*y) * x_0 + ω^(α_0*(y-1)+α_1) * x_1 + ... + ω^(α_0*(y-1)+α_k) * x_k)