----------------------------------------------------------------------------------------------------
-- Exponentiation of Cantor Normal Forms
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module CantorNormalForm.Exponentiation where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)
open import Cubical.Relation.Nullary

open import CantorNormalForm.Base
open import CantorNormalForm.Addition
open import CantorNormalForm.Subtraction
open import CantorNormalForm.Multiplication

{-

The definition of exponentiation for CNFs is motivated by the
following properties of ordinal exponentiation:

■ a ^ 0 = 1 ^ b = 1

■ 0 ^ b = 0

■ a ^ k = a · a ^ (k - 1)   for 0 < k < ω

■ k ^ (ω ^ b) = ω ^ (ω ^ (b - 1))

■ (ω ^ a + ω ^ b) ^ (ω ^ c) = ω ^ (a · ω ^ c)   for a ≥ b > 0 and c

■ a ^ (b + c) = a ^ b · a ^ c

■ a ^ (b · c) = (a ^ b) ^ c

-}


infixl  _^_

_^_ : Cnf → Cnf → Cnf
a ^ 𝟎 = 𝟏
𝟎 ^ b@(ω^ _ + _ [ _ ]) = 𝟎
(ω^ 𝟎 + 𝟎 [ _ ]) ^ b@(ω^ _ + _ [ _ ]) = 𝟏
a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]) ^
 b@(ω^ 𝟎 + y [ _ ]) = a · a ^ y
a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]) ^
 b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ]) = ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y
a@(ω^ (ω^ _ + _ [ _ ]) + _ [ _ ]) ^
 b@(ω^ 𝟎 + y [ _ ]) = a · a ^ y
a@(ω^ a₁@(ω^ _ + _ [ _ ]) + _ [ _ ]) ^
 b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ]) = ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y



𝟎^-spec : ∀ {a} → a > 𝟎 → 𝟎 ^ a ≡ 𝟎
𝟎^-spec <₁ = refl

𝟏^-spec : ∀ {r} b → (ω^ 𝟎 + 𝟎 [ r ]) ^ b ≡ 𝟏
𝟏^-spec 𝟎 = refl
𝟏^-spec (ω^ _ + _ [ _ ]) = refl

nz^𝟏-is-identity : ∀ a b {r} → (ω^ a + b [ r ]) ^ 𝟏 ≡ ω^ a + b [ r ]
nz^𝟏-is-identity  𝟎                𝟎               = Cnf⁼ refl refl
nz^𝟏-is-identity  𝟎               (ω^ _ + _ [ _ ]) = Cnf⁼ refl refl
nz^𝟏-is-identity (ω^ _ + _ [ _ ])  𝟎               = Cnf⁼ refl refl
nz^𝟏-is-identity (ω^ _ + _ [ _ ]) (ω^ _ + _ [ _ ]) = refl

nz^𝟏-is-identity' : ∀ {a} → a > 𝟎 → a ^ 𝟏 ≡ a
nz^𝟏-is-identity' {ω^ a + b [ _ ]} <₁ = nz^𝟏-is-identity a b

^+𝟏-spec : (a b : Cnf) → a ^ (b + 𝟏) ≡ a ^ b · a
^+𝟏-spec a@𝟎 b@𝟎 = refl  -- : 𝟎 ≡ 𝟎
^+𝟏-spec a@𝟎 b@(ω^ b₁ + _ [ _ ]) with <-tri b₁ 𝟎
... | inr _ = refl  -- : 𝟎 ≡ 𝟎
^+𝟏-spec a@(ω^ _ + _ [ _ ]) b@𝟎 =
   a ^ (𝟎 + 𝟏)
  ≡⟨ nz^𝟏-is-identity _ _ ⟩
   a
  ≡⟨ sym (𝟏·-is-identity _) ⟩
   a ^ 𝟎 · a ∎
^+𝟏-spec a@(ω^ 𝟎 + 𝟎 [ _ ]) b@(ω^ b₁ + _ [ _ ]) with <-tri b₁ 𝟎
... | inr _ = refl  -- : 𝟏 ≡ 𝟏
^+𝟏-spec a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]) b@(ω^ 𝟎 + y [ _ ]) =
   a ^ (b + 𝟏)
  ≡⟨ refl ⟩
   a · a ^ (y + 𝟏)
  ≡⟨ cong (a ·_) (^+𝟏-spec a y) ⟩
   a · (a ^ y · a)
  ≡⟨ ·-is-assoc a (a ^ y) a ⟩
   a · a ^ y · a
  ≡⟨ refl ⟩
   a ^ b · a ∎
