----------------------------------------------------------------------------------------------------
-- 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 37 _^_

_^_ : 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