Safe Haskell	None
Language	Haskell2010

Crypto.Lol.Factored

Contents

Factored natural numbers
Prime powers
Primes
Constructors
Unwrappers
Arithmetic operations
Convenient reflections
Number-theoretic laws
Utility operations on prime powers
Re-export
Convenient synonyms for Factored, PrimePower, and Prime types

Description

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.

Synopsis

Factored natural numbers

data Factored Source

Instances

Eq Factored Source
Show Factored Source
(Fact m, C i) => Reflects Factored m i Source
SEq Factored (KProxy Factored) Source
PEq Factored (KProxy Factored) Source
SDecide Factored (KProxy Factored) Source
SingKind Factored (KProxy Factored) Source
(Ring r, Fact m, UCElt t r) => C r (UCyc Factored t m C r)
(Ring r, Tensor t, Fact m, TElt t r) => C r (UCyc Factored t m D r)
(Ring r, Tensor t, Fact m, TElt t r) => C r (UCyc Factored t m P r)
(Random r, Tensor t, Fact m, CRTElt t r) => Random (Either (UCyc Factored t m P r) (UCyc Factored t m C r))
(GFCtx k fp d, Fact m, UCElt t fp) => C (GF k fp d) (UCyc Factored t m P fp)
(Tensor t, Fact m) => Functor (UCyc Factored t m D)
(Tensor t, Fact m) => Functor (UCyc Factored t m P)
(Tensor t, Fact m) => Applicative (UCyc Factored t m D)
(Tensor t, Fact m) => Applicative (UCyc Factored t m P)
(Tensor t, Fact m) => Foldable (UCyc Factored t m D)
(Tensor t, Fact m) => Foldable (UCyc Factored t m P)
(Tensor t, Fact m) => Traversable (UCyc Factored t m D)
(Tensor t, Fact m) => Traversable (UCyc Factored t m P)
(Eq r, Fact m, UCElt t r) => Eq (UCyc Factored t m C r)
(Eq r, Tensor t, Fact m, TElt t r) => Eq (UCyc Factored t m D r)
(Eq r, Tensor t, Fact m, TElt t r) => Eq (UCyc Factored t m P r)
(Show r, Show (CRTExt r), Tensor t, Fact m, TElt t r, TElt t (CRTExt r)) => Show (UCyc Factored t m rep r)
(Tensor t, Fact m, NFElt r, TElt t r, TElt t (CRTExt r)) => NFData (UCyc Factored t m rep r)
(Fact m, UCElt t r) => C (UCyc Factored t m C r)
(ZeroTestable r, Fact m, UCElt t r) => C (UCyc Factored t m C r)
(ZeroTestable r, Tensor t, Fact m, TElt t r) => C (UCyc Factored t m D r)
(ZeroTestable r, Tensor t, Fact m, TElt t r) => C (UCyc Factored t m P r)
(Fact m, UCElt t r) => C (UCyc Factored t m C r)
(Additive r, Tensor t, Fact m, TElt t r) => C (UCyc Factored t m D r)
(Additive r, Tensor t, Fact m, TElt t r) => C (UCyc Factored t m P r)
(Lift' r, Tensor t, Fact m, TElt t r, TElt t (LiftOf r)) => Lift' (UCyc Factored t m D r) Source
(Lift' r, Tensor t, Fact m, TElt t r, TElt t (LiftOf r)) => Lift' (UCyc Factored t m P r) Source
(Rescale a b, Tensor t, Fact m, TElt t a, TElt t b) => Rescale (UCyc Factored t m D a) (UCyc Factored t m D b) Source
(Rescale a b, Tensor t, Fact m, TElt t a, TElt t b) => Rescale (UCyc Factored t m P a) (UCyc Factored t m P b) Source
(Reduce a b, Tensor t, Fact m, TElt t a, TElt t b) => Reduce (UCyc Factored t m D a) (UCyc Factored t m D b) Source
(Reduce a b, Tensor t, Fact m, TElt t a, TElt t b) => Reduce (UCyc Factored t m P a) (UCyc Factored t m P b) Source
data Sing Factored where SF :: (~) Factored z (F n) => Sing [PrimePower] n -> Sing Factored z Source
type (:/=) Factored x y = Not ((:==) Factored x y)
type (:==) Factored a0 b0 Source
type DemoteRep Factored (KProxy Factored) = Factored Source

type SFactored = (Sing :: Factored -> *) Source

type Fact m = SingI m Source

Kind-restricted synonym for SingI.

fType :: Int -> TypeQ Source

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 Source

Template Haskell splice that defines the Factored type synonym Fn for a positive integer n.

Prime powers

data PrimePower Source

Instances

Eq PrimePower Source
Show PrimePower Source
(PPow pp, C i) => Reflects PrimePower pp i Source
SEq PrimePower (KProxy PrimePower) Source
PEq PrimePower (KProxy PrimePower) Source
SDecide PrimePower (KProxy PrimePower) Source
SingKind PrimePower (KProxy PrimePower) Source
(PPow pp, (~) * zq (ZqBasic PrimePower pp z), PrimeField (ZpOf zq), Ring zq, Ring (ZpOf zq)) => ZPP (ZqBasic PrimePower pp z) Source
data Sing PrimePower where SPP :: (~) PrimePower z (PP n) => Sing ((,) Prime Pos) n -> Sing PrimePower z Source
type (:/=) PrimePower x y = Not ((:==) PrimePower x y)
type (:==) PrimePower a0 b0 Source
type DemoteRep PrimePower (KProxy PrimePower) = PrimePower Source
type ZpOf (ZqBasic PrimePower pp z) = ZqBasic Prime (PrimePP pp) z Source

type SPrimePower = (Sing :: PrimePower -> *) Source

data family Sing a

The singleton kind-indexed data family.

Instances

data Sing Bool where SFalse :: (~) Bool z0 False => Sing Bool z0 STrue :: (~) Bool z0 True => Sing Bool z0
data Sing Ordering where SLT :: (~) Ordering z0 LT => Sing Ordering z0 SEQ :: (~) Ordering z0 EQ => Sing Ordering z0 SGT :: (~) Ordering z0 GT => Sing Ordering z0
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z0 () => Sing () z0
data Sing Pos where SO :: (~) Pos z O => Sing Pos z SS :: (~) Pos z (S n) => Sing Pos n -> Sing Pos z
data Sing Bin where SB1 :: (~) Bin z B1 => Sing Bin z SD0 :: (~) Bin z (D0 n) => Sing Bin n -> Sing Bin z SD1 :: (~) Bin z (D1 n) => Sing Bin n -> Sing Bin z
data Sing Prime where SP :: (~) Prime z (P n) => Sing Bin n -> Sing Prime z
data Sing PrimePower where SPP :: (~) PrimePower z (PP n) => Sing ((,) Prime Pos) n -> Sing PrimePower z
data Sing Factored where SF :: (~) Factored z (F n) => Sing [PrimePower] n -> Sing Factored z
data Sing [a0] where SNil :: (~) [a0] z0 ([] a0) => Sing [a0] z0 SCons :: (~) [a0] z0 ((:) a0 n0 n1) => Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0
data Sing (Maybe a0) where SNothing :: (~) (Maybe a0) z0 (Nothing a0) => Sing (Maybe a0) z0 SJust :: (~) (Maybe a0) z0 (Just a0 n0) => Sing a0 n0 -> Sing (Maybe a0) z0
data Sing (TyFun k1 k2 -> *) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t) }
data Sing (Either a0 b0) where SLeft :: (~) (Either a0 b0) z0 (Left a0 b0 n0) => Sing a0 n0 -> Sing (Either a0 b0) z0 SRight :: (~) (Either a0 b0) z0 (Right a0 b0 n0) => Sing b0 n0 -> Sing (Either a0 b0) z0
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a0 b0) z0 ((,) a0 b0 n0 n1) => Sing a0 n0 -> Sing b0 n1 -> Sing ((,) a0 b0) z0
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a0 b0 c0) z0 ((,,) a0 b0 c0 n0 n1 n2) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing ((,,) a0 b0 c0) z0
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a0 b0 c0 d0) z0 ((,,,) a0 b0 c0 d0 n0 n1 n2 n3) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing ((,,,) a0 b0 c0 d0) z0
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0