^+𝟏-spec a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]) b@(ω^ (ω^ 𝟎 + 𝟎 [ _ ]) + y [ _ ]) =
   a ^ (b + 𝟏)
  ≡⟨ refl ⟩
   ω · a ^ (y + 𝟏)
  ≡⟨ cong (ω ·_) (^+𝟏-spec a y) ⟩
   ω · (a ^ y · a)
  ≡⟨ ·-is-assoc ω (a ^ y) a ⟩
   (ω · a ^ y) · a
  ≡⟨ refl ⟩
   a ^ b · a ∎
^+𝟏-spec a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
         b@(ω^ b₁@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]) + y [ _ ]) =
   a ^ (b + 𝟏)
  ≡⟨ refl ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ (y + 𝟏)
  ≡⟨ cong (ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ ·_) (^+𝟏-spec a y) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · (a ^ y · a)
  ≡⟨ ·-is-assoc ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ (a ^ y) a ⟩
   (ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y) · a
  ≡⟨ refl ⟩
   a ^ b · a ∎
^+𝟏-spec a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
         b@(ω^ b₁@(ω^ (ω^ _ + _ [ _ ]) + _ [ _ ]) + y [ _ ]) =
   a ^ (b + 𝟏)
  ≡⟨ refl ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ (y + 𝟏)
  ≡⟨ cong (ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ ·_) (^+𝟏-spec a y) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · (a ^ y · a)
  ≡⟨ ·-is-assoc ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ (a ^ y) a ⟩
   (ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y) · a
  ≡⟨ refl ⟩
   a ^ b · a ∎
^+𝟏-spec a@(ω^ (ω^ _ + _ [ _ ]) + _ [ _ ])
         b@(ω^ 𝟎 + y [ _ ]) =
   a ^ (b + 𝟏)
  ≡⟨ refl ⟩
   a · a ^ (y + 𝟏)
  ≡⟨ cong (a ·_) (^+𝟏-spec a y) ⟩
   a · (a ^ y · a)
  ≡⟨ ·-is-assoc a (a ^ y) a ⟩
   a · a ^ y · a
  ≡⟨ refl ⟩
   a ^ b · a ∎
^+𝟏-spec a@(ω^ a₁@(ω^ _ + _ [ _ ]) + _ [ _ ])
         b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ]) =
   a ^ (b + 𝟏)
  ≡⟨ refl ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ (y + 𝟏)
  ≡⟨ cong (ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ ·_) (^+𝟏-spec a y) ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · (a ^ y · a)
  ≡⟨ ·-is-assoc ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ (a ^ y) a ⟩
   (ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y) · a
  ≡⟨ refl ⟩
   a ^ b · a ∎

nz^>𝟎 : ∀ {a} b → a > 𝟎 → a ^ b > 𝟎
nz^>𝟎 {ω^ _ + _ [ _ ]} 𝟎 <₁ = <₁
nz^>𝟎 {ω^ 𝟎 + 𝟎 [ _ ]} (ω^ _ + _ [ _ ]) <₁ = <₁
nz^>𝟎 {ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]} (ω^ 𝟎 + y [ _ ]) <₁ =
  ω^·ω^>𝟎 _ _ <₁ (nz^>𝟎 y <₁)
nz^>𝟎 {ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]} (ω^ (ω^ _ + _ [ _ ]) + y [ _ ]) <₁ =
  ω^·ω^>𝟎 _ _ <₁ (nz^>𝟎 y <₁)
nz^>𝟎 {ω^ (ω^ _ + _ [ _ ]) + _ [ _ ]} (ω^ 𝟎 + y [ _ ]) <₁ =
  ω^·ω^>𝟎 _ _ <₁ (nz^>𝟎 y <₁)
