Safe Haskell	None
Language	Haskell2010

Crypto.Lol.Factored

Contents

Factored natural numbers
Prime powers
Naturals
Constructors
Unwrappers
Arithmetic operations
Reflections
Number-theoretic laws
Utility operations (on prime powers)
Type synonyms (not type families)

Description

This file defines types and operations for type-level representation and manipulation of factored integers. It relies on TH, so the documentation will be difficult to read. See comments for better documentation.

Synopsis

Factored natural numbers

newtype Factored Source

Constructors

F [PrimePower]

Instances

Eq Factored Source
Show Factored Source
(Fact m, Integral i) => Reflects Factored m i Source
SingKind Factored (KProxy Factored) Source
SingI [PrimePower] n0 => SingI Factored (F n) Source
SEq Factored (KProxy Factored) Source
PEq Factored (KProxy Factored) Source
SDecide Factored (KProxy Factored) 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. Use this in constraints for types requiring a Factored type.

Prime powers

newtype PrimePower Source

Constructors

PP (Nat, Nat)

Instances

Eq PrimePower Source
Show PrimePower Source
(PPow pp, Integral i) => Reflects PrimePower pp i Source
SingKind PrimePower (KProxy PrimePower) Source
SingI ((,) Nat Nat) n0 => SingI PrimePower (PP n) Source
SEq PrimePower (KProxy PrimePower) Source
PEq PrimePower (KProxy PrimePower) Source
SDecide 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 ((,) Nat Nat) 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 Nat (PrimePP pp) z Source

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

type PPow pp = SingI pp Source

Kind-restricted synonym for SingI. Use this in constraints for types requiring a PrimePower type.

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 PrimePower where SPP :: (~) PrimePower z (PP n) => Sing ((,) Nat Nat) n -> Sing PrimePower z
data Sing Factored where SF :: (~) Factored z (F n) => Sing [PrimePower] n -> Sing Factored z
data Sing Nat where SZ :: (~) Nat z0 Z => Sing Nat z0 SS :: (~) Nat z0 (S n0) => Sing Nat n0 -> Sing Nat z0
type MonomorphicRep Nat (Sing Nat) = Int
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

Naturals

data Nat :: *

Instances