type PPow pp = SingI pp Source

Kind-restricted synonym for SingI.

ppType :: PP -> TypeQ Source

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 Source

Template Haskell splice that defines the PrimePower type synonym PPn, where n=p^e.

Primes

data Prime Source

Instances

Eq Prime Source
Ord Prime Source
Show Prime Source
(Prim p, C i) => Reflects Prime p i Source
POrd Prime (KProxy Prime) Source
SOrd Bin (KProxy Bin) => SOrd Prime (KProxy Prime) Source
SEq Prime (KProxy Prime) Source
PEq Prime (KProxy Prime) Source
SDecide Prime (KProxy Prime) Source
SingKind Prime (KProxy Prime) Source
data Sing Prime where SP :: (~) Prime z (P n) => Sing Bin n -> Sing Prime z Source
type Min Prime arg0 arg1 = Apply Prime Prime (Apply (TyFun Prime Prime -> *) Prime (Min_1627641717Sym0 Prime) arg0) arg1
type Max Prime arg0 arg1 = Apply Prime Prime (Apply (TyFun Prime Prime -> *) Prime (Max_1627641684Sym0 Prime) arg0) arg1
type (:>=) Prime arg0 arg1 = Apply Bool Prime (Apply (TyFun Prime Bool -> *) Prime (TFHelper_1627641651Sym0 Prime) arg0) arg1
type (:>) Prime arg0 arg1 = Apply Bool Prime (Apply (TyFun Prime Bool -> *) Prime (TFHelper_1627641618Sym0 Prime) arg0) arg1
type (:<=) Prime arg0 arg1 = Apply Bool Prime (Apply (TyFun Prime Bool -> *) Prime (TFHelper_1627641585Sym0 Prime) arg0) arg1
type (:<) Prime arg0 arg1 = Apply Bool Prime (Apply (TyFun Prime Bool -> *) Prime (TFHelper_1627641552Sym0 Prime) arg0) arg1
type Compare Prime a0 a1 Source
type (:/=) Prime x y = Not ((:==) Prime x y)
type (:==) Prime a0 b0 Source
type DemoteRep Prime (KProxy Prime) = Prime Source