nz^>𝟎 {ω^ (ω^ _ + _ [ _ ]) + _ [ _ ]} (ω^ (ω^ _ + _ [ _ ]) + y [ _ ]) <₁ =
  ω^·ω^>𝟎 _ _ <₁ (nz^>𝟎 y <₁)

fin^fin<ω : ∀ a b → left a ≡ 𝟎 → left b ≡ 𝟎 → a ^ b < ω
fin^fin<ω a b@𝟎 _ _ = <₂ <₁  -- : 𝟏 < ω
fin^fin<ω a@𝟎 b@(ω^ _ + _ [ _ ]) _ _ = <₁  -- : 𝟎 < ω
fin^fin<ω a@(ω^ 𝟎 + 𝟎 [ _ ]) b@(ω^ 𝟎 + _ [ _ ]) _ _ = <₂ <₁  -- : 𝟏 < ω
fin^fin<ω a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]) b@(ω^ 𝟎 + y [ s ]) _ _ = a·a^y<ω  -- : a · a ^ y < ω
 where
  a^y<ω : a ^ y < ω
  a^y<ω = fin^fin<ω a y refl (≤𝟎→≡𝟎 s)
  a·a^y<ω : a · a ^ y < ω
  a·a^y<ω = fin·fin<ω a (a ^ y) refl (<ω→fin a^y<ω)
fin^fin<ω a@(ω^ 𝟎 + _ [ _ ]) b@(ω^ y@(ω^ _ + _ [ _ ]) + _ [ _ ]) _ y≡𝟎 = ⊥-rec (ω≢𝟎 y≡𝟎)
fin^fin<ω a@(ω^ x@(ω^ _ + _ [ _ ]) + _ [ _ ]) b@(ω^ _ + _ [ _ ]) x≡𝟎 _ = ⊥-rec (ω≢𝟎 x≡𝟎)

≤^r : ∀ a b → b > 𝟎 → a ≤ a ^ b
≤^r a@𝟎
    b@(ω^ _ + _ [ _ ])
    <₁ = ≤-refl  -- : 𝟎 ≤ 𝟎
≤^r a@(ω^ 𝟎 + 𝟎 [ _ ])
    b@(ω^ _ + _ [ _ ])
    <₁ = inr (Cnf⁼ refl refl)  -- : 𝟏 ≤ 𝟏
≤^r a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
    b@(ω^ 𝟎 + y [ _ ])
    <₁ = ≤·r a (a ^ y) (nz^>𝟎 y <₁)  -- : a ≤ a · a ^ y
≤^r a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
    b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ])
    <₁ = ≤-trans claim₀ claim₁  -- : a ≤ ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y
 where
  claim₀ : a ≤ ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩
  claim₀ = inl (<₂ <₁)
  claim₁ : ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ ≤ ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y
  claim₁ = ≤·r _ _ (nz^>𝟎 y <₁)
≤^r a@(ω^ (ω^ _ + _ [ _ ]) + _ [ _ ])
    b@(ω^ 𝟎 + y [ _ ])
    <₁ = ≤·r a (a ^ y) (nz^>𝟎 y <₁)  -- : a ≤ a · a ^ y
≤^r a@(ω^ a₁@(ω^ _ + _ [ _ ]) + _ [ _ ])
    b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ])
    <₁ = ≤-trans claim₀ claim₁  -- : a ≤ ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y
 where
  claim₀ : a ≤ ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩
  claim₀ = inl (<₂ (<₂ (<+r _ _ <₁)))
  claim₁ : ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ ≤ ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y
  claim₁ = ≤·r _ _ (nz^>𝟎 y <₁)

^r-is-<-monotone : ∀ a b c → a > 𝟏 → b < c → a ^ b < a ^ c
^r-is-<-monotone a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
                 b@𝟎
                 c@(ω^ _ + _ [ _ ])
                 (<₃ _ <₁) b<c = goal
 where
  goal : 𝟏 < a ^ c
  goal = <∘≤-in-< (<₃ refl <₁) (≤^r a c <₁)
