{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.Polynomial.Factorization.Hensel.Internal
-- Copyright   :  (c) Masahiro Sakai 2013-2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- * <http://www.math.kobe-u.ac.jp/Asir/ca.pdf>
--
-- * <http://www14.in.tum.de/konferenzen/Jass07/courses/1/Bulwahn/Buhlwahn_Paper.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.Data.Polynomial.Factorization.Hensel.Internal
  ( hensel
  , cabook_proposition_5_10
  , cabook_proposition_5_11
  ) where

import Control.Exception (assert)
import Data.FiniteField
import Data.Proxy
import GHC.TypeLits

import ToySolver.Data.Polynomial.Base (UPolynomial)
import qualified ToySolver.Data.Polynomial.Base as P

-- import Text.PrettyPrint.HughesPJClass

hensel :: forall p. KnownNat p => UPolynomial Integer -> [UPolynomial (PrimeField p)] -> Integer -> [UPolynomial Integer]
hensel :: UPolynomial Integer
-> [UPolynomial (PrimeField p)] -> Integer -> [UPolynomial Integer]
hensel UPolynomial Integer
f [UPolynomial (PrimeField p)]
fs1 Integer
k
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0    = [Char] -> [UPolynomial Integer]
forall a. HasCallStack => [Char] -> a
error [Char]
"ToySolver.Data.Polynomial.Factorization.Hensel.hensel: k <= 0"
  | Bool
otherwise = Bool -> [UPolynomial Integer] -> [UPolynomial Integer]
forall a. HasCallStack => Bool -> a -> a
assert Bool
precondition ([UPolynomial Integer] -> [UPolynomial Integer])
-> [UPolynomial Integer] -> [UPolynomial Integer]
forall a b. (a -> b) -> a -> b
$ Integer -> [UPolynomial Integer] -> [UPolynomial Integer]
go Integer
1 ((UPolynomial (PrimeField p) -> UPolynomial Integer)
-> [UPolynomial (PrimeField p)] -> [UPolynomial Integer]
forall a b. (a -> b) -> [a] -> [b]
map ((PrimeField p -> Integer)
-> UPolynomial (PrimeField p) -> UPolynomial Integer
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff PrimeField p -> Integer
forall (p :: Nat). PrimeField p -> Integer
Data.FiniteField.toInteger) [UPolynomial (PrimeField p)]
fs1)
  where
    precondition :: Bool
precondition =
      (Integer -> PrimeField p)
-> UPolynomial Integer -> UPolynomial (PrimeField p)
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff Integer -> PrimeField p
forall a. Num a => Integer -> a
fromInteger UPolynomial Integer
f UPolynomial (PrimeField p) -> UPolynomial (PrimeField p) -> Bool
forall a. Eq a => a -> a -> Bool
== [UPolynomial (PrimeField p)] -> UPolynomial (PrimeField p)
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [UPolynomial (PrimeField p)]
fs1 Bool -> Bool -> Bool
&&
      UPolynomial Integer -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial Integer
f Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial (PrimeField p) -> Integer
forall t. Degree t => t -> Integer
P.deg ([UPolynomial (PrimeField p)] -> UPolynomial (PrimeField p)
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [UPolynomial (PrimeField p)]
fs1)

    p :: Integer
    p :: Integer
p = Proxy p -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy p
forall k (t :: k). Proxy t
Proxy :: Proxy p)

    go :: Integer -> [UPolynomial Integer] -> [UPolynomial Integer]
    go :: Integer -> [UPolynomial Integer] -> [UPolynomial Integer]
go !Integer
i [UPolynomial Integer]
fs
      | Integer
iInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
k      = Bool -> [UPolynomial Integer] -> [UPolynomial Integer]
forall a. HasCallStack => Bool -> a -> a
assert (Integer -> [UPolynomial Integer] -> Bool
check Integer
i [UPolynomial Integer]
fs) ([UPolynomial Integer] -> [UPolynomial Integer])
-> [UPolynomial Integer] -> [UPolynomial Integer]
forall a b. (a -> b) -> a -> b
$ [UPolynomial Integer]
fs
      | Bool
