prop_floorLog :: Positive Int -> Bool
prop_floorLog Positive {getPositive = n} =
  floorLog n == floor @Double @Int (logBase 2 $ fromIntegral n)

--
--   In the sequel, we use the convention that expressions surrounded by square brackets are evaluated using ordinal operations, while other expressions are evaluated using nim operations.  For example, \([2\cdot 2] = 4\), but \(2\cdot 2=3\).

    floorLog,

import Math.NumberTheory.Logarithms

-- | Index of highest-order set bit, or -1 if there are none.
floorLog :: (Bits a, Num b) => a -> b
floorLog n
  | n == zeroBits = -1
  | otherwise = 1 + floorLog (n .>>. 1)

-- | Finite nimber addition is calculated as follows: the nimber sum of a two-power and itself is 0, while the nimber sum of a set of distinct two-powers is their ordinary sum.

-- | Finite nimber addition is calculated as follows: the nim sum of a two-power (Conway's name for a [power] of 2) and itself is 0, while the nim sum of a set of distinct two-powers is equal to their [sum].

--   Finite nimber multiplication is calculated as follows: the nimber square of a Fermat two-power is its sesquimultiple, while the nimber product of a set of distinct Fermat two-powers is their ordinary product.
--   The sesquimultiple of a Fermat two-power is equal to itself plus the product of all smaller Fermat two-powers.

--   Finite nimber multiplication is calculated as follows: the nim square of a Fermat two-power (a number of the form \(\left[2^{2^n}\right]\) for some \(n\)) is its sesquimultiple, while the nim product of a set of distinct Fermat two-powers is their [product].
--   The sesquimultiple of a Fermat two-power is equal to itself plus (or [plus]) the product (or [product]) of all smaller Fermat two-powers.

    let m = max (floorLog @Int (floorLog a)) (floorLog @Int (floorLog b)) -- D = 2^2^m is the largest Fermat 2-power less than or equal to both a and b

    let m = max (intLog2 (naturalLog2 $ getFiniteNimber a)) (intLog2 (naturalLog2 $ getFiniteNimber b)) -- D = 2^2^m is the largest Fermat 2-power less than or equal to both a and b

  let m = floorLog @Int $ floorLog n -- D = 2^2^m is the largest Fermat 2-power less than or equal to n

  let m = intLog2 . naturalLog2 $ getFiniteNimber n -- D = 2^2^m is the largest Fermat 2-power less than or equal to n

pow :: (Integral a, Bits a) => FiniteNimber -> a -> FiniteNimber

pow :: FiniteNimber -> Integer -> FiniteNimber

      let m = floorLog @Int $ floorLog x
       in (foldr (mult' m . snd) 1 . filter (testBit n . fst) . zip [0 ..] . take (1 + floorLog (n + 1))) $ iterate (sqr' m) x

      let m = intLog2 . naturalLog2 $ getFiniteNimber x
       in (foldr (mult' m . snd) 1 . filter (testBit n . fst) . zip [0 ..] . take (1 + integerLog2 (n + 1))) $ iterate (sqr' m) x

    let m = floorLog @Int $ floorLog n -- D = 2^2^m is the largest Fermat 2-power less than or equal to n

    let m = intLog2 . naturalLog2 $ getFiniteNimber n -- D = 2^2^m is the largest Fermat 2-power less than or equal to n

    let m = floorLog @Int $ floorLog n -- D = 2^2^m is the largest Fermat 2-power less than or equal to n

    let m = intLog2 . naturalLog2 $ getFiniteNimber n -- D = 2^2^m is the largest Fermat 2-power less than or equal to n

  let m = 1 + floorLog @Int (floorLog n) -- 2^2^m is the order of the smallest field containing n

  let m = 1 + intLog2 (naturalLog2 $ getFiniteNimber n) -- 2^2^m is the order of the smallest field containing n

{-# LANGUAGE DerivingStrategies #-}
{-# OPTIONS_GHC -Wno-type-defaults #-}
--   This module implements the set of nimbers below \(\left[\omega^{\omega^\omega}\right]\), which are the smallest algebraically closed field of characteristic two.
--   See /On the algebraic closure of two/ by H. W. Lenstra, Jr: <https://www.sciencedirect.com/science/article/pii/1385725877900531>.
module Data.Nimber.Algebraic
  (
  )
where
import Data.Nimber.Finite
import Numeric.Natural
data AlgebraicNimber where

                      Data.Nimber.Finite

                      Data.Nimber.Finite,
                      Data.Nimber.Algebraic,

                      arithmoi,
                      integer-logarithms,