^r-is-<-monotone a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
                 b@(ω^ 𝟎 + y [ _ ])
                 c@(ω^ 𝟎 + z [ _ ])
                 (<₃ _ <₁) (<₃ _ y<z) = goal
 where
  a^y<a^z : a ^ y < a ^ z
  a^y<a^z = ^r-is-<-monotone a y z (<₃ refl <₁) y<z
  goal : a · a ^ y < a · a ^ z
  goal = ω^·-is-<-monotone a (a ^ y) (a ^ z) <₁ a^y<a^z
^r-is-<-monotone a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
                 b@(ω^ 𝟎 + y [ inr 𝟎≡y ])
                 c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ _ ])
                 (<₃ _ <₁) b<c = goal
 where
  a^y<ω : a ^ y < ω
  a^y<ω = fin^fin<ω a y refl (sym 𝟎≡y)
  l⟨a^y⟩≡𝟎 : left (a ^ y) ≡ 𝟎
  l⟨a^y⟩≡𝟎 = <ω→fin a^y<ω
  a·a^y<ω : a · a ^ y < ω
  a·a^y<ω = fin·fin<ω a (a ^ y) refl l⟨a^y⟩≡𝟎
  goal : a · a ^ y < ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ · a ^ z
  goal = <∘≤-in-< a·a^y<ω (≤-trans (≤₂' 𝟏≤ω^ 𝟎≤) (≤·r _ (a ^ z) (nz^>𝟎 z <₁)))
^r-is-<-monotone a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
                 b@(ω^ b₁@(ω^ _ + _ [ _ ]) + _ [ _ ])
                 c@(ω^ 𝟎 + _ [ _ ])
                 (<₃ _ <₁) b<c = ⊥-rec (<→≯ b<c (<₂ <₁))
^r-is-<-monotone a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
                 b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ s ])
                 c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ _ ])
                 (<₃ _ <₁) (<₂ b₁<c₁) = goal
 where
  claim₀ : ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ < ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩
  claim₀ = <₂ (<₂ (-𝟏-is-<-monotone b₁ c₁ <₁ b₁<c₁))
  y<ω^c₁ : y < ω^⟨ c₁ ⟩
  y<ω^c₁ = <-trans (right< b₁ y s) (<₂ b₁<c₁)
  claim₁ : a ^ y < ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩  -- ≡ a ^ ω^⟨ c₁ ⟩
  claim₁ = ^r-is-<-monotone a y ω^⟨ c₁ ⟩ (<₃ refl <₁) y<ω^c₁
  claim : ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y < ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩
  claim = ω^ω^-is-mul-indecomposable _ _ claim₀ claim₁
  goal : ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y < ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ · a ^ z
  goal = <∘≤-in-< claim (≤·r _ (a ^ z) (nz^>𝟎 z <₁))
^r-is-<-monotone a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
                 b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ])
                 c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ _ ])
                 (<₃ _ <₁) (<₃ b₁≡c₁ y<z) = goal
 where
  a^y<a^z : a ^ y < a ^ z
  a^y<a^z = ^r-is-<-monotone a y z (<₃ refl <₁) y<z
  claim : ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y < ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ z
  claim = ω^·-is-<-monotone _ _ _ <₁ a^y<a^z
  goal : ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y < ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ · a ^ z
  goal = subst (λ x → ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y < ω^⟨ ω^⟨ x - 𝟏 ⟩ ⟩ · a ^ z) b₁≡c₁ claim
^r-is-<-monotone a@(ω^ a₁@(ω^ _ + _ [ _ ]) + x [ _ ])
                 b@𝟎
                 c@(ω^ _ + _ [ _ ])
                 a<𝟏 b<c = goal
 where
  goal : 𝟏 < a ^ c
  goal = <∘≤-in-< a<𝟏 (≤^r a c <₁)
^r-is-<-monotone a@(ω^ a₁@(ω^ _ + _ [ _ ]) + x [ _ ])
                 b@(ω^ 𝟎 + y [ _ ])
                 c@(ω^ 𝟎 + z [ _ ])
                 a<𝟏 (<₃ _ y<z) = goal
 where
  a^y<a^z : a ^ y < a ^ z
  a^y<a^z = ^r-is-<-monotone a y z a<𝟏 y<z
  goal : a · a ^ y < a · a ^ z
  goal = ω^·-is-<-monotone a (a ^ y) (a ^ z) <₁ a^y<a^z
