Crypto.Lol.Factored

This module defines types and operations for type-level representation and manipulation of natural numbers, as represented by their prime-power factorizations. It relies on Template Haskell, so parts of the documentation may be difficult to read. See source-level comments for further details.

Factored natural numbers

data Factored

Instances

Eq Factored

Methods

(==) :: Factored -> Factored -> Bool

(/=) :: Factored -> Factored -> Bool

Show Factored

Methods

showsPrec :: Int -> Factored -> ShowS

show :: Factored -> String

showList :: [Factored] -> ShowS

SEq Factored

Methods

(%:==) :: Sing Factored a -> Sing Factored b -> Sing Bool ((Factored :== a) b)

(%:/=) :: Sing Factored a -> Sing Factored b -> Sing Bool ((Factored :/= a) b)

SDecide Factored

Methods

(%~) :: Sing Factored a -> Sing Factored b -> Decision ((Factored :~: a) b)

SingKind Factored

Associated Types

type DemoteRep Factored :: *

Methods

fromSing :: Sing Factored a -> DemoteRep Factored

toSing :: DemoteRep Factored -> SomeSing Factored

(Fact m, C i) => Reflects Factored m i

Methods

value :: Tagged m i i

PEq Factored (Proxy * Factored)

Associated Types

type ((Proxy * Factored) :== (x :: Proxy * Factored)) (y :: Proxy * Factored) :: Bool

type ((Proxy * Factored) :/= (x :: Proxy * Factored)) (y :: Proxy * Factored) :: Bool

Fact m => Show (ArgType Factored m)

Methods

showsPrec :: Int -> ArgType Factored m -> ShowS

show :: ArgType Factored m -> String

showList :: [ArgType Factored m] -> ShowS

data Sing Factored

data Sing Factored where

• SF :: Sing Factored z

type DemoteRep Factored

type DemoteRep Factored = Factored

type (:/=) Factored x y

type (:/=) Factored x y = Not ((:==) Factored x y)

type (:==) Factored a0 b0

type (:==) Factored a0 b0

type SFactored = (Sing :: Factored -> Type)

type Fact m = SingI m

Kind-restricted synonym for SingI.

fType :: Int -> TypeQ

Template Haskell splice for the Factored type corresponding to a given positive integer. Factors its argument using a naive trial-division algorithm with primes, so should only be used on small-to-moderate-sized arguments (any reasonable cyclotomic index should be OK).

fDec :: Int -> DecQ

Template Haskell splice that defines the Factored type synonym F\(n\) for a positive integer \(n\).

reifyFact :: Int -> (forall m. SFactored m -> a) -> a

Reify a Factored as a singleton.

reifyFactI :: Int -> (forall m proxy. Fact m => proxy m -> a) -> a

Reify a Factored for a Fact constraint.

intToFact :: Int -> Factored

Converts input to its data-level Factored representation.

Prime powers

data PrimePower

Instances

Eq PrimePower

Methods

(==) :: PrimePower -> PrimePower -> Bool

(/=) :: PrimePower -> PrimePower -> Bool

Show PrimePower

Methods

showsPrec :: Int -> PrimePower -> ShowS

show :: PrimePower -> String

showList :: [PrimePower] -> ShowS

SEq PrimePower

Methods

(%:==) :: Sing PrimePower a -> Sing PrimePower b -> Sing Bool ((PrimePower :== a) b)

(%:/=) :: Sing PrimePower a -> Sing PrimePower b -> Sing Bool ((PrimePower :/= a) b)

SDecide PrimePower

Methods

(%~) :: Sing PrimePower a -> Sing PrimePower b -> Decision ((PrimePower :~: a) b)

SingKind PrimePower

Associated Types

type DemoteRep PrimePower :: *

Methods

fromSing :: Sing PrimePower a -> DemoteRep PrimePower

toSing :: DemoteRep PrimePower -> SomeSing PrimePower

(PPow pp, C i) => Reflects PrimePower pp i

Methods

value :: Tagged pp i i

PEq PrimePower (Proxy * PrimePower)

Associated Types

type ((Proxy * PrimePower) :== (x :: Proxy * PrimePower)) (y :: Proxy * PrimePower) :: Bool

type ((Proxy * PrimePower) :/= (x :: Proxy * PrimePower)) (y :: Proxy * PrimePower) :: Bool

(PPow pp, (~) * zq (ZqBasic PrimePower pp z), PrimeField (ZpOf zq), Ring zq) => ZPP (ZqBasic PrimePower pp z)

Associated Types

type ZpOf (ZqBasic PrimePower pp z) :: *

Methods

modulusZPP :: Tagged * (ZqBasic PrimePower pp z) PP

liftZp :: ZpOf (ZqBasic PrimePower pp z) -> ZqBasic PrimePower pp z

data Sing PrimePower

data Sing PrimePower where

• SPP :: Sing PrimePower z

type DemoteRep PrimePower

type DemoteRep PrimePower = PrimePower

type (:/=) PrimePower x y

type (:/=) PrimePower x y = Not ((:==) PrimePower x y)

type (:==) PrimePower a0 b0

type (:==) PrimePower a0 b0

type ZpOf (ZqBasic PrimePower pp z)

type ZpOf (ZqBasic PrimePower pp z) = ZqBasic PrimeBin (PrimePP pp) z

type SPrimePower = (Sing :: PrimePower -> Type)

data family Sing k (a :: k) :: *

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z0
• STrue :: Sing Bool z0

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z0
• SEQ :: Sing Ordering z0
• SGT :: Sing Ordering z0

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z0

data Sing Pos

data Sing Pos where

• SO :: Sing Pos z
• SS :: Sing Pos z

data Sing Bin

data Sing Bin where

• SB1 :: Sing Bin z
• SD0 :: Sing Bin z
• SD1 :: Sing Bin z

data Sing PrimeBin

data Sing PrimeBin where

• SP :: Sing PrimeBin z

data Sing PrimePower

data Sing PrimePower where

• SPP :: Sing PrimePower z

data Sing Factored

data Sing Factored where

• SF :: Sing Factored z

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a0] z0
• SCons :: Sing [a0] z0

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a0) z0
• SJust :: Sing (Maybe a0) z0

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a0) z0

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a0 b0) z0
• SRight :: Sing (Either a0 b0) z0

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a0, b0) z0

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a0, b0, c0) z0

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a0, b0, c0, d0) z0

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a0, b0, c0, d0, e0) z0

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a0, b0, c0, d0, e0, f0) z0

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

type PPow pp = SingI pp

Kind-restricted synonym for SingI.

ppType :: PP -> TypeQ

Template Haskell splice for the PrimePower type corresponding to a given PP. (Calls pType on the first component of its argument, so should only be used on small-to-moderate-sized numbers.) This is the preferred (and only) way of constructing a concrete PrimePower type.

ppDec :: PP -> DecQ

Template Haskell splice that defines the PrimePower type synonym PP\(n\), where \( n=p^e \).

reifyPPow :: (Int, Int) -> (forall pp. SPrimePower pp -> a) -> a

Reify a PrimePower as a singleton.

reifyPPowI :: (Int, Int) -> (forall pp proxy. PPow pp => proxy pp -> a) -> a

Reify a PrimePower for a PPow constraint.

Primes

data PrimeBin

Instances

Eq PrimeBin

Methods

(==) :: PrimeBin -> PrimeBin -> Bool

(/=) :: PrimeBin -> PrimeBin -> Bool

Ord PrimeBin

Methods

compare :: PrimeBin -> PrimeBin -> Ordering

(<) :: PrimeBin -> PrimeBin -> Bool

(<=) :: PrimeBin -> PrimeBin -> Bool

(>) :: PrimeBin -> PrimeBin -> Bool

(>=) :: PrimeBin -> PrimeBin -> Bool

max :: PrimeBin -> PrimeBin -> PrimeBin

min :: PrimeBin -> PrimeBin -> PrimeBin

Show PrimeBin

Methods

showsPrec :: Int -> PrimeBin -> ShowS

show :: PrimeBin -> String

showList :: [PrimeBin] -> ShowS

SOrd Bin => SOrd PrimeBin

Methods

sCompare :: Sing PrimeBin t0 -> Sing PrimeBin t1 -> Sing Ordering (Apply PrimeBin Ordering (Apply PrimeBin (TyFun PrimeBin Ordering -> Type) (CompareSym0 PrimeBin) t0) t1)

(%:<) :: Sing PrimeBin t0 -> Sing PrimeBin t1 -> Sing Bool (Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) ((:<$) PrimeBin) t0) t1)

(%:<=) :: Sing PrimeBin t0 -> Sing PrimeBin t1 -> Sing Bool (Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) ((:<=$) PrimeBin) t0) t1)

(%:>) :: Sing PrimeBin t0 -> Sing PrimeBin t1 -> Sing Bool (Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) ((:>$) PrimeBin) t0) t1)

(%:>=) :: Sing PrimeBin t0 -> Sing PrimeBin t1 -> Sing Bool (Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) ((:>=$) PrimeBin) t0) t1)

sMax :: Sing PrimeBin t0 -> Sing PrimeBin t1 -> Sing PrimeBin (Apply PrimeBin PrimeBin (Apply PrimeBin (TyFun PrimeBin PrimeBin -> Type) (MaxSym0 PrimeBin) t0) t1)

sMin :: Sing PrimeBin t0 -> Sing PrimeBin t1 -> Sing PrimeBin (Apply PrimeBin PrimeBin (Apply PrimeBin (TyFun PrimeBin PrimeBin -> Type) (MinSym0 PrimeBin) t0) t1)

SEq PrimeBin

Methods

(%:==) :: Sing PrimeBin a -> Sing PrimeBin b -> Sing Bool ((PrimeBin :== a) b)

(%:/=) :: Sing PrimeBin a -> Sing PrimeBin b -> Sing Bool ((PrimeBin :/= a) b)

SDecide PrimeBin

Methods

(%~) :: Sing PrimeBin a -> Sing PrimeBin b -> Decision ((PrimeBin :~: a) b)

SingKind PrimeBin

Associated Types

type DemoteRep PrimeBin :: *

Methods