otherwise = Bool -> [UPolynomial Integer] -> [UPolynomial Integer]
forall a. HasCallStack => Bool -> a -> a
assert (Integer -> [UPolynomial Integer] -> Bool
check Integer
i [UPolynomial Integer]
fs) ([UPolynomial Integer] -> [UPolynomial Integer])
-> [UPolynomial Integer] -> [UPolynomial Integer]
forall a b. (a -> b) -> a -> b
$ Integer -> [UPolynomial Integer] -> [UPolynomial Integer]
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Integer -> [UPolynomial Integer] -> [UPolynomial Integer]
lift Integer
i [UPolynomial Integer]
fs)

    check :: Integer -> [UPolynomial Integer] -> Bool
    check :: Integer -> [UPolynomial Integer] -> Bool
check Integer
k' [UPolynomial Integer]
fs =
        [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
        [ (Integer -> Integer) -> UPolynomial Integer -> UPolynomial Integer
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
pk) UPolynomial Integer
f UPolynomial Integer -> UPolynomial Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer -> Integer) -> UPolynomial Integer -> UPolynomial Integer
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
pk) ([UPolynomial Integer] -> UPolynomial Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [UPolynomial Integer]
fs)
        , [UPolynomial (PrimeField p)]
fs1 [UPolynomial (PrimeField p)]
-> [UPolynomial (PrimeField p)] -> Bool
forall a. Eq a => a -> a -> Bool
== (UPolynomial Integer -> UPolynomial (PrimeField p))
-> [UPolynomial Integer] -> [UPolynomial (PrimeField p)]
forall a b. (a -> b) -> [a] -> [b]
map ((Integer -> PrimeField p)
-> UPolynomial Integer -> UPolynomial (PrimeField p)
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff Integer -> PrimeField p
forall a. Num a => Integer -> a
fromInteger) [UPolynomial Integer]
fs
        , [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [UPolynomial (PrimeField p) -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial (PrimeField p)
fi1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial Integer -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial Integer
fik | (UPolynomial (PrimeField p)
fi1, UPolynomial Integer
fik) <- [UPolynomial (PrimeField p)]
-> [UPolynomial Integer]
-> [(UPolynomial (PrimeField p), UPolynomial Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [UPolynomial (PrimeField p)]
fs1 [UPolynomial Integer]
fs]
        ]
      where
        pk :: Integer
pk = Integer
p Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
k'

    lift :: Integer -> [UPolynomial Integer] -> [UPolynomial Integer]
    lift :: Integer -> [UPolynomial Integer] -> [UPolynomial Integer]
lift Integer
k' [UPolynomial Integer]
fs = [UPolynomial Integer]
fs'
      where
        pk :: Integer
pk  = Integer
pInteger -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
k'
        pk1 :: Integer
pk1 = Integer
pInteger -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
k'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)

        -- f ≡ product fs + p^k h  (mod p^(k+1))
        h :: UPolynomial Integer
        h :: UPolynomial Integer
h = (Integer -> Integer) -> UPolynomial Integer -> UPolynomial Integer
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (\Integer
c -> (Integer
c Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
pk1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
pk) (UPolynomial Integer
f UPolynomial Integer -> UPolynomial Integer -> UPolynomial Integer
forall a. Num a => a -> a -> a
- [UPolynomial Integer] -> UPolynomial Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [UPolynomial Integer]
fs)

        hs :: [UPolynomial (PrimeField p)]
        hs :: [UPolynomial (PrimeField p)]
hs = [UPolynomial (PrimeField p)]
-> UPolynomial (PrimeField p) -> [UPolynomial (PrimeField p)]
forall k.
(Fractional k, Ord k) =>
[UPolynomial k] -> UPolynomial k -> [UPolynomial k]
cabook_proposition_5_11 ((UPolynomial Integer -> UPolynomial (PrimeField p))
-> [UPolynomial Integer] -> [UPolynomial (PrimeField p)]
forall a b. (a -> b) -> [a] -> [b]
map ((Integer -> PrimeField p)
-> UPolynomial Integer -> UPolynomial (PrimeField p)
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff Integer -> PrimeField p
forall a. Num a => Integer -> a
fromInteger) [UPolynomial Integer]
fs) ((Integer -> PrimeField p)
-> UPolynomial Integer -> UPolynomial (PrimeField p)
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff Integer -> PrimeField p
forall a. Num a => Integer -> a
fromInteger UPolynomial Integer
h)

        fs' :: [UPolynomial Integer]
        fs' :: [UPolynomial Integer]
fs' = [ (Integer -> Integer) -> UPolynomial Integer -> UPolynomial Integer
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
pk1) (UPolynomial Integer
fi UPolynomial Integer -> UPolynomial Integer -> UPolynomial Integer
forall a. Num a => a -> a -> a
+ Integer -> UPolynomial Integer
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant Integer
pk UPolynomial Integer -> UPolynomial Integer -> UPolynomial Integer
forall a. Num a => a -> a -> a
* (PrimeField p -> Integer)
-> UPolynomial (PrimeField p) -> UPolynomial Integer
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff PrimeField p -> Integer
forall (p :: Nat). PrimeField p -> Integer
Data.FiniteField.toInteger UPolynomial (PrimeField p)
hi)
              | (UPolynomial Integer
fi, UPolynomial (PrimeField p)
hi) <- [UPolynomial Integer]
-> [UPolynomial (PrimeField p)]
-> [(UPolynomial Integer, UPolynomial (PrimeField p))]
forall a b. [a] -> [b] -> [(a, b)]
zip [UPolynomial Integer]
fs [UPolynomial (PrimeField p)]
hs ]

-- http://www.math.kobe-u.ac.jp/Asir/ca.pdf
cabook_proposition_5_10
  :: forall k. (Num k, Fractional k, Eq k)
  => [UPolynomial k] -> [UPolynomial k]
cabook_proposition_5_10 :: [UPolynomial k] -> [UPolynomial k]
cabook_proposition_5_10 [UPolynomial k]
fs = [UPolynomial k] -> [UPolynomial k]
normalize ([UPolynomial k] -> [UPolynomial k]
go [UPolynomial k]
fs)
  where
    check :: [UPolynomial k] -> [UPolynomial k] -> Bool
    check :: [UPolynomial k] -> [UPolynomial k] -> Bool
check [UPolynomial k]
es [UPolynomial k]
fs' = [UPolynomial k] -> UPolynomial k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [UPolynomial k
ei UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* ([UPolynomial k] -> UPolynomial k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [UPolynomial k]
fs' UPolynomial k -> UPolynomial k -> UPolynomial k
forall k.
(Eq k, Fractional k) =>
UPolynomial k -> UPolynomial k -> UPolynomial k
`P.div` UPolynomial k
fi) | (UPolynomial k
ei,UPolynomial k
fi) <- [UPolynomial k]
-> [UPolynomial k] -> [(UPolynomial k, UPolynomial k)]
forall a b. [a] -> [b] -> [(a, b)]
zip [UPolynomial k]
es [UPolynomial k]
fs'] UPolynomial k -> UPolynomial k -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial k
1

    go :: [UPolynomial k] -> [UPolynomial k]
    go :: [UPolynomial k] -> [UPolynomial k]
go [] = [Char] -> [UPolynomial k]
forall a. HasCallStack => [Char] -> a
error [Char]
"cabook_proposition_5_10: empty list"
    go [UPolynomial k
fi] = Bool -> [UPolynomial k] -> [UPolynomial k]
forall a. HasCallStack => Bool -> a -> a
assert ([UPolynomial k] -> [UPolynomial k] -> Bool
check [UPolynomial k
1] [UPolynomial k
fi]) [UPolynomial k
1]
    go (UPolynomial k
fi : [UPolynomial k]
fs') =
      case UPolynomial k
-> UPolynomial k -> (UPolynomial k, UPolynomial k, UPolynomial k)
forall k.
(Eq k, Fractional k) =>
UPolynomial k
-> UPolynomial k -> (UPolynomial k, UPolynomial k, UPolynomial k)
P.exgcd ([UPolynomial k] -> UPolynomial k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [UPolynomial k]
fs') UPolynomial k
fi of
        (UPolynomial k
g,UPolynomial k
ei,UPolynomial k
v) ->
           Bool -> [UPolynomial k] -> [UPolynomial k]
forall a. HasCallStack => Bool -> a -> a
assert (UPolynomial k
g UPolynomial k -> UPolynomial k -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial k
1) ([UPolynomial k] -> [UPolynomial k])
-> [UPolynomial k] -> [UPolynomial k]
forall a b. (a -> b) -> a -> b
$
             let es' :: [UPolynomial k]
es' = [UPolynomial k] -> [UPolynomial k]
go [UPolynomial k]
fs'
                 es :: [UPolynomial k]
es  = UPolynomial k
ei UPolynomial k -> [UPolynomial k] -> [UPolynomial k]
forall a. a -> [a] -> [a]
: (UPolynomial k -> UPolynomial k)
-> [UPolynomial k] -> [UPolynomial k]
forall a b. (a -> b) -> [a] -> [b]
map (UPolynomial k
vUPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
*) [UPolynomial k]
es'
             in Bool -> [UPolynomial k] -> [UPolynomial k]
forall a. HasCallStack => Bool -> a -> a
assert ([UPolynomial k] -> [UPolynomial k] -> Bool
check [UPolynomial k]
es (UPolynomial k
fi UPolynomial k -> [UPolynomial k] -> [UPolynomial k]
forall a. a -> [a] -> [a]
: [UPolynomial k]
fs')) [UPolynomial k]
es

    normalize :: [UPolynomial k] -> [UPolynomial k]
    normalize :: [UPolynomial k] -> [UPolynomial k]
normalize [UPolynomial k]
es = Bool -> [UPolynomial k] -> [UPolynomial k]
forall a. HasCallStack => Bool -> a -> a
assert ([UPolynomial k] -> [UPolynomial k] -> Bool
check [UPolynomial k]
es2 [UPolynomial k]
fs) [UPolynomial k]
es2
      where
        es2 :: [UPolynomial k]
es2 = (UPolynomial k -> UPolynomial k -> UPolynomial k)
-> [UPolynomial k] -> [UPolynomial k] -> [UPolynomial k]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith UPolynomial k -> UPolynomial k -> UPolynomial k
forall k.
(Eq k, Fractional k) =>
UPolynomial k -> UPolynomial k -> UPolynomial k
P.mod [UPolynomial k]
es [UPolynomial k]
fs

-- http://www.math.kobe-u.ac.jp/Asir/ca.pdf
cabook_proposition_5_11
  :: forall k. (Fractional k, Ord k)
  => [UPolynomial k] -> UPolynomial k -> [UPolynomial k]
cabook_proposition_5_11 :: [UPolynomial k] -> UPolynomial k -> [UPolynomial k]
cabook_proposition_5_11 [UPolynomial k]
fs UPolynomial k
g =
  Bool -> [UPolynomial k] -> [UPolynomial k]
forall a. HasCallStack => Bool -> a -> a
assert (UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
g Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg ([UPolynomial k] -> UPolynomial k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [UPolynomial k]
fs)) ([UPolynomial k] -> [UPolynomial k])
-> [UPolynomial k] -> [UPolynomial k]
forall a b. (a -> b) -> a -> b
$
  Bool -> [UPolynomial k] -> [UPolynomial k]
forall a. HasCallStack => Bool -> a -> a
assert (UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0) ([UPolynomial k] -> [UPolynomial k])
-> [UPolynomial k] -> [UPolynomial k]
forall a b. (a -> b) -> a -> b
$
  Bool -> [UPolynomial k] -> [UPolynomial k]
forall a. HasCallStack => Bool -> a -> a
assert ([UPolynomial k] -> Bool
check [UPolynomial k]
es2) ([UPolynomial k] -> [UPolynomial k])
-> [UPolynomial k] -> [UPolynomial k]
forall a b. (a -> b) -> a -> b
$
    [UPolynomial k]
es2
  where
    es :: [UPolynomial k]
es  = (UPolynomial k -> UPolynomial k)
-> [UPolynomial k] -> [UPolynomial k]
forall a b. (a -> b) -> [a] -> [b]
map (UPolynomial k
gUPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
*) ([UPolynomial k] -> [UPolynomial k])
-> [UPolynomial k] -> [UPolynomial k]
forall a b. (a -> b) -> a -> b
$ [UPolynomial k] -> [UPolynomial k]
forall k.
(Num k, Fractional k, Eq k) =>
[UPolynomial k] -> [UPolynomial k]
cabook_proposition_5_10 [UPolynomial k]
fs
    c :: UPolynomial k
c   = [UPolynomial k] -> UPolynomial k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [UPolynomial k
ei UPolynomial k -> UPolynomial k -> UPolynomial k
forall k.
(Eq k, Fractional k) =>
UPolynomial k -> UPolynomial k -> UPolynomial k
`P.div` UPolynomial k
fi | (UPolynomial k
ei,UPolynomial k
fi) <- [UPolynomial k]
-> [UPolynomial k] -> [(UPolynomial k, UPolynomial k)]
forall a b. [a] -> [b] -> [(a, b)]
zip [UPolynomial k]
es [UPolynomial k]
fs]
    es2 :: [UPolynomial k]
es2 = case (UPolynomial k -> UPolynomial k -> UPolynomial k)
-> [UPolynomial k] -> [UPolynomial k] -> [UPolynomial k]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith UPolynomial k -> UPolynomial k -> UPolynomial k
forall k.
(Eq k, Fractional k) =>
UPolynomial k -> UPolynomial k -> UPolynomial k
P.mod [UPolynomial k]
es [UPolynomial k]
fs of
            UPolynomial k
e2' : [UPolynomial k]
es2' -> UPolynomial k
e2' UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
+ UPolynomial k
c UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* [UPolynomial k] -> UPolynomial k
forall a. [a] -> a
head [UPolynomial k]
fs UPolynomial k -> [UPolynomial k] -> [UPolynomial k]
forall a. a -> [a] -> [a]
: [UPolynomial k]
es2'

    check :: [UPolynomial k] -> Bool
    check :: [UPolynomial k] -> Bool
check [UPolynomial k]
es' =
      [UPolynomial k] -> UPolynomial k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [UPolynomial k
ei UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* ([UPolynomial k] -> UPolynomial k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [UPolynomial k]
fs UPolynomial k -> UPolynomial k -> UPolynomial k
forall k.
(Eq k, Fractional k) =>
UPolynomial k -> UPolynomial k -> UPolynomial k
`P.div` UPolynomial k
fi) | (UPolynomial k
ei,UPolynomial k
fi) <- [UPolynomial k]
-> [UPolynomial k] -> [(UPolynomial k, UPolynomial k)]
forall a b. [a] -> [b] -> [(a, b)]
zip [UPolynomial k]
es' [UPolynomial k]
fs] UPolynomial k -> UPolynomial k -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial k
g Bool -> Bool -> Bool
&&
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
ei Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
fi | (UPolynomial k
ei,UPolynomial k
fi) <- [UPolynomial k]
-> [UPolynomial k] -> [(UPolynomial k, UPolynomial k)]
forall a b. [a] -> [b] -> [(a, b)]
zip [UPolynomial k]
es' [UPolynomial k]
fs]