^r-is-<-monotone a@(ω^ a₁@(ω^ _ + _ [ _ ]) + x [ _ ])
                 b@(ω^ 𝟎 + y [ s ])
                 c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ t ])
                 a<𝟏 b<c = goal
 where
  claim₀ : a < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩
  claim₀ = <₂ (<₂ (<+r _ _ <₁))
  y<ω^c₁ : y < ω^⟨ c₁ ⟩
  y<ω^c₁ = <₂' (≤∘<-in-< s <₁)
  claim₁ : a ^ y < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩
  claim₁ = ^r-is-<-monotone a y ω^⟨ c₁ ⟩ a<𝟏 y<ω^c₁
  claim : a · a ^ y < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩
  claim = ω^⟨·ω^⟩-is-mul-indecomposable a (a ^ y) a₁ c₁ <₁ <₁ claim₀ claim₁
  goal : a · a ^ y < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ · a ^ z
  goal = <∘≤-in-< claim (≤·r _ (a ^ z) (nz^>𝟎 z <₁))
^r-is-<-monotone a@(ω^ a₁@(ω^ _ + _ [ _ ]) + x [ _ ])
                 b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ])
                 c@(ω^ 𝟎 + z [ _ ])
                 a<𝟏 b<c = ⊥-rec (<→≯ b<c (<₂ <₁))
^r-is-<-monotone a@(ω^ a₁@(ω^ a₂ + _ [ _ ]) + x [ _ ])
                 b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ s ])
                 c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ t ])
                 a<𝟏 (<₂ b₁<c₁) = goal
 where
  claim₀ : ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩
  claim₀ = <₂ (<₂ (+r-is-<-monotone a₂ b₁ c₁ b₁<c₁))
  y<ω^c₁ : y < ω^⟨ c₁ ⟩
  y<ω^c₁ = <₂' (≤∘<-in-< s b₁<c₁)
  claim₁ : a ^ y < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩
  claim₁ = ^r-is-<-monotone a y ω^⟨ c₁ ⟩ a<𝟏 y<ω^c₁
  claim : ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩
  claim = ω^⟨·ω^⟩-is-mul-indecomposable _ (a ^ y) a₁ c₁ <₁ <₁ claim₀ claim₁
  goal : ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ · a ^ z
  goal = <∘≤-in-< claim (≤·r _ (a ^ z) (nz^>𝟎 z <₁))
^r-is-<-monotone a@(ω^ a₁@(ω^ _ + _ [ _ ]) + x [ _ ])
                 b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ s ])
                 c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ t ])
                 a<𝟏 (<₃ b₁≡c₁ y<z) = goal
 where
  a^y<a^z : a ^ y < a ^ z
  a^y<a^z = ^r-is-<-monotone a y z a<𝟏 y<z
  claim : ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y < ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ z
  claim = ω^·-is-<-monotone _ _ _ <₁ a^y<a^z
  goal : ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y < ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ · a ^ z
  goal = subst (λ x → ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y < ω^⟨ a₁ · ω^⟨ x ⟩ ⟩ · a ^ z) b₁≡c₁ claim


^r-is-≤-monotone : ∀ a b c → a > 𝟎 → b ≤ c → a ^ b ≤ a ^ c
^r-is-≤-monotone a b c _ (inr c≡b) =
    inr (cong (a ^_) c≡b)
^r-is-≤-monotone a@(ω^ 𝟎 + 𝟎 [ _ ]) b c _ (inl b<c) =
    inr (𝟏^-spec c ∙ sym (𝟏^-spec b))
^r-is-≤-monotone a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ]) b c _ (inl b<c) =
    inl (^r-is-<-monotone a b c (<₃ refl <₁) b<c)
^r-is-≤-monotone a@(ω^ (ω^ _ + _ [ _ ]) + _ [ _ ]) b c _ (inl b<c) =
    inl (^r-is-<-monotone a b c (<₂ <₁) b<c)


exponent-sum : ∀ a b c → a ^ (b + c) ≡ a ^ b · a ^ c
exponent-sum a 𝟎 𝟎 = refl  -- : 𝟎 ≡ 𝟎
exponent-sum a 𝟎 c@(ω^ _ + _ [ _ ]) =
   a ^ c
  ≡⟨ sym (𝟏·-is-identity (a ^ c)) ⟩
   𝟏 · a ^ c ∎