fromSing :: Sing PrimeBin a -> DemoteRep PrimeBin

toSing :: DemoteRep PrimeBin -> SomeSing PrimeBin

(Prime p, C i) => Reflects PrimeBin p i

Methods

value :: Tagged p i i

POrd PrimeBin (Proxy * PrimeBin)

Associated Types

type Compare (Proxy * PrimeBin) (arg0 :: Proxy * PrimeBin) (arg1 :: Proxy * PrimeBin) :: Ordering

type ((Proxy * PrimeBin) :< (arg0 :: Proxy * PrimeBin)) (arg1 :: Proxy * PrimeBin) :: Bool

type ((Proxy * PrimeBin) :<= (arg0 :: Proxy * PrimeBin)) (arg1 :: Proxy * PrimeBin) :: Bool

type ((Proxy * PrimeBin) :> (arg0 :: Proxy * PrimeBin)) (arg1 :: Proxy * PrimeBin) :: Bool

type ((Proxy * PrimeBin) :>= (arg0 :: Proxy * PrimeBin)) (arg1 :: Proxy * PrimeBin) :: Bool

type Max (Proxy * PrimeBin) (arg0 :: Proxy * PrimeBin) (arg1 :: Proxy * PrimeBin) :: a0

type Min (Proxy * PrimeBin) (arg0 :: Proxy * PrimeBin) (arg1 :: Proxy * PrimeBin) :: a0

PEq PrimeBin (Proxy * PrimeBin)

Associated Types

type ((Proxy * PrimeBin) :== (x :: Proxy * PrimeBin)) (y :: Proxy * PrimeBin) :: Bool

type ((Proxy * PrimeBin) :/= (x :: Proxy * PrimeBin)) (y :: Proxy * PrimeBin) :: Bool

data Sing PrimeBin

data Sing PrimeBin where

• SP :: Sing PrimeBin z

type DemoteRep PrimeBin

type DemoteRep PrimeBin = PrimeBin

type Min PrimeBin arg0 arg1

type Min PrimeBin arg0 arg1 = Apply PrimeBin PrimeBin (Apply PrimeBin (TyFun PrimeBin PrimeBin -> Type) (Min_1627688153Sym0 PrimeBin) arg0) arg1

type Max PrimeBin arg0 arg1

type Max PrimeBin arg0 arg1 = Apply PrimeBin PrimeBin (Apply PrimeBin (TyFun PrimeBin PrimeBin -> Type) (Max_1627688120Sym0 PrimeBin) arg0) arg1

type (:>=) PrimeBin arg0 arg1

type (:>=) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627688087Sym0 PrimeBin) arg0) arg1

type (:>) PrimeBin arg0 arg1

type (:>) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627688054Sym0 PrimeBin) arg0) arg1

type (:<=) PrimeBin arg0 arg1

type (:<=) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627688021Sym0 PrimeBin) arg0) arg1

type (:<) PrimeBin arg0 arg1

type (:<) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627687988Sym0 PrimeBin) arg0) arg1

type Compare PrimeBin a1 a0

type Compare PrimeBin a1 a0

type (:/=) PrimeBin x y

type (:/=) PrimeBin x y = Not ((:==) PrimeBin x y)

type (:==) PrimeBin a0 b0

type (:==) PrimeBin a0 b0

type SPrimeBin = (Sing :: PrimeBin -> Type)

type Prime p = SingI p

Kind-restricted synonym for SingI.

pType :: Int -> TypeQ

Template Haskell splice for the PrimeBin type corresponding to a given positive prime integer. (Uses prime to enforce primality of the base, so should only be used on small-to-moderate-sized arguments.) This is the preferred (and only) way of constructing a concrete PrimeBin type (and is used to define the Prime\(p\) type synonyms).

pDec :: Int -> DecQ

Template Haskell splice that defines the PrimeBin type synonym Prime\(p\) for a positive prime integer \( p \).

reifyPrime :: Int -> (forall p. SPrimeBin p -> a) -> a

Reify a PrimeBin as a singleton.

reifyPrimeI :: Int -> (forall p proxy. Prime p => proxy p -> a) -> a

Reify a PrimeBin for a Prime constraint.

valueP :: PrimeBin -> Int

Value of a PrimeBin.

Constructors

pToPP :: PrimeBin -> PrimePower

sPToPP :: forall t. Sing t -> Sing (Apply PToPPSym0 t :: PrimePower)

type family PToPP (a :: PrimeBin) :: PrimePower where ...

Equations

PToPP p = Apply PPSym0 (Apply (Apply Tuple2Sym0 p) OSym0)

ppToF :: PrimePower -> Factored

sPpToF :: forall t. Sing t -> Sing (Apply PpToFSym0 t :: Factored)

type family PpToF (a :: PrimePower) :: Factored where ...

Equations

PpToF pp = Apply FSym0 (Apply (Apply (:$) pp) '[])

pToF :: PrimeBin -> Factored

sPToF :: forall t. Sing t -> Sing (Apply PToFSym0 t :: Factored)

type family PToF (a :: PrimeBin) :: Factored where ...

Equations

PToF a_1627689243 = Apply (Apply (Apply (:.$) PpToFSym0) PToPPSym0) a_1627689243

Unwrappers

unF :: Factored -> [PrimePower]

sUnF :: forall t. Sing t -> Sing (Apply UnFSym0 t :: [PrimePower])

type family UnF (a :: Factored) :: [PrimePower] where ...

Equations

UnF (F pps) = pps

unPP :: PrimePower -> (PrimeBin, Pos)

sUnPP :: forall t. Sing t -> Sing (Apply UnPPSym0 t :: (PrimeBin, Pos))

type family UnPP (a :: PrimePower) :: (PrimeBin, Pos) where ...

Equations

UnPP (PP pp) = pp

primePP :: PrimePower -> PrimeBin

type family PrimePP (a :: PrimePower) :: PrimeBin where ...

Equations

PrimePP a_1627678502 = Apply (Apply (Apply (:.$) FstSym0) UnPPSym0) a_1627678502

exponentPP :: PrimePower -> Pos

type family ExponentPP (a :: PrimePower) :: Pos where ...

Equations

ExponentPP a_1627678509 = Apply (Apply (Apply (:.$) SndSym0) UnPPSym0) a_1627678509

Arithmetic operations

fPPMul :: PrimePower -> Factored -> Factored

type family FPPMul (a :: PrimePower) (a :: Factored) :: Factored where ...

Equations

FPPMul pp (F pps) = Apply FSym0 (Apply (Apply PpMulSym0 pp) pps)

fMul :: Factored -> Factored -> Factored

type family FMul (a :: Factored) (a :: Factored) :: Factored where ...

Equations

FMul (F pps1) (F pps2) = Apply FSym0 (Apply (Apply PpsMulSym0 pps1) pps2)

type * a b = FMul a b

Type (family) synonym for multiplication of Factored types.

fDivides :: Factored -> Factored -> Bool

type family FDivides (a :: Factored) (a :: Factored) :: Bool where ...

Equations

FDivides (F pps1) (F pps2) = Apply (Apply PpsDividesSym0 pps1) pps2

type Divides m m' = (Fact m, Fact m', FDivides m m' ~ True)

Constraint synonym for divisibility of Factored types.

fDiv :: Factored -> Factored -> Factored

type family FDiv (a :: Factored) (a :: Factored) :: Factored where ...

Equations

FDiv (F pps1) (F pps2) = Apply FSym0 (Apply (Apply PpsDivSym0 pps1) pps2)

type (/) a b = FDiv a b

Type (family) synonym for division of Factored types.

fGCD :: Factored -> Factored -> Factored

type family FGCD (a :: Factored) (a :: Factored) :: Factored where ...

Equations

FGCD (F pps1) (F pps2) = Apply FSym0 (Apply (Apply PpsGCDSym0 pps1) pps2)

fLCM :: Factored -> Factored -> Factored

type family FLCM (a :: Factored) (a :: Factored) :: Factored where ...

Equations

FLCM (F pps1) (F pps2) = Apply FSym0 (Apply (Apply PpsLCMSym0 pps1) pps2)

type Coprime m m' = FGCD m m' ~ F1

Constraint synonym for coprimality of Factored types.

fOddRadical :: Factored -> Factored

type family FOddRadical (a :: Factored) :: Factored where ...

Equations

FOddRadical (F pps) = Apply FSym0 (Apply PpsOddRadSym0 pps)

pFree :: PrimeBin -> Factored -> Factored

type family PFree (a :: PrimeBin) (a :: Factored) :: Factored where ...

Equations

PFree p (F pps) = Apply FSym0 (Apply (Let1627711705GoSym2 p pps) pps)

Convenient reflections

ppsFact :: forall m. Fact m => Tagged m [PP]

Value-level prime-power factorization tagged by a Factored type.

valueFact :: Fact m => Tagged m Int

The value of a Factored type.

totientFact :: Fact m => Tagged m Int

The totient of a Factored type's value.

radicalFact :: Fact m => Tagged m Int

The radical (product of prime divisors) of a Factored type.

oddRadicalFact :: Fact m => Tagged m Int

The odd radical (product of odd prime divisors) of a Factored type.

valueHatFact :: Fact m => Tagged m Int

The "hat" of a Factored type's value: \( \hat{m} = \begin{cases} m & \mbox{if } m \text{ is odd} \\ m/2 & \text{otherwise} \end{cases} \).

ppPPow :: forall pp. PPow pp => Tagged pp PP

Reflect a PrimePower type to a PP value.

primePPow :: PPow pp => Tagged pp Int

Reflect the prime component of a PrimePower type.

exponentPPow :: PPow pp => Tagged pp Int

Reflect the exponent component of a PrimePower type.

valuePPow :: PPow pp => Tagged pp Int

The value of a PrimePower type.

totientPPow :: PPow pp => Tagged pp Int

The totient of a PrimePower type's value.

radicalPPow :: PPow pp => Tagged pp Int

The radical of a PrimePower type's value.

oddRadicalPPow :: PPow pp => Tagged pp Int

The odd radical of a PrimePower type's value.

valueHatPPow :: PPow pp => Tagged pp Int

The "hat" of a PrimePower type's value: \( p^e \) if \( p \) is odd, \( 2^{e-1} \) otherwise.

valuePrime :: forall p. Prime p => Tagged p Int

The value of a PrimeBin type.

Data-level equivalents of reflections for Factored data

valueF :: Factored -> Int

The value of a Factored.

totientF :: Factored -> Int

Totient of a Factored.

radicalF :: Factored -> Int

The radical of a Factored.

oddRadicalF :: Factored -> Int

The odd radical of a Factored.

valueHatF :: Factored -> Int

The hat of a Factored.

Number-theoretic laws

transDivides :: forall k l m. Proxy k -> Proxy l -> Proxy m -> (k `Divides` l, l `Divides` m) :- (k `Divides` m)

Entails constraint for transitivity of division, i.e. if \( k \mid l \) and \( l \mid m \), then \( k \mid m \).

gcdDivides :: forall m1 m2 g. Proxy m1 -> Proxy m2 -> (Fact m1, Fact m2, g ~ FGCD m1 m2) :- (g `Divides` m1, g `Divides` m2)

Entailment for divisibility by GCD: if \( g=\gcd(m_1,m_2) \) then \( g \mid m_1 \) and \( g \mid m_2 \).

lcmDivides :: forall m1 m2 l. Proxy m1 -> Proxy m2 -> (Fact m1, Fact m2, l ~ FLCM m1 m2) :- (m1 `Divides` l, m2 `Divides` l)

Entailment for LCM divisibility: if \( l=\lcm(m_1,m_2) \) then \( m_1 \mid l \) and \( m_2 \mid l \).

lcm2Divides :: forall m1 m2 l m. Proxy m1 -> Proxy m2 -> Proxy m -> (m1 `Divides` m, m2 `Divides` m, l ~ FLCM m1 m2) :- (m1 `Divides` l, m2 `Divides` l, FLCM m1 m2 `Divides` m)

Entailment for LCM divisibility: the LCM of two divisors of \( m \) also divides \( m \).

pSplitTheorems :: forall p m f. Proxy p -> Proxy m -> (Prime p, Fact m, f ~ PFree p m) :- (f `Divides` m, Coprime (PToF p) f)

Entailment for \( p \)-free division: if \( f \) is \(m \) after removing all \( p \)-factors, then \( f \mid m \) and \( \gcd(f,p)=1 \).

pFreeDivides :: forall p m m'. Proxy p -> Proxy m -> Proxy m' -> (Prime p, m `Divides` m') :- (PFree p m `Divides` PFree p m')

Entailment for \( p \)-free division: if \( m \mid m' \), then \( \text{p-free}(m) \mid \text{p-free}(m') \).