type SPrime = (Sing :: Prime -> *) Source

type Prim p = SingI p Source

Kind-restricted synonym for SingI.

pType :: Int -> TypeQ Source

Template Haskell splice for the Prime 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 Prime type (and is used to define the Primep type synonyms).

pDec :: Int -> DecQ Source

Template Haskell splice that defines the Prime type synonym Primep for a positive prime integer p.

Constructors

pToPP :: Prime -> PrimePower Source

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

type family PToPP a :: PrimePower Source

Equations

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

ppToF :: PrimePower -> Factored Source

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

type family PpToF a :: Factored Source

Equations

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

pToF :: Prime -> Factored Source

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

type family PToF a :: Factored Source

Equations

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

Unwrappers

unF :: Factored -> [PrimePower] Source

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

type family UnF a :: [PrimePower] Source

Equations

UnF (F pps) = pps

unPP :: PrimePower -> (Prime, Pos) Source

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

type family UnPP a :: (Prime, Pos) Source

Equations

UnPP (PP pp) = pp

primePP :: PrimePower -> Prime Source

type family PrimePP a :: Prime Source

Equations

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

exponentPP :: PrimePower -> Pos Source

type family ExponentPP a :: Pos Source

Equations

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

Arithmetic operations

fPPMul :: PrimePower -> Factored -> Factored Source

type family FPPMul a a :: Factored Source

Equations

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

fMul :: Factored -> Factored -> Factored Source

type family FMul a a :: Factored Source

Equations

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

type * a b = FMul a b Source

Type (family) synonym for multiplication of Factored types

fDivides :: Factored -> Factored -> Bool Source

type family FDivides a a :: Bool Source

Equations

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

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

Constraint synonym for divisibility of Factored types.

fDiv :: Factored -> Factored -> Factored Source

type family FDiv a a :: Factored Source

Equations

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

type (/) a b = FDiv a b Source

Type (family) synonym for division of Factored types

fGCD :: Factored -> Factored -> Factored Source

type family FGCD a a :: Factored Source

Equations

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

fLCM :: Factored -> Factored -> Factored Source

type family FLCM a a :: Factored Source

Equations

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

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

Constraint synonym for coprimality of Factored types.

fOddRadical :: Factored -> Factored Source

type family FOddRadical a :: Factored Source

Equations

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

pFree :: Prime -> Factored -> Factored Source

type family PFree a a :: Factored Source

Equations

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

Convenient reflections

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

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

valueFact :: Fact m => Tagged m Int Source

The value of a Factored type.

totientFact :: Fact m => Tagged m Int Source

The totient of a Factored type's value.

valueHatFact :: Fact m => Tagged m Int Source

The "hat" of a Factored type's value: hat{m} is m if m is odd, and m/2 otherwise.

radicalFact :: Fact m => Tagged m Int Source

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

oddRadicalFact :: Fact m => Tagged m Int Source

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

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

Reflect a PrimePower type to a PP value.

primePPow :: PPow pp => Tagged pp Int Source

Reflect the prime component of a PrimePower type.

exponentPPow :: PPow pp => Tagged pp Int Source

Reflect the exponent component of a PrimePower type.

valuePPow :: PPow pp => Tagged pp Int Source

The value of a PrimePower type.

totientPPow :: PPow pp => Tagged pp Int Source

The totient of a PrimePower type's value.

valuePrime :: forall p. Prim p => Tagged p Int Source

The value of a Prime type.

Number-theoretic laws

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

Entails constraint for transitivity of division, i.e. if k|l and l|m, then k|m.

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

Entailment for divisibility by GCD: if g=GCD(m1,m2) then g|m1 and g|m2.

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

Entailment for LCM divisibility: if l=LCM(m1,m2) then m1|l and m2|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) Source

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

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

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

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

Entailment for p-free division: if m|m', then p-free(m) | 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 Source

Return m if m is odd, and m/2 otherwise.

type PP = (Int, Int) Source

Type synonym for (prime, exponent) pair.

ppToPP :: PrimePower -> PP Source

Conversion.

valuePP :: PP -> Int Source

The value of a prime power.

totientPP :: PP -> Int Source

Totient of a prime power.

radicalPP :: PP -> Int Source

The radical of a prime power.

oddRadicalPP :: PP -> Int Source

The odd radical of a prime power.

