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

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

module CantorNormalForm.Exponentiation where

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


infixl  _^_

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