(\\) :: a => (b -> r) -> (:-) a b -> r infixl 1

Given that a :- b, derive something that needs a context b, using the context a

Utility operations on prime powers

valueHat :: Integral i => i -> i

Return \( m \) if \( m \) is odd, and \( m/2 \) otherwise.

type PP = (Int, Int)

Type synonym for (prime, exponent) pair.

ppToPP :: PrimePower -> PP

Conversion.

valuePP :: PP -> Int

The value of a prime power.

totientPP :: PP -> Int

Totient of a prime power.

radicalPP :: PP -> Int

The radical of a prime power.

oddRadicalPP :: PP -> Int

The odd radical of a prime power.

valueHatPP :: PP -> Int

The "hat" of a prime power: \( p^e \) if \( p \) is odd, \( 2^{e-1} \) otherwise.

Re-export

Positive naturals in Peano representation

data Pos

Constructors

O

S Pos

Instances

Eq Pos

Methods

(==) :: Pos -> Pos -> Bool

(/=) :: Pos -> Pos -> Bool

Ord Pos

Methods

compare :: Pos -> Pos -> Ordering

(<) :: Pos -> Pos -> Bool

(<=) :: Pos -> Pos -> Bool

(>) :: Pos -> Pos -> Bool

(>=) :: Pos -> Pos -> Bool

max :: Pos -> Pos -> Pos

min :: Pos -> Pos -> Pos

Show Pos

Methods

showsPrec :: Int -> Pos -> ShowS

show :: Pos -> String

showList :: [Pos] -> ShowS

SOrd Pos

Methods

sCompare :: Sing Pos t0 -> Sing Pos t1 -> Sing Ordering (Apply Pos Ordering (Apply Pos (TyFun Pos Ordering -> Type) (CompareSym0 Pos) t0) t1)

(%:<) :: Sing Pos t0 -> Sing Pos t1 -> Sing Bool (Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) ((:<$) Pos) t0) t1)

(%:<=) :: Sing Pos t0 -> Sing Pos t1 -> Sing Bool (Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) ((:<=$) Pos) t0) t1)

(%:>) :: Sing Pos t0 -> Sing Pos t1 -> Sing Bool (Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) ((:>$) Pos) t0) t1)

(%:>=) :: Sing Pos t0 -> Sing Pos t1 -> Sing Bool (Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) ((:>=$) Pos) t0) t1)

sMax :: Sing Pos t0 -> Sing Pos t1 -> Sing Pos (Apply Pos Pos (Apply Pos (TyFun Pos Pos -> Type) (MaxSym0 Pos) t0) t1)

sMin :: Sing Pos t0 -> Sing Pos t1 -> Sing Pos (Apply Pos Pos (Apply Pos (TyFun Pos Pos -> Type) (MinSym0 Pos) t0) t1)

SEq Pos

Methods

(%:==) :: Sing Pos a -> Sing Pos b -> Sing Bool ((Pos :== a) b)

(%:/=) :: Sing Pos a -> Sing Pos b -> Sing Bool ((Pos :/= a) b)

SDecide Pos

Methods

(%~) :: Sing Pos a -> Sing Pos b -> Decision ((Pos :~: a) b)

SingKind Pos

Associated Types

type DemoteRep Pos :: *

Methods

fromSing :: Sing Pos a -> DemoteRep Pos

toSing :: DemoteRep Pos -> SomeSing Pos

SingI Pos O

Methods

sing :: Sing O a

SingI Pos n0 => SingI Pos (S n0)

Methods

sing :: Sing (S n0) a

POrd Pos (Proxy * Pos)

Associated Types

type Compare (Proxy * Pos) (arg0 :: Proxy * Pos) (arg1 :: Proxy * Pos) :: Ordering

type ((Proxy * Pos) :< (arg0 :: Proxy * Pos)) (arg1 :: Proxy * Pos) :: Bool

type ((Proxy * Pos) :<= (arg0 :: Proxy * Pos)) (arg1 :: Proxy * Pos) :: Bool

type ((Proxy * Pos) :> (arg0 :: Proxy * Pos)) (arg1 :: Proxy * Pos) :: Bool

type ((Proxy * Pos) :>= (arg0 :: Proxy * Pos)) (arg1 :: Proxy * Pos) :: Bool

type Max (Proxy * Pos) (arg0 :: Proxy * Pos) (arg1 :: Proxy * Pos) :: a0

type Min (Proxy * Pos) (arg0 :: Proxy * Pos) (arg1 :: Proxy * Pos) :: a0

PEq Pos (Proxy * Pos)

Associated Types

type ((Proxy * Pos) :== (x :: Proxy * Pos)) (y :: Proxy * Pos) :: Bool

type ((Proxy * Pos) :/= (x :: Proxy * Pos)) (y :: Proxy * Pos) :: Bool

SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) AddPosSym1

Methods

suppressUnusedWarnings :: Proxy AddPosSym1 t -> ()

SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) SubPosSym1

Methods

suppressUnusedWarnings :: Proxy SubPosSym1 t -> ()

SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> Type) -> *) AddPosSym0

Methods

suppressUnusedWarnings :: Proxy AddPosSym0 t -> ()

SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> Type) -> *) SubPosSym0

Methods

suppressUnusedWarnings :: Proxy SubPosSym0 t -> ()

SuppressUnusedWarnings (TyFun Pos Pos -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

data Sing Pos

data Sing Pos where

• SO :: Sing Pos z
• SS :: Sing Pos z

type DemoteRep Pos

type DemoteRep Pos = Pos

type Min Pos arg0 arg1

type Min Pos arg0 arg1 = Apply Pos Pos (Apply Pos (TyFun Pos Pos -> Type) (Min_1627688153Sym0 Pos) arg0) arg1

type Max Pos arg0 arg1

type Max Pos arg0 arg1 = Apply Pos Pos (Apply Pos (TyFun Pos Pos -> Type) (Max_1627688120Sym0 Pos) arg0) arg1

type (:>=) Pos arg0 arg1

type (:>=) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627688087Sym0 Pos) arg0) arg1

type (:>) Pos arg0 arg1

type (:>) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627688054Sym0 Pos) arg0) arg1

type (:<=) Pos arg0 arg1

type (:<=) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627688021Sym0 Pos) arg0) arg1

type (:<) Pos arg0 arg1

type (:<) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627687988Sym0 Pos) arg0) arg1

type Compare Pos a1 a0

type Compare Pos a1 a0

type (:/=) Pos x y

type (:/=) Pos x y = Not ((:==) Pos x y)

type (:==) Pos a0 b0

type (:==) Pos a0 b0

type Apply Pos Pos SSym0 l0

type Apply Pos Pos SSym0 l0 = SSym1 l0

type Apply Pos Pos (AddPosSym1 l1) l0

type Apply Pos Pos (AddPosSym1 l1) l0

type Apply Pos Pos (SubPosSym1 l1) l0

type Apply Pos Pos (SubPosSym1 l1) l0

type Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0

type Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0 = AddPosSym1 l0

type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0

type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0 = SubPosSym1 l0

data family Sing k (a :: k) :: *

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z0
• STrue :: Sing Bool z0

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z0
• SEQ :: Sing Ordering z0
• SGT :: Sing Ordering z0

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z0

data Sing Pos

data Sing Pos where

• SO :: Sing Pos z
• SS :: Sing Pos z

data Sing Bin

data Sing Bin where

• SB1 :: Sing Bin z
• SD0 :: Sing Bin z
• SD1 :: Sing Bin z

data Sing PrimeBin

data Sing PrimeBin where