valuePPs :: [PP] -> Int Source

Product of values of individual PPs

totientPPs :: [PP] -> Int Source

Product of totients of individual PPs

radicalPPs :: [PP] -> Int Source

Product of radicals of individual PPs

oddRadicalPPs :: [PP] -> Int Source

Product of odd radicals of individual PPs

Re-export

module Crypto.Lol.PosBin

Convenient synonyms for `Factored`, `PrimePower`, and `Prime` types

type F1 = F `[]` Source

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)`]` Source

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)`]` Source

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type F376 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 (D1 (D1 (D1 (D0 B1))))), O)`]` Source

type F377 = F `[PP `(P (D1 (D0 (D1 B1))), O)`, PP `(P (D1 (D0 (D1 (D1 B1)))), O)`]` Source

type F378 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), S (S O))`, PP `(P (D1 (D1 B1)), O)`]` Source

type F379 = F `[PP `(P (D1 (D1 (D0 (D1 (D1 (D1 (D1 (D0 B1)))))))), O)`]` Source

type F380 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D0 (D0 B1)))), O)`]` Source

type F381 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))), O)`]` Source

type F382 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1))))))), O)`]` Source

type F383 = F `[PP `(P (D1 (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1)))))))), O)`]` Source

type F384 = F `[PP `(P (D0 B1), S (S (S (S (S (S O))))))`, PP `(P (D1 B1), O)`]` Source

type F385 = F `[PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D1 (D0 B1))), O)`]` Source

type F386 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 (D0 (D0 (D0 (D0 (D1 B1))))))), O)`]` Source

type F387 = F `[PP `(P (D1 B1), S O)`, PP `(P (D1 (D1 (D0 (D1 (D0 B1))))), O)`]` Source

type F388 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)`]` Source

type F389 = F `[PP `(P (D1 (D0 (D1 (D0 (D0 (D0 (D0 (D1 B1)))))))), O)`]` Source

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)`]` Source

type F391 = F `[PP `(P (D1 (D0 (D0 (D0 B1)))), O)`, PP `(P (D1 (D1 (D1 (D0 B1)))), O)`]` Source

type F392 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 (D1 B1)), S O)`]` Source

type F393 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))), O)`]` Source

type F394 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 (D1 (D0 (D0 (D0 (D1 B1))))))), O)`]` Source

type F395 = F `[PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)`]` Source

type F396 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 B1), S O)`, PP `(P (D1 (D1 (D0 B1))), O)`]` Source

type F397 = F `[PP `(P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D1 B1)))))))), O)`]` Source

type F398 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D1 (D0 (D0 (D0 (D1 B1))))))), O)`]` Source

type F399 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D1 (D0 (D0 B1)))), O)`]` Source

type F400 = F `[PP `(P (D0 B1), S (S (S O)))`, PP `(P (D1 (D0 B1)), S O)`]` Source

type F401 = F `[PP `(P (D1 (D0 (D0 (D0 (D1 (D0 (D0 (D1 B1)))))))), O)`]` Source

type F402 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)`]` Source

type F403 = F `[PP `(P (D1 (D0 (D1 B1))), O)`, PP `(P (D1 (D1 (D1 (D1 B1)))), O)`]` Source

type F404 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)`]` Source

type F405 = F `[PP `(P (D1 B1), S (S (S O)))`, PP `(P (D1 (D0 B1)), O)`]` Source

type F406 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D0 (D1 (D1 B1)))), O)`]` Source

type F407 = F `[PP `(P (D1 (D1 (D0 B1))), O)`, PP `(P (D1 (D0 (D1 (D0 (D0 B1))))), O)`]` Source

type F408 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 B1), O)`, PP `(P (D1 (D0 (D0 (D0 B1)))), O)`]` Source

type F409 = F `[PP `(P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D1 B1)))))))), O)`]` Source

type F410 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D0 (D0 (D1 (D0 B1))))), O)`]` Source

type F411 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))), O)`]` Source

type F412 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))), O)`]` Source

type F413 = F `[PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D1 (D0 (D1 (D1 B1))))), O)`]` Source

type F414 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), S O)`, PP `(P (D1 (D1 (D1 (D0 B1)))), O)`]` Source

type F415 = F `[PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)`]` Source

type F416 = F `[PP `(P (D0 B1), S (S (S (S O))))`, PP `(P (D1 (D0 (D1 B1))), O)`]` Source

type F417 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))), O)`]` Source

type F418 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D0 B1))), O)`, PP `(P (D1 (D1 (D0 (D0 B1)))), O)`]` Source

type F419 = F `[PP `(P (D1 (D1 (D0 (D0 (D0 (D1 (D0 (D1 B1)))))))), O)`]` Source

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)`]` Source

type F421 = F `[PP `(P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D1 B1)))))))), O)`]` Source

type F422 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D0 (D0 (D1 (D0 (D1 B1))))))), O)`]` Source