exponent-sum a b@(ω^ _ + _ [ _ ]) 𝟎 =
   a ^ b
  ≡⟨ sym (·𝟏-is-identity (a ^ b)) ⟩
   a ^ b · 𝟏 ∎
exponent-sum 𝟎 b@(ω^ _ + _ [ _ ]) c@(ω^ _ + _ [ _ ]) =
   𝟎 ^ (b + c)
  ≡⟨ 𝟎^-spec (<∘≤-in-< <₁ (≤+r b c)) ⟩
   𝟎 ∎
exponent-sum a@(ω^ 𝟎 + 𝟎 [ _ ]) b@(ω^ _ + _ [ _ ]) c@(ω^ _ + _ [ _ ]) =
   a ^ (b + c)
  ≡⟨ 𝟏^-spec (b + c) ⟩
   𝟏 -- ≡ 𝟏 · 𝟏
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
exponent-sum a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
             b@(ω^ 𝟎 + y [ _ ])
             c@(ω^ 𝟎 + z [ _ ]) =
   a ^ (b + c)
  ≡⟨ refl ⟩
   a · a ^ (y + c)
  ≡⟨ cong (a ·_) (exponent-sum a y c) ⟩
   a · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc a (a ^ y) (a ^ c) ⟩
   a · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
exponent-sum a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
             b@(ω^ 𝟎 + y [ s ])
             c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ _ ]) =
   a ^ (b + c)
  ≡⟨ refl ⟩
   a ^ c
  ≡⟨ refl ⟩
   ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ · a ^ z
  ≡⟨ refl ⟩  -- note: ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ ≡ a · ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩
   (a · ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩) · a ^ z
  ≡⟨ sym (·-is-assoc a ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ (a ^ z)) ⟩
   a · (ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ · a ^ z)
  ≡⟨ refl ⟩
   a · a ^ c
  ≡⟨ cong (λ x → a · a ^ x) c≡y+c ⟩
   a · a ^ (y + c)
  ≡⟨ cong (a ·_) (exponent-sum a y c) ⟩
   a · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc a (a ^ y) (a ^ c) ⟩
   a · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
 where
  ly<lc : left y < left c
  ly<lc = ≤∘<-in-< s <₁
  c≡y+c : c ≡ y + c
  c≡y+c = sym (+-left-cancel y c ly<lc)
exponent-sum a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
             b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ])
             c@(ω^ 𝟎 + z [ _ ]) =
   a ^ (b + c)
  ≡⟨ refl ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ (y + c)
  ≡⟨ cong (ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ ·_) (exponent-sum a y c) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ (a ^ y) (a ^ c) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
exponent-sum a@(ω^ 𝟎 + (ω^ _ + _ [ _ ]) [ _ ])
             b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ s ])
             c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ _ ]) with <-tri b₁ c₁
... | inl b₁<c₁ =
   a ^ c
  ≡⟨ refl ⟩
   ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ · a ^ z
  ≡⟨ cong (_· a ^ z) p ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ · a ^ z
  ≡⟨ sym (·-is-assoc ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ (a ^ z)) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · (ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ · a ^ z)
  ≡⟨ refl ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ c
  ≡⟨ cong (λ x → ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ x) c≡y+c ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ (y + c)
  ≡⟨ cong (ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ ·_) (exponent-sum a y c) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ (a ^ y) (a ^ c) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
 where
  ly<lc : left y < left c
  ly<lc = ≤∘<-in-< s b₁<c₁
  c≡y+c : c ≡ y + c
  c≡y+c = sym (+-left-cancel y c ly<lc)
  b₁-𝟏<c₁-𝟏 : b₁ - 𝟏 < c₁ - 𝟏
  b₁-𝟏<c₁-𝟏 = -𝟏-is-<-monotone b₁ c₁ <₁ b₁<c₁
  p : ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩ ≡ ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · ω^⟨ ω^⟨ c₁ - 𝟏 ⟩ ⟩
  p = sym (·ω^ω^-cancel ω^⟨ b₁ - 𝟏 ⟩ 𝟎 𝟎≤ b₁-𝟏<c₁-𝟏)