• SP :: Sing PrimeBin z

data Sing PrimePower

data Sing PrimePower where

• SPP :: Sing PrimePower z

data Sing Factored

data Sing Factored where

• SF :: Sing Factored z

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a0] z0
• SCons :: Sing [a0] z0

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a0) z0
• SJust :: Sing (Maybe a0) z0

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a0) z0

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a0 b0) z0
• SRight :: Sing (Either a0 b0) z0

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a0, b0) z0

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a0, b0, c0) z0

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a0, b0, c0, d0) z0

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a0, b0, c0, d0, e0) z0

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a0, b0, c0, d0, e0, f0) z0

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

type SPos = (Sing :: Pos -> Type)

type PosC p = SingI p

Kind-restricted synonym for SingI.

posType :: Int -> TypeQ

Template Haskell splice for the Pos type representing a given Int, e.g., $(posType 8).

posDec :: Int -> DecQ

Template Haskell splice that defines the Pos type synonym P\(n\).

reifyPos :: Int -> (forall p. SPos p -> a) -> a

Reify a Pos as a singleton.

reifyPosI :: Int -> (forall p proxy. PosC p => proxy p -> a) -> a

Reify a Pos for a SingI constraint.

posToInt :: C z => Pos -> z

Convert a Pos to an integral type.

intToPos :: C z => z -> Pos

Convert an integral type to a Pos.

addPos :: Pos -> Pos -> Pos

sAddPos :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply AddPosSym0 t) t :: Pos)

type family AddPos (a :: Pos) (a :: Pos) :: Pos where ...

Equations

AddPos O b = Apply SSym0 b

AddPos (S a) b = Apply (Apply ($$) SSym0) (Apply (Apply AddPosSym0 a) b)

subPos :: Pos -> Pos -> Pos

sSubPos :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply SubPosSym0 t) t :: Pos)

type family SubPos (a :: Pos) (a :: Pos) :: Pos where ...

Equations

SubPos (S a) O = a

SubPos (S a) (S b) = Apply (Apply SubPosSym0 a) b

SubPos O _z_1627625799 = Apply ErrorSym0 "Invalid call to subPos: a <= b"

type OSym0 = O

data SSym0 l

Instances

SuppressUnusedWarnings (TyFun Pos Pos -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type Apply Pos Pos SSym0 l0

type Apply Pos Pos SSym0 l0 = SSym1 l0

type SSym1 t = S t

data AddPosSym0 l

Instances

SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> Type) -> *) AddPosSym0

Methods

suppressUnusedWarnings :: Proxy AddPosSym0 t -> ()

type Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0

type Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0 = AddPosSym1 l0

data AddPosSym1 l l

Instances

SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) AddPosSym1

Methods

suppressUnusedWarnings :: Proxy AddPosSym1 t -> ()

type Apply Pos Pos (AddPosSym1 l1) l0

type Apply Pos Pos (AddPosSym1 l1) l0

data SubPosSym0 l

Instances

SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> Type) -> *) SubPosSym0

Methods

suppressUnusedWarnings :: Proxy SubPosSym0 t -> ()

type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0

type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0 = SubPosSym1 l0

data SubPosSym1 l l

Instances

SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) SubPosSym1

Methods

suppressUnusedWarnings :: Proxy SubPosSym1 t -> ()

type Apply Pos Pos (SubPosSym1 l1) l0

type Apply Pos Pos (SubPosSym1 l1) l0

Positive naturals in binary representation

data Bin

Constructors

B1

D0 Bin

D1 Bin

Instances

Eq Bin

Methods

(==) :: Bin -> Bin -> Bool

(/=) :: Bin -> Bin -> Bool

Ord Bin

Methods

compare :: Bin -> Bin -> Ordering

(<) :: Bin -> Bin -> Bool

(<=) :: Bin -> Bin -> Bool

(>) :: Bin -> Bin -> Bool

(>=) :: Bin -> Bin -> Bool

max :: Bin -> Bin -> Bin

min :: Bin -> Bin -> Bin

Show Bin

Methods

showsPrec :: Int -> Bin -> ShowS

show :: Bin -> String

showList :: [Bin] -> ShowS

SOrd Bin

Methods

sCompare :: Sing Bin t0 -> Sing Bin t1 -> Sing Ordering (Apply Bin Ordering (Apply Bin (TyFun Bin Ordering -> Type) (CompareSym0 Bin) t0) t1)

(%:<) :: Sing Bin t0 -> Sing Bin t1 -> Sing Bool (Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) ((:<$) Bin) t0) t1)

(%:<=) :: Sing Bin t0 -> Sing Bin t1 -> Sing Bool (Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) ((:<=$) Bin) t0) t1)

(%:>) :: Sing Bin t0 -> Sing Bin t1 -> Sing Bool (Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) ((:>$) Bin) t0) t1)

(%:>=) :: Sing Bin t0 -> Sing Bin t1 -> Sing Bool (Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) ((:>=$) Bin) t0) t1)

sMax :: Sing Bin t0 -> Sing Bin t1 -> Sing Bin (Apply Bin Bin (Apply Bin (TyFun Bin Bin -> Type) (MaxSym0 Bin) t0) t1)

sMin :: Sing Bin t0 -> Sing Bin t1 -> Sing Bin (Apply Bin Bin (Apply Bin (TyFun Bin Bin -> Type) (MinSym0 Bin) t0) t1)

SEq Bin

Methods

(%:==) :: Sing Bin a -> Sing Bin b -> Sing Bool ((Bin :== a) b)

(%:/=) :: Sing Bin a -> Sing Bin b -> Sing Bool ((Bin :/= a) b)

SDecide Bin

Methods

(%~) :: Sing Bin a -> Sing Bin b -> Decision ((Bin :~: a) b)

SingKind Bin

Associated Types

type DemoteRep Bin :: *

Methods

fromSing :: Sing Bin a -> DemoteRep Bin

toSing :: DemoteRep Bin -> SomeSing Bin

SingI Bin B1

Methods

sing :: Sing B1 a

SingI Bin n0 => SingI Bin (D0 n0)

Methods

sing :: Sing (D0 n0) a

SingI Bin n0 => SingI Bin (D1 n0)

Methods

sing :: Sing (D1 n0) a

POrd Bin (Proxy * Bin)

Associated Types

type Compare (Proxy * Bin) (arg0 :: Proxy * Bin) (arg1 :: Proxy * Bin) :: Ordering

type ((Proxy * Bin) :< (arg0 :: Proxy * Bin)) (arg1 :: Proxy * Bin) :: Bool

type ((Proxy * Bin) :<= (arg0 :: Proxy * Bin)) (arg1 :: Proxy * Bin) :: Bool

type ((Proxy * Bin) :> (arg0 :: Proxy * Bin)) (arg1 :: Proxy * Bin) :: Bool

type ((Proxy * Bin) :>= (arg0 :: Proxy * Bin)) (arg1 :: Proxy * Bin) :: Bool

type Max (Proxy * Bin) (arg0 :: Proxy * Bin) (arg1 :: Proxy * Bin) :: a0

type Min (Proxy * Bin) (arg0 :: Proxy * Bin) (arg1 :: Proxy * Bin) :: a0

PEq Bin (Proxy * Bin)

Associated Types

type ((Proxy * Bin) :== (x :: Proxy * Bin)) (y :: Proxy * Bin) :: Bool

type ((Proxy * Bin) :/= (x :: Proxy * Bin)) (y :: Proxy * Bin) :: Bool

SuppressUnusedWarnings (TyFun Bin Bin -> *) D1Sym0

Methods

suppressUnusedWarnings :: Proxy D1Sym0 t -> ()

SuppressUnusedWarnings (TyFun Bin Bin -> *) D0Sym0

Methods

suppressUnusedWarnings :: Proxy D0Sym0 t -> ()

data Sing Bin

data Sing Bin where

• SB1 :: Sing Bin z
• SD0 :: Sing Bin z
• SD1 :: Sing Bin z

type DemoteRep Bin

type DemoteRep Bin = Bin

type Min Bin arg0 arg1

type Min Bin arg0 arg1 = Apply Bin Bin (Apply Bin (TyFun Bin Bin -> Type) (Min_1627688153Sym0 Bin) arg0) arg1

type Max Bin arg0 arg1

type Max Bin arg0 arg1 = Apply Bin Bin (Apply Bin (TyFun Bin Bin -> Type) (Max_1627688120Sym0 Bin) arg0) arg1

type (:>=) Bin arg0 arg1

type (:>=) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627688087Sym0 Bin) arg0) arg1

type (:>) Bin arg0 arg1

type (:>) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627688054Sym0 Bin) arg0) arg1

type (:<=) Bin arg0 arg1

type (:<=) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627688021Sym0 Bin) arg0) arg1

type (:<) Bin arg0 arg1

type (:<) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627687988Sym0 Bin) arg0) arg1

type Compare Bin a1 a0

type Compare Bin a1 a0

type (:/=) Bin x y

type (:/=) Bin x y = Not ((:==) Bin x y)

type (:==) Bin a0 b0

type (:==) Bin a0 b0

type Apply Bin Bin D1Sym0 l0

type Apply Bin Bin D1Sym0 l0 = D1Sym1 l0

type Apply Bin Bin D0Sym0 l0

type Apply Bin Bin D0Sym0 l0 = D0Sym1 l0

data family Sing k (a :: k) :: *

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z0
• STrue :: Sing Bool z0

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z0
• SEQ :: Sing Ordering z0
• SGT :: Sing Ordering z0

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z0

data Sing Pos

data Sing Pos where

• SO :: Sing Pos z
• SS :: Sing Pos z

data Sing Bin

data Sing Bin where

• SB1 :: Sing Bin z
• SD0 :: Sing Bin z
• SD1 :: Sing Bin z

data Sing PrimeBin

data Sing PrimeBin where

• SP :: Sing PrimeBin z

data Sing PrimePower

data Sing PrimePower where

• SPP :: Sing PrimePower z

data Sing Factored

data Sing Factored where