type F423 = F `[PP `(P (D1 B1), S O)`, PP `(P (D1 (D1 (D1 (D1 (D0 B1))))), O)`]` Source

type F424 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 (D0 (D1 (D0 (D1 B1))))), O)`]` Source

type F425 = F `[PP `(P (D1 (D0 B1)), S O)`, PP `(P (D1 (D0 (D0 (D0 B1)))), O)`]` Source

type F426 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)`]` Source

type F427 = F `[PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D0 (D1 (D1 (D1 B1))))), O)`]` Source

type F428 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))), O)`]` Source

type F429 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D0 B1))), O)`, PP `(P (D1 (D0 (D1 B1))), O)`]` Source

type F430 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D0 (D1 (D0 B1))))), O)`]` Source

type F431 = F `[PP `(P (D1 (D1 (D1 (D1 (D0 (D1 (D0 (D1 B1)))))))), O)`]` Source

type F432 = F `[PP `(P (D0 B1), S (S (S O)))`, PP `(P (D1 B1), S (S O))`]` Source

type F433 = F `[PP `(P (D1 (D0 (D0 (D0 (D1 (D1 (D0 (D1 B1)))))))), O)`]` Source

type F434 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D1 (D1 (D1 B1)))), O)`]` Source

type F435 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D0 (D1 (D1 B1)))), O)`]` Source

type F436 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))), O)`]` Source

type F437 = F `[PP `(P (D1 (D1 (D0 (D0 B1)))), O)`, PP `(P (D1 (D1 (D1 (D0 B1)))), O)`]` Source

type F438 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), O)`, PP `(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)`]` Source

type F439 = F `[PP `(P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D1 B1)))))))), O)`]` Source

type F440 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D0 B1))), O)`]` Source

type F441 = F `[PP `(P (D1 B1), S O)`, PP `(P (D1 (D1 B1)), S O)`]` Source

type F442 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 (D1 B1))), O)`, PP `(P (D1 (D0 (D0 (D0 B1)))), O)`]` Source

type F443 = F `[PP `(P (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D1 B1)))))))), O)`]` Source

type F444 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 B1), O)`, PP `(P (D1 (D0 (D1 (D0 (D0 B1))))), O)`]` Source

type F445 = F `[PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)`]` Source

type F446 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D1 (D1 (D1 (D0 (D1 B1))))))), O)`]` Source

type F447 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))), O)`]` Source

type F448 = F `[PP `(P (D0 B1), S (S (S (S (S O)))))`, PP `(P (D1 (D1 B1)), O)`]` Source

type F449 = F `[PP `(P (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D1 B1)))))))), O)`]` Source

type F450 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), S O)`, PP `(P (D1 (D0 B1)), S O)`]` Source

type F451 = F `[PP `(P (D1 (D1 (D0 B1))), O)`, PP `(P (D1 (D0 (D0 (D1 (D0 B1))))), O)`]` Source

type F452 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))), O)`]` Source

type F453 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))), O)`]` Source

type F454 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D0 (D0 (D0 (D1 (D1 B1))))))), O)`]` Source

type F455 = F `[PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D0 (D1 B1))), O)`]` Source

type F456 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D0 (D0 B1)))), O)`]` Source

type F457 = F `[PP `(P (D1 (D0 (D0 (D1 (D0 (D0 (D1 (D1 B1)))))))), O)`]` Source

type F458 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 (D1 (D0 (D0 (D1 (D1 B1))))))), O)`]` Source

type F459 = F `[PP `(P (D1 B1), S (S O))`, PP `(P (D1 (D0 (D0 (D0 B1)))), O)`]` Source

type F460 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D1 (D0 B1)))), O)`]` Source

type F461 = F `[PP `(P (D1 (D0 (D1 (D1 (D0 (D0 (D1 (D1 B1)))))))), O)`]` Source

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)`]` Source

type F463 = F `[PP `(P (D1 (D1 (D1 (D1 (D0 (D0 (D1 (D1 B1)))))))), O)`]` Source

type F464 = F `[PP `(P (D0 B1), S (S (S O)))`, PP `(P (D1 (D0 (D1 (D1 B1)))), O)`]` Source

type F465 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D1 (D1 B1)))), O)`]` Source

type F466 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1))))))), O)`]` Source

type F467 = F `[PP `(P (D1 (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1)))))))), O)`]` Source

type F468 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 B1), S O)`, PP `(P (D1 (D0 (D1 B1))), O)`]` Source

type F469 = F `[PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)`]` Source

type F470 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D1 (D1 (D0 B1))))), O)`]` Source

type F471 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))), O)`]` Source

type F472 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 (D1 (D0 (D1 (D1 B1))))), O)`]` Source

type F473 = F `[PP `(P (D1 (D1 (D0 B1))), O)`, PP `(P (D1 (D1 (D0 (D1 (D0 B1))))), O)`]` Source

type F474 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)`]` Source