... | inr b₁≥c₁ =
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ (y + c)
  ≡⟨ cong (ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ ·_) (exponent-sum a y c) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ (a ^ y) (a ^ c) ⟩
   ω^⟨ ω^⟨ b₁ - 𝟏 ⟩ ⟩ · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
exponent-sum a@(ω^ a₁@(ω^ _ + _ [ _ ]) + _ [ _ ])
             b@(ω^ 𝟎 + y [ _ ])
             c@(ω^ 𝟎 + z [ _ ]) =
   a ^ (b + c)
  ≡⟨ refl ⟩
   a · a ^ (y + c)
  ≡⟨ cong (a ·_) (exponent-sum a y c) ⟩
   a · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc a (a ^ y) (a ^ c) ⟩
   a · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
exponent-sum a@(ω^ a₁@(ω^ _ + _ [ _ ]) + x [ r ])
             b@(ω^ 𝟎 + y [ s ])
             c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ _ ]) =
   a ^ (b + c)
  ≡⟨ refl ⟩
   ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ · a ^ z
  ≡⟨ cong (_· a ^ z) p ⟩
   (a · ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩) · a ^ z
  ≡⟨ sym (·-is-assoc a ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ (a ^ z)) ⟩
   a · (ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ · a ^ z)
  ≡⟨ refl ⟩
   a · a ^ c
  ≡⟨ cong (λ x → a · a ^ x) c≡y+c ⟩
   a · a ^ (y + c)
  ≡⟨ cong (a ·_) (exponent-sum a y c) ⟩
   a · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc a (a ^ y) (a ^ c) ⟩
   a · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
 where
  ly<lc : left y < left c
  ly<lc = ≤∘<-in-< s <₁
  c≡y+c : c ≡ y + c
  c≡y+c = sym (+-left-cancel y c ly<lc)
  p : ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ ≡ a · ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩
  p = sym (·ω^⟨·ω^⟩-cancel a a₁ c₁ <₁ <₁ (<+r _ c₁ <₁))
exponent-sum a@(ω^ a₁@(ω^ _ + _ [ _ ]) + _ [ _ ])
             b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ])
             c@(ω^ 𝟎 + z [ _ ]) =
   a ^ (b + c)
  ≡⟨ refl ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ (y + c)
  ≡⟨ cong (ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ ·_) (exponent-sum a y c) ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ (a ^ y) (a ^ c) ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
exponent-sum a@(ω^ a₁@(ω^ _ + _ [ _ ]) + _ [ _ ])
             b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ s ])
             c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ _ ]) with <-tri b₁ c₁
... | inl b₁<c₁ =
   a ^ c
  ≡⟨ refl ⟩
   ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ · a ^ z
  ≡⟨ cong (_· a ^ z) p ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ · a ^ z
  ≡⟨ sym (·-is-assoc ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ (a ^ z)) ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · (ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ · a ^ z)
  ≡⟨ refl ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ c
  ≡⟨ cong (λ x → ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ x) c≡y+c ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ (y + c)
  ≡⟨ cong (ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ ·_) (exponent-sum a y c) ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ (a ^ y) (a ^ c) ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎
 where
  ly<lc : left y < left c
  ly<lc = ≤∘<-in-< s b₁<c₁
  c≡y+c : c ≡ y + c
  c≡y+c = sym (+-left-cancel y c ly<lc)
  p : ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩ ≡ ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · ω^⟨ a₁ · ω^⟨ c₁ ⟩ ⟩
  p = sym (·ω^⟨·ω^⟩-cancel ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ a₁ c₁ <₁ <₁
                           (+r-is-<-monotone (left a₁) b₁ c₁ b₁<c₁))
... | inr b₁≥c₁ =
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ (y + c)
  ≡⟨ cong (ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ ·_) (exponent-sum a y c) ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · (a ^ y · a ^ c)
  ≡⟨ ·-is-assoc ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ (a ^ y) (a ^ c) ⟩
   ω^⟨ a₁ · ω^⟨ b₁ ⟩ ⟩ · a ^ y · a ^ c
  ≡⟨ refl ⟩
   a ^ b · a ^ c ∎