• SF :: Sing Factored z

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a0] z0
• SCons :: Sing [a0] z0

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a0) z0
• SJust :: Sing (Maybe a0) z0

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a0) z0

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a0 b0) z0
• SRight :: Sing (Either a0 b0) z0

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a0, b0) z0

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a0, b0, c0) z0

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a0, b0, c0, d0) z0

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a0, b0, c0, d0, e0) z0

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a0, b0, c0, d0, e0, f0) z0

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

type SBin = (Sing :: Bin -> Type)

type BinC b = SingI b

Kind-restricted synonym for SingI.

binType :: Int -> TypeQ

Template Haskell splice for the Bin type representing a given Int, e.g., $(binType 89).

binDec :: Int -> DecQ

Template Haskell splice that defines the Bin type synonym B\(n\).

reifyBin :: Int -> (forall b. SBin b -> a) -> a

Reify a Bin as a singleton.

reifyBinI :: Int -> (forall b proxy. BinC b => proxy b -> a) -> a

Reify a Bin for a SingI constraint.

binToInt :: C z => Bin -> z

Convert a Bin to an integral type.

intToBin :: C z => z -> Bin

Convert an integral type to a Bin.

type B1Sym0 = B1

data D0Sym0 l

Instances

SuppressUnusedWarnings (TyFun Bin Bin -> *) D0Sym0

Methods

suppressUnusedWarnings :: Proxy D0Sym0 t -> ()

type Apply Bin Bin D0Sym0 l0

type Apply Bin Bin D0Sym0 l0 = D0Sym1 l0

type D0Sym1 t = D0 t

data D1Sym0 l

Instances

SuppressUnusedWarnings (TyFun Bin Bin -> *) D1Sym0

Methods

suppressUnusedWarnings :: Proxy D1Sym0 t -> ()

type Apply Bin Bin D1Sym0 l0

type Apply Bin Bin D1Sym0 l0 = D1Sym1 l0

type D1Sym1 t = D1 t

Miscellaneous

intDec

Arguments

:: String

pfx

-> (Int -> TypeQ)

f

-> Int

n

-> DecQ

Template Haskell splice that declares a type synonym <pfx>\(n\) as the type f n.

primes :: [Int]

Infinite list of primes, built using Sieve of Erastothenes.

prime :: Int -> Bool

Search for the argument in primes. This is not particularly fast, but works well enough for moderate-sized numbers that would appear as (divisors of) cyclotomic indices of interest.

Convenient synonyms for Pos and Bin types

type P1 = O

type P2 = S O

type P3 = S (S O)

type P4 = S (S (S O))

type P5 = S (S (S (S O)))

type P6 = S (S (S (S (S O))))

type P7 = S (S (S (S (S (S O)))))

type P8 = S (S (S (S (S (S (S O))))))

type P9 = S (S (S (S (S (S (S (S O)))))))

type P10 = S (S (S (S (S (S (S (S (S O))))))))

type P11 = S (S (S (S (S (S (S (S (S (S O)))))))))

type P12 = S (S (S (S (S (S (S (S (S (S (S O))))))))))

type P13 = S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))

type P14 = S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))

type P15 = S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))

type P16 = S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))

type B1 = B1

type B2 = D0 B1

type B3 = D1 B1

type B4 = D0 (D0 B1)

type B5 = D1 (D0 B1)

type B6 = D0 (D1 B1)

type B7 = D1 (D1 B1)

type B8 = D0 (D0 (D0 B1))

type B9 = D1 (D0 (D0 B1))

type B10 = D0 (D1 (D0 B1))

type B11 = D1 (D1 (D0 B1))

type B12 = D0 (D0 (D1 B1))

type B13 = D1 (D0 (D1 B1))

type B14 = D0 (D1 (D1 B1))

type B15 = D1 (D1 (D1 B1))

type B16 = D0 (D0 (D0 (D0 B1)))

type B17 = D1 (D0 (D0 (D0 B1)))

type B18 = D0 (D1 (D0 (D0 B1)))

type B19 = D1 (D1 (D0 (D0 B1)))

type B20 = D0 (D0 (D1 (D0 B1)))

type B21 = D1 (D0 (D1 (D0 B1)))

type B22 = D0 (D1 (D1 (D0 B1)))

type B23 = D1 (D1 (D1 (D0 B1)))

type B24 = D0 (D0 (D0 (D1 B1)))

type B25 = D1 (D0 (D0 (D1 B1)))

type B26 = D0 (D1 (D0 (D1 B1)))

type B27 = D1 (D1 (D0 (D1 B1)))

type B28 = D0 (D0 (D1 (D1 B1)))

type B29 = D1 (D0 (D1 (D1 B1)))

type B30 = D0 (D1 (D1 (D1 B1)))

type B31 = D1 (D1 (D1 (D1 B1)))

type B32 = D0 (D0 (D0 (D0 (D0 B1))))

type B33 = D1 (D0 (D0 (D0 (D0 B1))))

type B34 = D0 (D1 (D0 (D0 (D0 B1))))

type B35 = D1 (D1 (D0 (D0 (D0 B1))))

type B36 = D0 (D0 (D1 (D0 (D0 B1))))

type B37 = D1 (D0 (D1 (D0 (D0 B1))))

type B38 = D0 (D1 (D1 (D0 (D0 B1))))

type B39 = D1 (D1 (D1 (D0 (D0 B1))))

type B40 = D0 (D0 (D0 (D1 (D0 B1))))

type B41 = D1 (D0 (D0 (D1 (D0 B1))))

type B42 = D0 (D1 (D0 (D1 (D0 B1))))

type B43 = D1 (D1 (D0 (D1 (D0 B1))))

type B44 = D0 (D0 (D1 (D1 (D0 B1))))

type B45 = D1 (D0 (D1 (D1 (D0 B1))))

type B46 = D0 (D1 (D1 (D1 (D0 B1))))

type B47 = D1 (D1 (D1 (D1 (D0 B1))))

type B48 = D0 (D0 (D0 (D0 (D1 B1))))

type B49 = D1 (D0 (D0 (D0 (D1 B1))))

type B50 = D0 (D1 (D0 (D0 (D1 B1))))

type B51 = D1 (D1 (D0 (D0 (D1 B1))))

type B52 = D0 (D0 (D1 (D0 (D1 B1))))

type B53 = D1 (D0 (D1 (D0 (D1 B1))))

type B54 = D0 (D1 (D1 (D0 (D1 B1))))

type B55 = D1 (D1 (D1 (D0 (D1 B1))))

type B56 = D0 (D0 (D0 (D1 (D1 B1))))

type B57 = D1 (D0 (D0 (D1 (D1 B1))))

type B58 = D0 (D1 (D0 (D1 (D1 B1))))

type B59 = D1 (D1 (D0 (D1 (D1 B1))))

type B60 = D0 (D0 (D1 (D1 (D1 B1))))

type B61 = D1 (D0 (D1 (D1 (D1 B1))))

type B62 = D0 (D1 (D1 (D1 (D1 B1))))

type B63 = D1 (D1 (D1 (D1 (D1 B1))))

type B64 = D0 (D0 (D0 (D0 (D0 (D0 B1)))))

type B65 = D1 (D0 (D0 (D0 (D0 (D0 B1)))))

type B66 = D0 (D1 (D0 (D0 (D0 (D0 B1)))))

type B67 = D1 (D1 (D0 (D0 (D0 (D0 B1)))))

type B68 = D0 (D0 (D1 (D0 (D0 (D0 B1)))))

type B69 = D1 (D0 (D1 (D0 (D0 (D0 B1)))))

type B70 = D0 (D1 (D1 (D0 (D0 (D0 B1)))))

type B71 = D1 (D1 (D1 (D0 (D0 (D0 B1)))))

type B72 = D0 (D0 (D0 (D1 (D0 (D0 B1)))))

type B73 = D1 (D0 (D0 (D1 (D0 (D0 B1)))))

type B74 = D0 (D1 (D0 (D1 (D0 (D0 B1)))))

type B75 = D1 (D1 (D0 (D1 (D0 (D0 B1)))))

type B76 = D0 (D0 (D1 (D1 (D0 (D0 B1)))))

type B77 = D1 (D0 (D1 (D1 (D0 (D0 B1)))))

type B78 = D0 (D1 (D1 (D1 (D0 (D0 B1)))))

type B79 = D1 (D1 (D1 (D1 (D0 (D0 B1)))))

type B80 = D0 (D0 (D0 (D0 (D1 (D0 B1)))))

type B81 = D1 (D0 (D0 (D0 (D1 (D0 B1)))))

type B82 = D0 (D1 (D0 (D0 (D1 (D0 B1)))))

type B83 = D1 (D1 (D0 (D0 (D1 (D0 B1)))))

type B84 = D0 (D0 (D1 (D0 (D1 (D0 B1)))))

type B85 = D1 (D0 (D1 (D0 (D1 (D0 B1)))))

type B86 = D0 (D1 (D1 (D0 (D1 (D0 B1)))))

type B87 = D1 (D1 (D1 (D0 (D1 (D0 B1)))))

type B88 = D0 (D0 (D0 (D1 (D1 (D0 B1)))))

type B89 = D1 (D0 (D0 (D1 (D1 (D0 B1)))))

type B90 = D0 (D1 (D0 (D1 (D1 (D0 B1)))))

type B91 = D1 (D1 (D0 (D1 (D1 (D0 B1)))))

type B92 = D0 (D0 (D1 (D1 (D1 (D0 B1)))))

type B93 = D1 (D0 (D1 (D1 (D1 (D0 B1)))))

type B94 = D0 (D1 (D1 (D1 (D1 (D0 B1)))))

type B95 = D1 (D1 (D1 (D1 (D1 (D0 B1)))))

type B96 = D0 (D0 (D0 (D0 (D0 (D1 B1)))))

type B97 = D1 (D0 (D0 (D0 (D0 (D1 B1)))))

type B98 = D0 (D1 (D0 (D0 (D0 (D1 B1)))))

type B99 = D1 (D1 (D0 (D0 (D0 (D1 B1)))))

type B100 = D0 (D0 (D1 (D0 (D0 (D1 B1)))))

type B101 = D1 (D0 (D1 (D0 (D0 (D1 B1)))))