type F475 = F `[PP `(P (D1 (D0 B1)), S O)`, PP `(P (D1 (D1 (D0 (D0 B1)))), O)`]` Source

type F476 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D0 (D0 (D0 B1)))), O)`]` Source

type F477 = F `[PP `(P (D1 B1), S O)`, PP `(P (D1 (D0 (D1 (D0 (D1 B1))))), O)`]` Source

type F478 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1))))))), O)`]` Source

type F479 = F `[PP `(P (D1 (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1)))))))), O)`]` Source

type F480 = F `[PP `(P (D0 B1), S (S (S (S O))))`, PP `(P (D1 B1), O)`, PP `(P (D1 (D0 B1)), O)`]` Source

type F481 = F `[PP `(P (D1 (D0 (D1 B1))), O)`, PP `(P (D1 (D0 (D1 (D0 (D0 B1))))), O)`]` Source

type F482 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 (D0 (D0 (D1 (D1 (D1 B1))))))), O)`]` Source

type F483 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D1 (D1 (D0 B1)))), O)`]` Source

type F484 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D1 (D0 B1))), S O)`]` Source

type F485 = F `[PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)`]` Source

type F486 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), S (S (S (S O))))`]` Source

type F487 = F `[PP `(P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D1 B1)))))))), O)`]` Source

type F488 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 (D0 (D1 (D1 (D1 B1))))), O)`]` Source

type F489 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))), O)`]` Source

type F490 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 B1)), S O)`]` Source

type F491 = F `[PP `(P (D1 (D1 (D0 (D1 (D0 (D1 (D1 (D1 B1)))))))), O)`]` Source

type F492 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 B1), O)`, PP `(P (D1 (D0 (D0 (D1 (D0 B1))))), O)`]` Source

type F493 = F `[PP `(P (D1 (D0 (D0 (D0 B1)))), O)`, PP `(P (D1 (D0 (D1 (D1 B1)))), O)`]` Source

type F494 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D0 (D1 B1))), O)`, PP `(P (D1 (D1 (D0 (D0 B1)))), O)`]` Source

type F495 = F `[PP `(P (D1 B1), S O)`, PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D1 (D0 B1))), O)`]` Source

type F496 = F `[PP `(P (D0 B1), S (S (S O)))`, PP `(P (D1 (D1 (D1 (D1 B1)))), O)`]` Source