Eq Nat
Num Nat
Ord Nat
Show Nat
SingI Nat Z
(NatC a, Integral i) => Reflects Nat a i Source
SingKind Nat (KProxy Nat)
SingI Nat n0 => SingI Nat (S n0)
PNum Nat (KProxy Nat)
SNum Nat (KProxy Nat)
POrd Nat (KProxy Nat)
SOrd Nat (KProxy Nat)
SEq Nat (KProxy Nat)
PEq Nat (KProxy Nat)
SDecide Nat (KProxy Nat)
SuppressUnusedWarnings (TyFun Nat Nat -> *) FromInteger_1627442636Sym0
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> ) -> ) (:<<=$)
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> ) -> ) TFHelper_1627439035Sym0
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:**$)
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) TFHelper_1627442590Sym0
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) TFHelper_1627442565Sym0
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) TFHelper_1627442539Sym0
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) Min_1627439072Sym0
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) Max_1627439105Sym0
SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0
SuppressUnusedWarnings (TyFun Nat Nat -> *) Signum_1627442618Sym0
SuppressUnusedWarnings (TyFun Nat Nat -> *) Abs_1627442605Sym0
SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) (:<<=$$)
SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) TFHelper_1627439035Sym1
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> ) (:*$$)
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) TFHelper_1627442590Sym1
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) TFHelper_1627442565Sym1
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) TFHelper_1627442539Sym1
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) Min_1627439072Sym1
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) Max_1627439105Sym1
data Sing Nat where SZ :: (~) Nat z0 Z => Sing Nat z0 SS :: (~) Nat z0 (S n0) => Sing Nat n0 -> Sing Nat z0
type FromInteger Nat a0 = Apply Nat Nat FromInteger_1627442636Sym0 a0
type Signum Nat a0 = Apply Nat Nat Signum_1627442618Sym0 a0
type Abs Nat a0 = Apply Nat Nat Abs_1627442605Sym0 a0
type Negate Nat arg0 = Apply Nat Nat (Negate_1627753635Sym0 Nat) arg0
type (:) Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> ) Nat TFHelper_1627442590Sym0 a0) a1
type (:-) Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442565Sym0 a0) a1
type (:+) Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442539Sym0 a0) a1
type Min Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat Min_1627439072Sym0 a0) a1
type Max Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat Max_1627439105Sym0 a0) a1
type (:>=) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641651Sym0 Nat) arg0) arg1
type (:>) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641618Sym0 Nat) arg0) arg1
type (:<=) Nat a0 a1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat TFHelper_1627439035Sym0 a0) a1
type (:<) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641552Sym0 Nat) arg0) arg1
type Compare Nat arg0 arg1 = Apply Ordering Nat (Apply (TyFun Nat Ordering -> *) Nat (Compare_1627641519Sym0 Nat) arg0) arg1
type (:/=) Nat x y = Not ((:==) Nat x y)
type (:==) Nat a0 b0 = Equals_1627433556 a0 b0
type Apply Nat Nat FromInteger_1627442636Sym0 l0 = FromInteger_1627442636Sym1 l0
type Apply Nat Nat SSym0 l0 = SSym1 l0
type Apply Nat Nat Signum_1627442618Sym0 l0 = Signum_1627442618Sym1 l0
type Apply Nat Nat Abs_1627442605Sym0 l0 = Abs_1627442605Sym1 l0
type Apply Bool Nat ((:<<=$$) l1) l0 = (:<<=$$$) l1 l0
type Apply Bool Nat (TFHelper_1627439035Sym1 l1) l0 = TFHelper_1627439035Sym2 l1 l0
type Apply Nat Nat ((:$$) l1) l0 = (:$$$) l1 l0
type Apply Nat Nat (TFHelper_1627442590Sym1 l1) l0 = TFHelper_1627442590Sym2 l1 l0
type Apply Nat Nat (TFHelper_1627442565Sym1 l1) l0 = TFHelper_1627442565Sym2 l1 l0
type Apply Nat Nat (TFHelper_1627442539Sym1 l1) l0 = TFHelper_1627442539Sym2 l1 l0
type Apply Nat Nat (Min_1627439072Sym1 l1) l0 = Min_1627439072Sym2 l1 l0
type Apply Nat Nat (Max_1627439105Sym1 l1) l0 = Max_1627439105Sym2 l1 l0
type DemoteRep Nat (KProxy Nat) = Nat
type MonomorphicRep Nat (Sing Nat) = Int
type CharOf * (ZqBasic Nat p z) = p Source
type Apply (TyFun Nat Bool -> *) Nat (:<<=$) l0 = (:<<=$$) l0
type Apply (TyFun Nat Bool -> *) Nat TFHelper_1627439035Sym0 l0 = TFHelper_1627439035Sym1 l0
type Apply (TyFun Nat Nat -> ) Nat (:$) l0 = (:*$$) l0
type Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442590Sym0 l0 = TFHelper_1627442590Sym1 l0
type Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442565Sym0 l0 = TFHelper_1627442565Sym1 l0
type Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442539Sym0 l0 = TFHelper_1627442539Sym1 l0
type Apply (TyFun Nat Nat -> *) Nat Min_1627439072Sym0 l0 = Min_1627439072Sym1 l0
type Apply (TyFun Nat Nat -> *) Nat Max_1627439105Sym0 l0 = Max_1627439105Sym1 l0

type NatC p = SingI p Source

Kind-restricted synonym for SingI. Use this in constraints for types requiring a Nat type.

type family PrimeNat a Source

Equations

PrimeNat arg_1627477463 = Case_1627477969 arg_1627477463 arg_1627477463

type Prime p = (NatC p, PrimeNat p ~ True) Source

Constructors