type B102 = D0 (D1 (D1 (D0 (D0 (D1 B1)))))

type B103 = D1 (D1 (D1 (D0 (D0 (D1 B1)))))

type B104 = D0 (D0 (D0 (D1 (D0 (D1 B1)))))

type B105 = D1 (D0 (D0 (D1 (D0 (D1 B1)))))

type B106 = D0 (D1 (D0 (D1 (D0 (D1 B1)))))

type B107 = D1 (D1 (D0 (D1 (D0 (D1 B1)))))

type B108 = D0 (D0 (D1 (D1 (D0 (D1 B1)))))

type B109 = D1 (D0 (D1 (D1 (D0 (D1 B1)))))

type B110 = D0 (D1 (D1 (D1 (D0 (D1 B1)))))

type B111 = D1 (D1 (D1 (D1 (D0 (D1 B1)))))

type B112 = D0 (D0 (D0 (D0 (D1 (D1 B1)))))

type B113 = D1 (D0 (D0 (D0 (D1 (D1 B1)))))

type B114 = D0 (D1 (D0 (D0 (D1 (D1 B1)))))

type B115 = D1 (D1 (D0 (D0 (D1 (D1 B1)))))

type B116 = D0 (D0 (D1 (D0 (D1 (D1 B1)))))

type B117 = D1 (D0 (D1 (D0 (D1 (D1 B1)))))

type B118 = D0 (D1 (D1 (D0 (D1 (D1 B1)))))

type B119 = D1 (D1 (D1 (D0 (D1 (D1 B1)))))

type B120 = D0 (D0 (D0 (D1 (D1 (D1 B1)))))

type B121 = D1 (D0 (D0 (D1 (D1 (D1 B1)))))

type B122 = D0 (D1 (D0 (D1 (D1 (D1 B1)))))

type B123 = D1 (D1 (D0 (D1 (D1 (D1 B1)))))

type B124 = D0 (D0 (D1 (D1 (D1 (D1 B1)))))

type B125 = D1 (D0 (D1 (D1 (D1 (D1 B1)))))

type B126 = D0 (D1 (D1 (D1 (D1 (D1 B1)))))

type B127 = D1 (D1 (D1 (D1 (D1 (D1 B1)))))

type B128 = D0 (D0 (D0 (D0 (D0 (D0 (D0 B1))))))

Convenient synonyms for Factored, PrimePower, and Prime types

type F1 = F '[]

type F2 = F '[PP '(P (D0 B1), O)]

type F3 = F '[PP '(P (D1 B1), O)]

type F4 = F '[PP '(P (D0 B1), S O)]

type F5 = F '[PP '(P (D1 (D0 B1)), O)]

type F6 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O)]

type F7 = F '[PP '(P (D1 (D1 B1)), O)]

type F8 = F '[PP '(P (D0 B1), S (S O))]

type F9 = F '[PP '(P (D1 B1), S O)]

type F10 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O)]

type F11 = F '[PP '(P (D1 (D1 (D0 B1))), O)]

type F12 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O)]

type F13 = F '[PP '(P (D1 (D0 (D1 B1))), O)]

type F14 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O)]

type F15 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)]

type F16 = F '[PP '(P (D0 B1), S (S (S O)))]

type F17 = F '[PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F18 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O)]

type F19 = F '[PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F20 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O)]

type F21 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)]

type F22 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F23 = F '[PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F24 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O)]

type F25 = F '[PP '(P (D1 (D0 B1)), S O)]

type F26 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F27 = F '[PP '(P (D1 B1), S (S O))]

type F28 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 B1)), O)]

type F29 = F '[PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F30 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)]

type F31 = F '[PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F32 = F '[PP '(P (D0 B1), S (S (S (S O))))]

type F33 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F34 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F35 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)]

type F36 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S O)]

type F37 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F38 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F39 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F40 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 B1)), O)]

type F41 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F42 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)]

type F43 = F '[PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F44 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 B1))), O)]

type F45 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O)]

type F46 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F47 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F48 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 B1), O)]

type F49 = F '[PP '(P (D1 (D1 B1)), S O)]

type F50 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), S O)]

type F51 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F52 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 B1))), O)]

type F53 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F54 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S (S O))]

type F55 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F56 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 B1)), O)]

type F57 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F58 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F59 = F '[PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)]

type F60 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)]

type F61 = F '[PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)]

type F62 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F63 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 B1)), O)]

type F64 = F '[PP '(P (D0 B1), S (S (S (S (S O)))))]

type F65 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F66 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F67 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)]

type F68 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F69 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F70 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)]

type F71 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)]

type F72 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), S O)]

type F73 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)]

type F74 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F75 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), S O)]

type F76 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F77 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F78 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F79 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)]

type F80 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D0 B1)), O)]

type F81 = F '[PP '(P (D1 B1), S (S (S O)))]

type F82 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F83 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)]

type F84 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)]

type F85 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F86 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F87 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F88 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D0 B1))), O)]

type F89 = F '[PP '(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)]

type F90 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O)]

type F91 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F92 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F93 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F94 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F95 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F96 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 B1), O)]

type F97 = F '[PP '(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)]

type F98 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), S O)]

type F99 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 B1))), O)]

type F100 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), S O)]

type F101 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)]

type F102 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F103 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))), O)]

type F104 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D1 B1))), O)]

type F105 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)]

type F106 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F107 = F '[PP '(P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))), O)]

type F108 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S (S O))]

type F109 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))), O)]

type F110 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F111 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F112 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D1 B1)), O)]

type F113 = F '[PP '(P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))), O)]

type F114 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F115 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F116 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F117 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D1 B1))), O)]

type F118 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)]

type F119 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F120 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)]

type F121 = F '[PP '(P (D1 (D1 (D0 B1))), S O)]

type F122 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)]

type F123 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F124 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F125 = F '[PP '(P (D1 (D0 B1)), S (S O))]

type F126 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D1 B1)), O)]

type F127 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))), O)]

type F128 = F '[PP '(P (D0 B1), S (S (S (S (S (S O))))))]

type F129 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F130 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F131 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))), O)]

type F132 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F133 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F134 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)]

type F135 = F '[PP '(P (D1 B1), S (S O)), PP '(P (D1 (D0 B1)), O)]

type F136 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F137 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))), O)]

type F138 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F139 = F '[PP '(P (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))), O)]

type F140 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)]

type F141 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F142 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)]

type F143 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F144 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 B1), S O)]

type F145 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F146 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)]

type F147 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), S O)]

type F148 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F149 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))), O)]

type F150 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), S O)]

type F151 = F '[PP '(P (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))), O)]

type F152 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F153 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F154 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F155 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F156 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F157 = F '[PP '(P (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))), O)]

type F158 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)]

type F159 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F160 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 (D0 B1)), O)]

type F161 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F162 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S (S (S O)))]

type F163 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))), O)]

type F164 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F165 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F166 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)]

type F167 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D1 (D0 B1))))))), O)]

type F168 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)]

type F169 = F '[PP '(P (D1 (D0 (D1 B1))), S O)]

type F170 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F171 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F172 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F173 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1))))))), O)]

type F174 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F175 = F '[PP '(P (D1 (D0 B1)), S O), PP '(P (D1 (D1 B1)), O)]

type F176 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D1 (D0 B1))), O)]

type F177 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)]

type F178 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)]

type F179 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1))))))), O)]

type F180 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O)]

type F181 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 (D1 (D0 B1))))))), O)]

type F182 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F183 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)]

type F184 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F185 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F186 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F187 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F188 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F189 = F '[PP '(P (D1 B1), S (S O)), PP '(P (D1 (D1 B1)), O)]

type F190 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F191 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1))))))), O)]

type F192 = F '[PP '(P (D0 B1), S (S (S (S (S O))))), PP '(P (D1 B1), O)]

type F193 = F '[PP '(P (D1 (D0 (D0 (D0 (D0 (D0 (D1 B1))))))), O)]

type F194 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)]

type F195 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F196 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 B1)), S O)]

type F197 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D0 (D1 B1))))))), O)]

type F198 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 B1))), O)]

type F199 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D0 (D1 B1))))))), O)]

type F200 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 B1)), S O)]

type F201 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)]

type F202 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)]

type F203 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F204 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F205 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F206 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))), O)]

type F207 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F208 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D0 (D1 B1))), O)]

type F209 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F210 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)]

type F211 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D0 (D1 B1))))))), O)]

type F212 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F213 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)]

type F214 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))), O)]

type F215 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F216 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), S (S O))]

type F217 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F218 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))), O)]

type F219 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)]

type F220 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F221 = F '[PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F222 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F223 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D0 (D1 B1))))))), O)]

type F224 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 (D1 B1)), O)]

type F225 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), S O)]

type F226 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))), O)]

type F227 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D1 (D1 B1))))))), O)]

type F228 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F229 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D1 (D1 B1))))))), O)]

type F230 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F231 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F232 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F233 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1))))))), O)]

type F234 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D1 B1))), O)]

type F235 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F236 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)]

type F237 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)]

type F238 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F239 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1))))))), O)]

type F240 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)]

type F241 = F '[PP '(P (D1 (D0 (D0 (D0 (D1 (D1 (D1 B1))))))), O)]

type F242 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 B1))), S O)]

type F243 = F '[PP '(P (D1 B1), S (S (S (S O))))]

type F244 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)]

type F245 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), S O)]

type F246 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F247 = F '[PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F248 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F249 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)]

type F250 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), S (S O))]

type F251 = F '[PP '(P (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1))))))), O)]

type F252 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S O), PP '(P (D1 (D1 B1)), O)]

type F253 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F254 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))), O)]

type F255 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F256 = F '[PP '(P (D0 B1), S (S (S (S (S (S (S O)))))))]

type F257 = F '[PP '(P (D1 (D0 (D0 (D0 (D0 (D0 (D0 (D0 B1)))))))), O)]

type F258 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F259 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F260 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F261 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F262 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))), O)]

type F263 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1)))))))), O)]

type F264 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F265 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F266 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F267 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)]

type F268 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)]

type F269 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D0 B1)))))))), O)]

type F270 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S (S O)), PP '(P (D1 (D0 B1)), O)]