type F497 = F `[PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)`]` Source

type F498 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)`]` Source

type F499 = F `[PP `(P (D1 (D1 (D0 (D0 (D1 (D1 (D1 (D1 B1)))))))), O)`]` Source

type F500 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D0 B1)), S (S O))`]` Source

type F501 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D1 (D1 (D0 (D0 (D1 (D0 B1))))))), O)`]` Source

type F502 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1))))))), O)`]` Source

type F503 = F `[PP `(P (D1 (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1)))))))), O)`]` Source

type F504 = F `[PP `(P (D0 B1), S (S O))`, PP `(P (D1 B1), S O)`, PP `(P (D1 (D1 B1)), O)`]` Source

type F505 = F `[PP `(P (D1 (D0 B1)), O)`, PP `(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)`]` Source

type F506 = F `[PP `(P (D0 B1), O)`, PP `(P (D1 (D1 (D0 B1))), O)`, PP `(P (D1 (D1 (D1 (D0 B1)))), O)`]` Source

type F507 = F `[PP `(P (D1 B1), O)`, PP `(P (D1 (D0 (D1 B1))), S O)`]` Source

type F508 = F `[PP `(P (D0 B1), S O)`, PP `(P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))), O)`]` Source

type F509 = F `[PP `(P (D1 (D0 (D1 (D1 (D1 (D1 (D1 (D1 B1)))))))), O)`]` Source

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)`]` Source

type F511 = F `[PP `(P (D1 (D1 B1)), O)`, PP `(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)`]` Source

type F512 = F `[PP `(P (D0 B1), S (S (S (S (S (S (S (S O))))))))`]` Source

type F1024 = F `[PP `(P (D0 B1), S (S (S (S (S (S (S (S (S O)))))))))`]` Source

type F2048 = F `[PP `(P (D0 B1), S (S (S (S (S (S (S (S (S (S O))))))))))`]` Source

type PP2 = PP `(P (D0 B1), O)` Source

type PP4 = PP `(P (D0 B1), S O)` Source

type PP8 = PP `(P (D0 B1), S (S O))` Source

type PP16 = PP `(P (D0 B1), S (S (S O)))` Source

type PP32 = PP `(P (D0 B1), S (S (S (S O))))` Source

type PP64 = PP `(P (D0 B1), S (S (S (S (S O)))))` Source

type PP128 = PP `(P (D0 B1), S (S (S (S (S (S O))))))` Source

type PP3 = PP `(P (D1 B1), O)` Source

type PP9 = PP `(P (D1 B1), S O)` Source

type PP27 = PP `(P (D1 B1), S (S O))` Source

type PP81 = PP `(P (D1 B1), S (S (S O)))` Source

type PP5 = PP `(P (D1 (D0 B1)), O)` Source

type PP7 = PP `(P (D1 (D1 B1)), O)` Source

type PP11 = PP `(P (D1 (D1 (D0 B1))), O)` Source

type Prime2 = P (D0 B1) Source

type Prime3 = P (D1 B1) Source

type Prime5 = P (D1 (D0 B1)) Source

type Prime7 = P (D1 (D1 B1)) Source

type Prime11 = P (D1 (D1 (D0 B1))) Source

type Prime13 = P (D1 (D0 (D1 B1))) Source

type Prime17 = P (D1 (D0 (D0 (D0 B1)))) Source

type Prime19 = P (D1 (D1 (D0 (D0 B1)))) Source

type Prime23 = P (D1 (D1 (D1 (D0 B1)))) Source

type Prime29 = P (D1 (D0 (D1 (D1 B1)))) Source

type Prime31 = P (D1 (D1 (D1 (D1 B1)))) Source

type Prime37 = P (D1 (D0 (D1 (D0 (D0 B1))))) Source

type Prime41 = P (D1 (D0 (D0 (D1 (D0 B1))))) Source

type Prime43 = P (D1 (D1 (D0 (D1 (D0 B1))))) Source

type Prime47 = P (D1 (D1 (D1 (D1 (D0 B1))))) Source

type Prime53 = P (D1 (D0 (D1 (D0 (D1 B1))))) Source

type Prime59 = P (D1 (D1 (D0 (D1 (D1 B1))))) Source

type Prime61 = P (D1 (D0 (D1 (D1 (D1 B1))))) Source

type Prime67 = P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))) Source

type Prime71 = P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))) Source

type Prime73 = P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))) Source

type Prime79 = P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))) Source

type Prime83 = P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))) Source

type Prime89 = P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))) Source

type Prime97 = P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))) Source

type Prime101 = P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))) Source

type Prime103 = P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))) Source

type Prime107 = P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))) Source

type Prime109 = P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))) Source

type Prime113 = P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))) Source

type Prime127 = P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))) Source

type Prime131 = P (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))) Source

type Prime137 = P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))) Source

type Prime139 = P (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))) Source

type Prime149 = P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))) Source

type Prime151 = P (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))) Source

type Prime157 = P (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))) Source

type Prime163 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))) Source

type Prime167 = P (D1 (D1 (D1 (D0 (D0 (D1 (D0 B1))))))) Source

type Prime173 = P (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1))))))) Source

type Prime179 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1))))))) Source

type Prime181 = P (D1 (D0 (D1 (D0 (D1 (D1 (D0 B1))))))) Source

type Prime191 = P (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1))))))) Source

type Prime193 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 B1))))))) Source

type Prime197 = P (D1 (D0 (D1 (D0 (D0 (D0 (D1 B1))))))) Source

type Prime199 = P (D1 (D1 (D1 (D0 (D0 (D0 (D1 B1))))))) Source

type Prime211 = P (D1 (D1 (D0 (D0 (D1 (D0 (D1 B1))))))) Source

type Prime223 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 B1))))))) Source

type Prime227 = P (D1 (D1 (D0 (D0 (D0 (D1 (D1 B1))))))) Source

type Prime229 = P (D1 (D0 (D1 (D0 (D0 (D1 (D1 B1))))))) Source

type Prime233 = P (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1))))))) Source

type Prime239 = P (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1))))))) Source

type Prime241 = P (D1 (D0 (D0 (D0 (D1 (D1 (D1 B1))))))) Source

type Prime251 = P (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1))))))) Source

type Prime257 = P (D1 (D0 (D0 (D0 (D0 (D0 (D0 (D0 B1)))))))) Source

type Prime263 = P (D1 (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1)))))))) Source

type Prime269 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D0 B1)))))))) Source

type Prime271 = P (D1 (D1 (D1 (D1 (D0 (D0 (D0 (D0 B1)))))))) Source

type Prime277 = P (D1 (D0 (D1 (D0 (D1 (D0 (D0 (D0 B1)))))))) Source

type Prime281 = P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D0 B1)))))))) Source

type Prime283 = P (D1 (D1 (D0 (D1 (D1 (D0 (D0 (D0 B1)))))))) Source

type Prime293 = P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D0 B1)))))))) Source

type Prime307 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 (D0 B1)))))))) Source

type Prime311 = P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D0 B1)))))))) Source

type Prime313 = P (D1 (D0 (D0 (D1 (D1 (D1 (D0 (D0 B1)))))))) Source

type Prime317 = P (D1 (D0 (D1 (D1 (D1 (D1 (D0 (D0 B1)))))))) Source

type Prime331 = P (D1 (D1 (D0 (D1 (D0 (D0 (D1 (D0 B1)))))))) Source

type Prime337 = P (D1 (D0 (D0 (D0 (D1 (D0 (D1 (D0 B1)))))))) Source

type Prime347 = P (D1 (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1)))))))) Source

type Prime349 = P (D1 (D0 (D1 (D1 (D1 (D0 (D1 (D0 B1)))))))) Source

type Prime353 = P (D1 (D0 (D0 (D0 (D0 (D1 (D1 (D0 B1)))))))) Source

type Prime359 = P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1)))))))) Source

type Prime367 = P (D1 (D1 (D1 (D1 (D0 (D1 (D1 (D0 B1)))))))) Source

type Prime373 = P (D1 (D0 (D1 (D0 (D1 (D1 (D1 (D0 B1)))))))) Source

type Prime379 = P (D1 (D1 (D0 (D1 (D1 (D1 (D1 (D0 B1)))))))) Source

type Prime383 = P (D1 (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1)))))))) Source

type Prime389 = P (D1 (D0 (D1 (D0 (D0 (D0 (D0 (D1 B1)))))))) Source

type Prime397 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D1 B1)))))))) Source

type Prime401 = P (D1 (D0 (D0 (D0 (D1 (D0 (D0 (D1 B1)))))))) Source

type Prime409 = P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D1 B1)))))))) Source

type Prime419 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 (D1 B1)))))))) Source

type Prime421 = P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D1 B1)))))))) Source

type Prime431 = P (D1 (D1 (D1 (D1 (D0 (D1 (D0 (D1 B1)))))))) Source

type Prime433 = P (D1 (D0 (D0 (D0 (D1 (D1 (D0 (D1 B1)))))))) Source

type Prime439 = P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D1 B1)))))))) Source

type Prime443 = P (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D1 B1)))))))) Source

type Prime449 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D1 B1)))))))) Source

type Prime457 = P (D1 (D0 (D0 (D1 (D0 (D0 (D1 (D1 B1)))))))) Source

type Prime461 = P (D1 (D0 (D1 (D1 (D0 (D0 (D1 (D1 B1)))))))) Source

type Prime463 = P (D1 (D1 (D1 (D1 (D0 (D0 (D1 (D1 B1)))))))) Source

type Prime467 = P (D1 (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1)))))))) Source

type Prime479 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1)))))))) Source

type Prime487 = P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D1 B1)))))))) Source

type Prime491 = P (D1 (D1 (D0 (D1 (D0 (D1 (D1 (D1 B1)))))))) Source

type Prime499 = P (D1 (D1 (D0 (D0 (D1 (D1 (D1 (D1 B1)))))))) Source

type Prime503 = P (D1 (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1)))))))) Source

type Prime509 = P (D1 (D0 (D1 (D1 (D1 (D1 (D1 (D1 B1)))))))) Source

type Prime521 = P (D1 (D0 (D0 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))))) Source

type Prime523 = P (D1 (D1 (D0 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))))) Source

type Prime541 = P (D1 (D0 (D1 (D1 (D1 (D0 (D0 (D0 (D0 B1))))))))) Source

type Prime547 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))))) Source

type Prime557 = P (D1 (D0 (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))))) Source

type Prime563 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D0 B1))))))))) Source

type Prime569 = P (D1 (D0 (D0 (D1 (D1 (D1 (D0 (D0 (D0 B1))))))))) Source

type Prime571 = P (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D0 (D0 B1))))))))) Source

type Prime577 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D0 (D0 B1))))))))) Source

type Prime587 = P (D1 (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D0 B1))))))))) Source

type Prime593 = P (D1 (D0 (D0 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))))) Source

type Prime599 = P (D1 (D1 (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))))) Source

type Prime601 = P (D1 (D0 (D0 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))))) Source

type Prime607 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))))) Source

type Prime613 = P (D1 (D0 (D1 (D0 (D0 (D1 (D1 (D0 (D0 B1))))))))) Source

type Prime617 = P (D1 (D0 (D0 (D1 (D0 (D1 (D1 (D0 (D0 B1))))))))) Source

type Prime619 = P (D1 (D1 (D0 (D1 (D0 (D1 (D1 (D0 (D0 B1))))))))) Source

type Prime631 = P (D1 (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))))) Source

type Prime641 = P (D1 (D0 (D0 (D0 (D0 (D0 (D0 (D1 (D0 B1))))))))) Source

type Prime643 = P (D1 (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D0 B1))))))))) Source

type Prime647 = P (D1 (D1 (D1 (D0 (D0 (D0 (D0 (D1 (D0 B1))))))))) Source

type Prime653 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))))) Source

type Prime659 = P (D1 (D1 (D0 (D0 (D1 (D0 (D0 (D1 (D0 B1))))))))) Source

Factored natural numbers

Prime powers

Primes

Constructors

Unwrappers

Arithmetic operations

Convenient reflections

Number-theoretic laws

Utility operations on prime powers

Re-export

Convenient synonyms for Factored, PrimePower, and Prime types

Convenient synonyms for `Factored`, `PrimePower`, and `Prime` types