toPP :: Nat -> Nat -> PrimePower Source

sToPP :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ToPPSym0 t) t :: PrimePower) Source

type family ToPP a a :: PrimePower Source

Equations

ToPP arg_1627477457 arg_1627477459 = Case_1627478025 arg_1627477457 arg_1627477459 (Apply (Apply Tuple2Sym0 arg_1627477457) arg_1627477459)

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

type PToF p = PpToF (ToPP p N1) Source

Type (family) synonym to create a Factored from a prime Nat

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 -> (Nat, Nat) Source

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

type family UnPP a :: (Nat, Nat) Source

Equations

UnPP (PP pp) = pp

primePP :: PrimePower -> Nat Source

type family PrimePP a :: Nat Source

Equations

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

exponentPP :: PrimePower -> Nat Source

type family ExponentPP a :: Nat Source

Equations

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

Arithmetic operations

fPPMul :: PrimePower -> Factored -> Factored Source

type family FPPMul a a :: Factored Source

Equations

FPPMul (PP `(_z_1627464517, Z)`) y = y
FPPMul (PP `(wild_1627464403, S wild_1627464405)`) (F pps) = Apply FSym0 (Apply (Apply PpMulSym0 (Let1627464524PpSym3 pps wild_1627464403 wild_1627464405)) 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 :: Nat -> Factored -> Factored Source

type family PFree a a :: Factored Source

Equations

PFree n (F pps) = Apply FSym0 (Apply (Let1627502462GoSym2 n pps) pps)

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

Int representing the value of a Factored type

totientFact :: Fact m => Tagged m Int Source

Int representing the totient of a Factored type's value

valueHatFact :: Fact m => Tagged m Int Source

Int representing the "hat" of a Factored type's value m: m, if m is odd, or m/2 otherwise.

radicalFact :: Fact m => Tagged m Int Source

Int representing the radical (product of prime divisors) of a Factored type

oddRadicalFact :: Fact m => Tagged m Int Source

Int representing the odd radical (product of odd prime divisors) of a Factored type

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

Reflects a PrimePower type to a PP value

primePPow :: PPow pp => Tagged pp Int Source

Reflects the prime component of a PrimePower type

exponentPPow :: PPow pp => Tagged pp Int Source

Reflects the exponent component of a PrimePower type

valuePPow :: PPow pp => Tagged pp Int Source

Int representing the value of a PrimePower type

totientPPow :: PPow pp => Tagged pp Int Source

Int representing the totient of a PrimePower type's value

valueNatC :: forall p. NatC p => Tagged p Int Source

Int representing the value of a Nat

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

Entails constraint for divisibility by GCD, i.e. 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

Entails constraint for LCM divisibility, i.e. 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

Entails constraint for LCM divisibility, i.e. the LCM of two divisors of m also divides m.

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

Entails basic facts for p-free division, i.e. 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' -> (NatC p, m `Divides` m') :- (PFree p m `Divides` PFree p m') Source

Entails basic facts for p-free division, i.e., 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

Returns m, if m is odd, or m/2 otherwise

type PP = (Int, Int) Source

Type synonym for (prime :: Int, exponent :: Int) pair

ppToPP :: PrimePower -> PP Source

Converts a Nat prime-power pair to an Int prime-power pair

valuePP :: PP -> Int Source

Evaluates a prime-power pair (p,e) to p^e

totientPP :: PP -> Int Source

Euler's totient function of a prime-power pair

radicalPP :: PP -> Int Source

The prime component of a prime-power pair

oddRadicalPP :: PP -> Int Source

The odd radical of a prime-power pair (p,_): p if p is odd, 1 if p==2

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

Type synonyms (not type families)

type family F1 Source

Equations

F1 = Apply FSym0 `[]`

type family F2 Source

Equations

F2 = Apply PrimeToFSym0 N2Sym0

type family F3 Source

Equations

F3 = Apply PrimeToFSym0 N3Sym0

type family F4 Source

Equations

F4 = Apply (Apply FMulSym0 F2Sym0) F2Sym0

type family F5 Source

Equations

F5 = Apply PrimeToFSym0 N5Sym0

type family F6 Source

Equations

F6 = Apply (Apply FMulSym0 F2Sym0) F3Sym0

type family F7 Source

Equations

F7 = Apply PrimeToFSym0 N7Sym0

type family F8 Source

Equations

F8 = Apply (Apply FMulSym0 F2Sym0) F4Sym0

type family F9 Source

Equations

F9 = Apply (Apply FMulSym0 F3Sym0) F3Sym0

type family F10 Source

Equations

F10 = Apply (Apply FMulSym0 F2Sym0) F5Sym0

type family F11 Source

Equations

F11 = Apply PrimeToFSym0 N11Sym0

type family F12 Source

Equations

F12 = Apply (Apply FMulSym0 F4Sym0) F3Sym0

type family F13 Source

Equations

F13 = Apply PrimeToFSym0 N13Sym0

type family F14 Source

Equations

F14 = Apply (Apply FMulSym0 F2Sym0) F7Sym0

type family F15 Source

Equations

F15 = Apply (Apply FMulSym0 F3Sym0) F5Sym0

type family F16 Source

Equations

F16 = Apply (Apply FMulSym0 F2Sym0) F8Sym0

type family F17 Source

Equations

F17 = Apply PrimeToFSym0 N17Sym0

type family F18 Source

Equations

F18 = Apply (Apply FMulSym0 F2Sym0) F9Sym0

type family F19 Source

Equations

F19 = Apply PrimeToFSym0 N19Sym0

type family F20 Source

Equations

F20 = Apply (Apply FMulSym0 F2Sym0) F10Sym0

type family F21 Source

Equations

F21 = Apply (Apply FMulSym0 F3Sym0) F7Sym0

type family F22 Source

Equations

F22 = Apply (Apply FMulSym0 F2Sym0) F11Sym0

type family F24 Source

Equations

F24 = Apply (Apply FMulSym0 F2Sym0) F12Sym0

type family F25 Source

Equations

F25 = Apply (Apply FMulSym0 F5Sym0) F5Sym0

type family F26 Source

Equations

F26 = Apply (Apply FMulSym0 F2Sym0) F13Sym0

type family F27 Source

Equations

F27 = Apply (Apply FMulSym0 F3Sym0) F9Sym0

type family F28 Source

Equations

F28 = Apply (Apply FMulSym0 F2Sym0) F14Sym0

type family F30 Source

Equations

F30 = Apply (Apply FMulSym0 F2Sym0) F15Sym0

type family F32 Source

Equations

F32 = Apply (Apply FMulSym0 F2Sym0) F16Sym0

type family F33 Source

Equations

F33 = Apply (Apply FMulSym0 F3Sym0) F11Sym0

type family F34 Source

Equations

F34 = Apply (Apply FMulSym0 F2Sym0) F17Sym0

type family F35 Source

Equations

F35 = Apply (Apply FMulSym0 F5Sym0) F7Sym0

type family F36 Source

Equations

F36 = Apply (Apply FMulSym0 F2Sym0) F18Sym0

type family F38 Source

Equations

F38 = Apply (Apply FMulSym0 F2Sym0) F19Sym0

type family F39 Source

Equations

F39 = Apply (Apply FMulSym0 F3Sym0) F13Sym0

type family F40 Source

Equations

F40 = Apply (Apply FMulSym0 F2Sym0) F20Sym0

type family F42 Source

Equations

F42 = Apply (Apply FMulSym0 F2Sym0) F21Sym0

type family F44 Source

Equations

F44 = Apply (Apply FMulSym0 F2Sym0) F22Sym0

type family F45 Source

Equations

F45 = Apply (Apply FMulSym0 F3Sym0) F15Sym0

type family F48 Source

Equations

F48 = Apply (Apply FMulSym0 F2Sym0) F24Sym0

type family F49 Source

Equations

F49 = Apply (Apply FMulSym0 F7Sym0) F7Sym0

type family F50 Source

Equations

F50 = Apply (Apply FMulSym0 F2Sym0) F25Sym0

type family F51 Source

Equations

F51 = Apply (Apply FMulSym0 F3Sym0) F17Sym0

type family F52 Source

Equations

F52 = Apply (Apply FMulSym0 F2Sym0) F26Sym0

type family F54 Source

Equations

F54 = Apply (Apply FMulSym0 F2Sym0) F27Sym0

type family F55 Source

Equations

F55 = Apply (Apply FMulSym0 F5Sym0) F11Sym0

type family F56 Source

Equations

F56 = Apply (Apply FMulSym0 F2Sym0) F28Sym0

type family F57 Source

Equations

F57 = Apply (Apply FMulSym0 F3Sym0) F19Sym0

type family F60 Source

Equations

F60 = Apply (Apply FMulSym0 F2Sym0) F30Sym0

type family F63 Source

Equations

F63 = Apply (Apply FMulSym0 F3Sym0) F21Sym0

type family F64 Source

Equations

F64 = Apply (Apply FMulSym0 F2Sym0) F32Sym0

type family F65 Source

Equations

F65 = Apply (Apply FMulSym0 F5Sym0) F13Sym0

type family F66 Source

Equations

F66 = Apply (Apply FMulSym0 F2Sym0) F33Sym0

type family F68 Source

Equations

F68 = Apply (Apply FMulSym0 F2Sym0) F34Sym0

type family F70 Source

Equations

F70 = Apply (Apply FMulSym0 F2Sym0) F35Sym0

type family F72 Source

Equations

F72 = Apply (Apply FMulSym0 F2Sym0) F36Sym0

type family F75 Source

Equations

F75 = Apply (Apply FMulSym0 F3Sym0) F25Sym0

type family F76 Source

Equations

F76 = Apply (Apply FMulSym0 F2Sym0) F38Sym0

type family F77 Source

Equations

F77 = Apply (Apply FMulSym0 F7Sym0) F11Sym0

type family F78 Source

Equations

F78 = Apply (Apply FMulSym0 F2Sym0) F39Sym0

type family F80 Source

Equations

F80 = Apply (Apply FMulSym0 F2Sym0) F40Sym0

type family F81 Source

Equations

F81 = Apply (Apply FMulSym0 F3Sym0) F27Sym0

type family F84 Source

Equations

F84 = Apply (Apply FMulSym0 F2Sym0) F42Sym0

type family F85 Source

Equations

F85 = Apply (Apply FMulSym0 F5Sym0) F17Sym0

type family F88 Source

Equations

F88 = Apply (Apply FMulSym0 F2Sym0) F44Sym0

type family F90 Source

Equations

F90 = Apply (Apply FMulSym0 F2Sym0) F45Sym0

type family F91 Source

Equations

F91 = Apply (Apply FMulSym0 F7Sym0) F13Sym0

type family F95 Source

Equations

F95 = Apply (Apply FMulSym0 F5Sym0) F19Sym0

type family F96 Source

Equations

F96 = Apply (Apply FMulSym0 F2Sym0) F48Sym0

type family F98 Source

Equations

F98 = Apply (Apply FMulSym0 F2Sym0) F49Sym0

type family F99 Source

Equations

F99 = Apply (Apply FMulSym0 F9Sym0) F11Sym0

type family F128 Source

Equations

F128 = Apply (Apply FMulSym0 F2Sym0) F64Sym0

type family F256 Source

Equations

F256 = Apply (Apply FMulSym0 F2Sym0) F128Sym0

type family F512 Source

Equations

F512 = Apply (Apply FMulSym0 F2Sym0) F256Sym0

type family F1024 Source

Equations

F1024 = Apply (Apply FMulSym0 F2Sym0) F512Sym0

type family F2048 Source

Equations

F2048 = Apply (Apply FMulSym0 F2Sym0) F1024Sym0