type F271 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 (D0 (D0 (D0 B1)))))))), O)]

type F272 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F273 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F274 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))), O)]

type F275 = F '[PP '(P (D1 (D0 B1)), S O), PP '(P (D1 (D1 (D0 B1))), O)]

type F276 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F277 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 (D0 (D0 (D0 B1)))))))), O)]

type F278 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))), O)]

type F279 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F280 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)]

type F281 = F '[PP '(P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D0 B1)))))))), O)]

type F282 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F283 = F '[PP '(P (D1 (D1 (D0 (D1 (D1 (D0 (D0 (D0 B1)))))))), O)]

type F284 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)]

type F285 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F286 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F287 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F288 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 B1), S O)]

type F289 = F '[PP '(P (D1 (D0 (D0 (D0 B1)))), S O)]

type F290 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F291 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)]

type F292 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)]

type F293 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D0 B1)))))))), O)]

type F294 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), S O)]

type F295 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)]

type F296 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F297 = F '[PP '(P (D1 B1), S (S O)), PP '(P (D1 (D1 (D0 B1))), O)]

type F298 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))), O)]

type F299 = F '[PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F300 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), S O)]

type F301 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F302 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))), O)]

type F303 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)]

type F304 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F305 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)]

type F306 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F307 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D1 (D0 (D0 B1)))))))), O)]

type F308 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F309 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))), O)]

type F310 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F311 = F '[PP '(P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D0 B1)))))))), O)]

type F312 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F313 = F '[PP '(P (D1 (D0 (D0 (D1 (D1 (D1 (D0 (D0 B1)))))))), O)]

type F314 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))), O)]

type F315 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)]

type F316 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)]

type F317 = F '[PP '(P (D1 (D0 (D1 (D1 (D1 (D1 (D0 (D0 B1)))))))), O)]

type F318 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F319 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F320 = F '[PP '(P (D0 B1), S (S (S (S (S O))))), PP '(P (D1 (D0 B1)), O)]

type F321 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))), O)]

type F322 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F323 = F '[PP '(P (D1 (D0 (D0 (D0 B1)))), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F324 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S (S (S O)))]

type F325 = F '[PP '(P (D1 (D0 B1)), S O), PP '(P (D1 (D0 (D1 B1))), O)]

type F326 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))), O)]

type F327 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))), O)]

type F328 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F329 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F330 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F331 = F '[PP '(P (D1 (D1 (D0 (D1 (D0 (D0 (D1 (D0 B1)))))))), O)]

type F332 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)]

type F333 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F334 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D1 (D0 B1))))))), O)]

type F335 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)]

type F336 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)]

type F337 = F '[PP '(P (D1 (D0 (D0 (D0 (D1 (D0 (D1 (D0 B1)))))))), O)]

type F338 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 B1))), S O)]

type F339 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))), O)]

type F340 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F341 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F342 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F343 = F '[PP '(P (D1 (D1 B1)), S (S O))]

type F344 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F345 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F346 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1))))))), O)]

type F347 = F '[PP '(P (D1 (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1)))))))), O)]

type F348 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F349 = F '[PP '(P (D1 (D0 (D1 (D1 (D1 (D0 (D1 (D0 B1)))))))), O)]

type F350 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), S O), PP '(P (D1 (D1 B1)), O)]

type F351 = F '[PP '(P (D1 B1), S (S O)), PP '(P (D1 (D0 (D1 B1))), O)]

type F352 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 (D1 (D0 B1))), O)]

type F353 = F '[PP '(P (D1 (D0 (D0 (D0 (D0 (D1 (D1 (D0 B1)))))))), O)]

type F354 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)]

type F355 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)]

type F356 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)]

type F357 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F358 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1))))))), O)]

type F359 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1)))))))), O)]

type F360 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O)]

type F361 = F '[PP '(P (D1 (D1 (D0 (D0 B1)))), S O)]

type F362 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D1 (D1 (D0 B1))))))), O)]

type F363 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), S O)]

type F364 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F365 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)]

type F366 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)]

type F367 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 (D1 (D1 (D0 B1)))))))), O)]

type F368 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F369 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F370 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F371 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F372 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F373 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 (D1 (D1 (D0 B1)))))))), O)]

type F374 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F375 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), S (S O))]

type F376 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F377 = F '[PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F378 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S (S O)), PP '(P (D1 (D1 B1)), O)]

type F379 = F '[PP '(P (D1 (D1 (D0 (D1 (D1 (D1 (D1 (D0 B1)))))))), O)]

type F380 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F381 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))), O)]

type F382 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1))))))), O)]

type F383 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1)))))))), O)]

type F384 = F '[PP '(P (D0 B1), S (S (S (S (S (S O)))))), PP '(P (D1 B1), O)]

type F385 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F386 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D0 (D0 (D0 (D1 B1))))))), O)]

type F387 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F388 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)]

type F389 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D0 (D0 (D1 B1)))))))), O)]

type F390 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F391 = F '[PP '(P (D1 (D0 (D0 (D0 B1)))), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F392 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 B1)), S O)]

type F393 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))), O)]

type F394 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 (D0 (D1 B1))))))), O)]

type F395 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)]

type F396 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 B1))), O)]

type F397 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D1 B1)))))))), O)]

type F398 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 (D1 B1))))))), O)]

type F399 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F400 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D0 B1)), S O)]

type F401 = F '[PP '(P (D1 (D0 (D0 (D0 (D1 (D0 (D0 (D1 B1)))))))), O)]

type F402 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)]

type F403 = F '[PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F404 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)]

type F405 = F '[PP '(P (D1 B1), S (S (S O))), PP '(P (D1 (D0 B1)), O)]

type F406 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F407 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F408 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F409 = F '[PP '(P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D1 B1)))))))), O)]

type F410 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F411 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))), O)]

type F412 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))), O)]

type F413 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)]

type F414 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F415 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)]

type F416 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 (D0 (D1 B1))), O)]

type F417 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))), O)]

type F418 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F419 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D1 (D0 (D1 B1)))))))), O)]

type F420 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)]

type F421 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D1 B1)))))))), O)]

type F422 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D1 (D0 (D1 B1))))))), O)]

type F423 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F424 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F425 = F '[PP '(P (D1 (D0 B1)), S O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F426 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)]

type F427 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)]

type F428 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))), O)]

type F429 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F430 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F431 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 (D1 (D0 (D1 B1)))))))), O)]

type F432 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 B1), S (S O))]

type F433 = F '[PP '(P (D1 (D0 (D0 (D0 (D1 (D1 (D0 (D1 B1)))))))), O)]

type F434 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F435 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F436 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))), O)]

type F437 = F '[PP '(P (D1 (D1 (D0 (D0 B1)))), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F438 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)]

type F439 = F '[PP '(P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D1 B1)))))))), O)]

type F440 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F441 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 B1)), S O)]

type F442 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F443 = F '[PP '(P (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D1 B1)))))))), O)]

type F444 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F445 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)]

type F446 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 (D1 (D0 (D1 B1))))))), O)]

type F447 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))), O)]

type F448 = F '[PP '(P (D0 B1), S (S (S (S (S O))))), PP '(P (D1 (D1 B1)), O)]

type F449 = F '[PP '(P (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D1 B1)))))))), O)]

type F450 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), S O)]

type F451 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F452 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))), O)]

type F453 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))), O)]

type F454 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D1 (D1 B1))))))), O)]

type F455 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)]

type F456 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F457 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 (D0 (D1 (D1 B1)))))))), O)]

type F458 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 (D1 (D1 B1))))))), O)]

type F459 = F '[PP '(P (D1 B1), S (S O)), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F460 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F461 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D0 (D1 (D1 B1)))))))), O)]

type F462 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F463 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 (D0 (D1 (D1 B1)))))))), O)]

type F464 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F465 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F466 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1))))))), O)]

type F467 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1)))))))), O)]

type F468 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D1 B1))), O)]

type F469 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)]

type F470 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)]

type F471 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))), O)]

type F472 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)]

type F473 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)]

type F474 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)]

type F475 = F '[PP '(P (D1 (D0 B1)), S O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F476 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F477 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)]

type F478 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1))))))), O)]

type F479 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1)))))))), O)]

type F480 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)]

type F481 = F '[PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)]

type F482 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D0 (D1 (D1 (D1 B1))))))), O)]

type F483 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F484 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 B1))), S O)]

type F485 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)]

type F486 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S (S (S (S O))))]

type F487 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D1 B1)))))))), O)]

type F488 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)]

type F489 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))), O)]

type F490 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), S O)]

type F491 = F '[PP '(P (D1 (D1 (D0 (D1 (D0 (D1 (D1 (D1 B1)))))))), O)]

type F492 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)]

type F493 = F '[PP '(P (D1 (D0 (D0 (D0 B1)))), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)]

type F494 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)]

type F495 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)]

type F496 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D1 (D1 (D1 B1)))), O)]

type F497 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)]

type F498 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)]

type F499 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D1 (D1 (D1 B1)))))))), O)]

type F500 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), S (S O))]

type F501 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D1 (D0 B1))))))), O)]

type F502 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1))))))), O)]

type F503 = F '[PP '(P (D1 (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1)))))))), O)]

type F504 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), S O), PP '(P (D1 (D1 B1)), O)]

type F505 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)]

type F506 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)]

type F507 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 B1))), S O)]

type F508 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))), O)]

type F509 = F '[PP '(P (D1 (D0 (D1 (D1 (D1 (D1 (D1 (D1 B1)))))))), O)]

type F510 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)]

type F511 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)]

type F512 = F '[PP '(P (D0 B1), S (S (S (S (S (S (S (S O))))))))]

type F1024 = F '[PP '(P (D0 B1), S (S (S (S (S (S (S (S (S O)))))))))]

type F2048 = F '[PP '(P (D0 B1), S (S (S (S (S (S (S (S (S (S O))))))))))]

type PP2 = PP '(P (D0 B1), O)

type PP4 = PP '(P (D0 B1), S O)

type PP8 = PP '(P (D0 B1), S (S O))

type PP16 = PP '(P (D0 B1), S (S (S O)))

type PP32 = PP '(P (D0 B1), S (S (S (S O))))

type PP64 = PP '(P (D0 B1), S (S (S (S (S O)))))

type PP128 = PP '(P (D0 B1), S (S (S (S (S (S O))))))

type PP3 = PP '(P (D1 B1), O)

type PP9 = PP '(P (D1 B1), S O)

type PP27 = PP '(P (D1 B1), S (S O))

type PP81 = PP '(P (D1 B1), S (S (S O)))

type PP5 = PP '(P (D1 (D0 B1)), O)

type PP7 = PP '(P (D1 (D1 B1)), O)

type PP11 = PP '(P (D1 (D1 (D0 B1))), O)

type Prime2 = P (D0 B1)

type Prime3 = P (D1 B1)

type Prime5 = P (D1 (D0 B1))

type Prime7 = P (D1 (D1 B1))

type Prime11 = P (D1 (D1 (D0 B1)))

type Prime13 = P (D1 (D0 (D1 B1)))

type Prime17 = P (D1 (D0 (D0 (D0 B1))))

type Prime19 = P (D1 (D1 (D0 (D0 B1))))

type Prime23 = P (D1 (D1 (D1 (D0 B1))))

type Prime29 = P (D1 (D0 (D1 (D1 B1))))

type Prime31 = P (D1 (D1 (D1 (D1 B1))))

type Prime37 = P (D1 (D0 (D1 (D0 (D0 B1)))))

type Prime41 = P (D1 (D0 (D0 (D1 (D0 B1)))))

type Prime43 = P (D1 (D1 (D0 (D1 (D0 B1)))))

type Prime47 = P (D1 (D1 (D1 (D1 (D0 B1)))))

type Prime53 = P (D1 (D0 (D1 (D0 (D1 B1)))))

type Prime59 = P (D1 (D1 (D0 (D1 (D1 B1)))))

type Prime61 = P (D1 (D0 (D1 (D1 (D1 B1)))))

type Prime67 = P (D1 (D1 (D0 (D0 (D0 (D0 B1))))))

type Prime71 = P (D1 (D1 (D1 (D0 (D0 (D0 B1))))))

type Prime73 = P (D1 (D0 (D0 (D1 (D0 (D0 B1))))))

type Prime79 = P (D1 (D1 (D1 (D1 (D0 (D0 B1))))))

type Prime83 = P (D1 (D1 (D0 (D0 (D1 (D0 B1))))))

type Prime89 = P (D1 (D0 (D0 (D1 (D1 (D0 B1))))))

type Prime97 = P (D1 (D0 (D0 (D0 (D0 (D1 B1))))))

type Prime101 = P (D1 (D0 (D1 (D0 (D0 (D1 B1))))))

type Prime103 = P (D1 (D1 (D1 (D0 (D0 (D1 B1))))))

type Prime107 = P (D1 (D1 (D0 (D1 (D0 (D1 B1))))))

type Prime109 = P (D1 (D0 (D1 (D1 (D0 (D1 B1))))))

type Prime113 = P (D1 (D0 (D0 (D0 (D1 (D1 B1))))))

type Prime127 = P (D1 (D1 (D1 (D1 (D1 (D1 B1))))))

type Prime131 = P (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1)))))))

type Prime137 = P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1)))))))

type Prime139 = P (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1)))))))

type Prime149 = P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1)))))))

type Prime151 = P (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1)))))))

type Prime157 = P (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1)))))))

type Prime163 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1)))))))

type Prime167 = P (D1 (D1 (D1 (D0 (D0 (D1 (D0 B1)))))))

type Prime173 = P (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1)))))))

type Prime179 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1)))))))

type Prime181 = P (D1 (D0 (D1 (D0 (D1 (D1 (D0 B1)))))))

type Prime191 = P (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1)))))))

type Prime193 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 B1)))))))

type Prime197 = P (D1 (D0 (D1 (D0 (D0 (D0 (D1 B1)))))))

type Prime199 = P (D1 (D1 (D1 (D0 (D0 (D0 (D1 B1)))))))

type Prime211 = P (D1 (D1 (D0 (D0 (D1 (D0 (D1 B1)))))))

type Prime223 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 B1)))))))

type Prime227 = P (D1 (D1 (D0 (D0 (D0 (D1 (D1 B1)))))))

type Prime229 = P (D1 (D0 (D1 (D0 (D0 (D1 (D1 B1)))))))

type Prime233 = P (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1)))))))

type Prime239 = P (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1)))))))

type Prime241 = P (D1 (D0 (D0 (D0 (D1 (D1 (D1 B1)))))))

type Prime251 = P (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1)))))))

type Prime257 = P (D1 (D0 (D0 (D0 (D0 (D0 (D0 (D0 B1))))))))

type Prime263 = P (D1 (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))))

type Prime269 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D0 B1))))))))

type Prime271 = P (D1 (D1 (D1 (D1 (D0 (D0 (D0 (D0 B1))))))))

type Prime277 = P (D1 (D0 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))))

type Prime281 = P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D0 B1))))))))

type Prime283 = P (D1 (D1 (D0 (D1 (D1 (D0 (D0 (D0 B1))))))))

type Prime293 = P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D0 B1))))))))

type Prime307 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 (D0 B1))))))))

type Prime311 = P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D0 B1))))))))

type Prime313 = P (D1 (D0 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))))

type Prime317 = P (D1 (D0 (D1 (D1 (D1 (D1 (D0 (D0 B1))))))))

type Prime331 = P (D1 (D1 (D0 (D1 (D0 (D0 (D1 (D0 B1))))))))

type Prime337 = P (D1 (D0 (D0 (D0 (D1 (D0 (D1 (D0 B1))))))))

type Prime347 = P (D1 (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1))))))))

type Prime349 = P (D1 (D0 (D1 (D1 (D1 (D0 (D1 (D0 B1))))))))

type Prime353 = P (D1 (D0 (D0 (D0 (D0 (D1 (D1 (D0 B1))))))))

type Prime359 = P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1))))))))

type Prime367 = P (D1 (D1 (D1 (D1 (D0 (D1 (D1 (D0 B1))))))))

type Prime373 = P (D1 (D0 (D1 (D0 (D1 (D1 (D1 (D0 B1))))))))

type Prime379 = P (D1 (D1 (D0 (D1 (D1 (D1 (D1 (D0 B1))))))))

type Prime383 = P (D1 (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1))))))))

type Prime389 = P (D1 (D0 (D1 (D0 (D0 (D0 (D0 (D1 B1))))))))

type Prime397 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D1 B1))))))))

type Prime401 = P (D1 (D0 (D0 (D0 (D1 (D0 (D0 (D1 B1))))))))

type Prime409 = P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D1 B1))))))))

type Prime419 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 (D1 B1))))))))

type Prime421 = P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D1 B1))))))))

type Prime431 = P (D1 (D1 (D1 (D1 (D0 (D1 (D0 (D1 B1))))))))

type Prime433 = P (D1 (D0 (D0 (D0 (D1 (D1 (D0 (D1 B1))))))))

type Prime439 = P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D1 B1))))))))

type Prime443 = P (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D1 B1))))))))

type Prime449 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D1 B1))))))))

type Prime457 = P (D1 (D0 (D0 (D1 (D0 (D0 (D1 (D1 B1))))))))

type Prime461 = P (D1 (D0 (D1 (D1 (D0 (D0 (D1 (D1 B1))))))))

type Prime463 = P (D1 (D1 (D1 (D1 (D0 (D0 (D1 (D1 B1))))))))

type Prime467 = P (D1 (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1))))))))

type Prime479 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1))))))))

type Prime487 = P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D1 B1))))))))

type Prime491 = P (D1 (D1 (D0 (D1 (D0 (D1 (D1 (D1 B1))))))))

type Prime499 = P (D1 (D1 (D0 (D0 (D1 (D1 (D1 (D1 B1))))))))

type Prime503 = P (D1 (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1))))))))

type Prime509 = P (D1 (D0 (D1 (D1 (D1 (D1 (D1 (D1 B1))))))))

type Prime521 = P (D1 (D0 (D0 (D1 (D0 (D0 (D0 (D0 (D0 B1)))))))))

type Prime523 = P (D1 (D1 (D0 (D1 (D0 (D0 (D0 (D0 (D0 B1)))))))))

type Prime541 = P (D1 (D0 (D1 (D1 (D1 (D0 (D0 (D0 (D0 B1)))))))))

type Prime547 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 (D0 (D0 B1)))))))))

type Prime557 = P (D1 (D0 (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1)))))))))

type Prime563 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D0 B1)))))))))

type Prime569 = P (D1 (D0 (D0 (D1 (D1 (D1 (D0 (D0 (D0 B1)))))))))

type Prime571 = P (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D0 (D0 B1)))))))))

type Prime577 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D0 (D0 B1)))))))))

type Prime587 = P (D1 (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D0 B1)))))))))

type Prime593 = P (D1 (D0 (D0 (D0 (D1 (D0 (D1 (D0 (D0 B1)))))))))

type Prime599 = P (D1 (D1 (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1)))))))))

type Prime601 = P (D1 (D0 (D0 (D1 (D1 (D0 (D1 (D0 (D0 B1)))))))))

type Prime607 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1)))))))))

type Prime613 = P (D1 (D0 (D1 (D0 (D0 (D1 (D1 (D0 (D0 B1)))))))))

type Prime617 = P (D1 (D0 (D0 (D1 (D0 (D1 (D1 (D0 (D0 B1)))))))))

type Prime619 = P (D1 (D1 (D0 (D1 (D0 (D1 (D1 (D0 (D0 B1)))))))))

type Prime631 = P (D1 (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1)))))))))

type Prime641 = P (D1 (D0 (D0 (D0 (D0 (D0 (D0 (D1 (D0 B1)))))))))

type Prime643 = P (D1 (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D0 B1)))))))))

type Prime647 = P (D1 (D1 (D1 (D0 (D0 (D0 (D0 (D1 (D0 B1)))))))))

type Prime653 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1)))))))))

type Prime659 = P (D1 (D1 (D0 (D0 (D1 (D0 (D0 (D1 (D0 B1)))))))))