    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Core.Sized
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Type-level sized bit-vectors. Thanks to Ben Blaxill for providing an
    -- initial implementation of this idea.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DataKinds            #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE ScopedTypeVariables  #-}
    {-# LANGUAGE TypeApplications     #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE TypeOperators        #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Core.Sized (
            -- * Type-sized unsigned bit-vectors
              SWord, WordN, sWord, sWord_, sWords
            -- * Type-sized signed bit-vectors
            , SInt, IntN, sInt, sInt_, sInts
            -- Bit-vector operations
            , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake
            -- Splitting and reconstructing from bytes
            , ByteConverter(..)
            -- Non-zero constraint
            , IsNonZero
           ) where

    import Data.Bits
    import Data.Maybe (fromJust)
    import Data.Proxy (Proxy(..))

    import GHC.TypeLits
    import Data.Kind

    import Data.SBV.Core.Data
    import Data.SBV.Core.Model
    import Data.SBV.Core.Operations
    import Data.SBV.Core.Symbolic

    import Data.SBV.SMT.SMT

    -- Doctest only
    -- $setup
    -- >>> :set -XTypeApplications
    -- >>> :set -XDataKinds
    -- >>> import Data.SBV.Provers.Prover (prove)

    -- | An unsigned bit-vector carrying its size info
    newtype WordN (n :: Nat) = WordN Integer deriving (WordN n -> WordN n -> Bool
    (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> Bool) -> Eq (WordN n)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall (n :: Nat). WordN n -> WordN n -> Bool
    /= :: WordN n -> WordN n -> Bool
    $c/= :: forall (n :: Nat). WordN n -> WordN n -> Bool
    == :: WordN n -> WordN n -> Bool
    $c== :: forall (n :: Nat). WordN n -> WordN n -> Bool
    Eq, Eq (WordN n)
    Eq (WordN n) =>
    (WordN n -> WordN n -> Ordering)
    -> (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> Bool)
    -> (WordN n -> WordN n -> WordN n)
    -> (WordN n -> WordN n -> WordN n)
    -> Ord (WordN n)
    WordN n -> WordN n -> Bool
    WordN n -> WordN n -> Ordering
    WordN n -> WordN n -> WordN n
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall (n :: Nat). Eq (WordN n)
    forall (n :: Nat). WordN n -> WordN n -> Bool
    forall (n :: Nat). WordN n -> WordN n -> Ordering
    forall (n :: Nat). WordN n -> WordN n -> WordN n
    min :: WordN n -> WordN n -> WordN n
    $cmin :: forall (n :: Nat). WordN n -> WordN n -> WordN n
    max :: WordN n -> WordN n -> WordN n
    $cmax :: forall (n :: Nat). WordN n -> WordN n -> WordN n
    >= :: WordN n -> WordN n -> Bool
    $c>= :: forall (n :: Nat). WordN n -> WordN n -> Bool
    > :: WordN n -> WordN n -> Bool
    $c> :: forall (n :: Nat). WordN n -> WordN n -> Bool
    <= :: WordN n -> WordN n -> Bool
    $c<= :: forall (n :: Nat). WordN n -> WordN n -> Bool
    < :: WordN n -> WordN n -> Bool
    $c< :: forall (n :: Nat). WordN n -> WordN n -> Bool
    compare :: WordN n -> WordN n -> Ordering
    $ccompare :: forall (n :: Nat). WordN n -> WordN n -> Ordering
    $cp1Ord :: forall (n :: Nat). Eq (WordN n)
    Ord)

    -- | A symbolic unsigned bit-vector carrying its size info
    type SWord (n :: Nat) = SBV (WordN n)

    -- | Show instance for 'WordN'
    instance Show (WordN n) where
      show :: WordN n -> String
    show (WordN v :: Integer
    v) = Integer -> String
    forall a. Show a => a -> String
    show Integer
    v

    -- | Grab the bit-size from the proxy
    intOfProxy :: KnownNat n => Proxy n -> Int
    intOfProxy :: Proxy n -> Int
    intOfProxy = Integer -> Int
    forall a. Enum a => a -> Int
    fromEnum (Integer -> Int) -> (Proxy n -> Integer) -> Proxy n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal

    -- | Catch 0-width cases
    type ZeroWidth = 'Text "Zero-width BV's are not allowed."

    -- | Type family to create the appropriate non-zero constraint
    type family IsNonZero (arg :: Nat) :: Constraint where
       IsNonZero 0 = TypeError ZeroWidth
       IsNonZero n = ()

    -- | 'WordN' has a kind
    instance (KnownNat n, IsNonZero n) => HasKind (WordN n) where
      kindOf :: WordN n -> Kind
    kindOf _ = Bool -> Int -> Kind
    KBounded Bool
    False (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n))

    -- | 'SymVal' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => SymVal (WordN n) where
       literal :: WordN n -> SBV (WordN n)
    literal  x :: WordN n
    x = Kind -> WordN n -> SBV (WordN n)
    forall a b. Integral a => Kind -> a -> SBV b
    genLiteral  (WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf WordN n
    x) WordN n
    x
       mkSymVal :: Maybe Quantifier -> Maybe String -> m (SBV (WordN n))
    mkSymVal   = Kind -> Maybe Quantifier -> Maybe String -> m (SBV (WordN n))
    forall (m :: * -> *) a.
    MonadSymbolic m =>
    Kind -> Maybe Quantifier -> Maybe String -> m (SBV a)
    genMkSymVar (WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (WordN n
    forall a. HasCallStack => a
    undefined :: WordN n))
       fromCV :: CV -> WordN n
    fromCV     = CV -> WordN n
    forall a. Integral a => CV -> a
    genFromCV

    -- | A signed bit-vector carrying its size info
    newtype IntN (n :: Nat) = IntN Integer deriving (IntN n -> IntN n -> Bool
    (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> Bool) -> Eq (IntN n)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall (n :: Nat). IntN n -> IntN n -> Bool
    /= :: IntN n -> IntN n -> Bool
    $c/= :: forall (n :: Nat). IntN n -> IntN n -> Bool
    == :: IntN n -> IntN n -> Bool
    $c== :: forall (n :: Nat). IntN n -> IntN n -> Bool
    Eq, Eq (IntN n)
    Eq (IntN n) =>
    (IntN n -> IntN n -> Ordering)
    -> (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> Bool)
    -> (IntN n -> IntN n -> IntN n)
    -> (IntN n -> IntN n -> IntN n)
    -> Ord (IntN n)
    IntN n -> IntN n -> Bool
    IntN n -> IntN n -> Ordering
    IntN n -> IntN n -> IntN n
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall (n :: Nat). Eq (IntN n)
    forall (n :: Nat). IntN n -> IntN n -> Bool
    forall (n :: Nat). IntN n -> IntN n -> Ordering
    forall (n :: Nat). IntN n -> IntN n -> IntN n
    min :: IntN n -> IntN n -> IntN n
    $cmin :: forall (n :: Nat). IntN n -> IntN n -> IntN n
    max :: IntN n -> IntN n -> IntN n
    $cmax :: forall (n :: Nat). IntN n -> IntN n -> IntN n
    >= :: IntN n -> IntN n -> Bool
    $c>= :: forall (n :: Nat). IntN n -> IntN n -> Bool
    > :: IntN n -> IntN n -> Bool
    $c> :: forall (n :: Nat). IntN n -> IntN n -> Bool
    <= :: IntN n -> IntN n -> Bool
    $c<= :: forall (n :: Nat). IntN n -> IntN n -> Bool
    < :: IntN n -> IntN n -> Bool
    $c< :: forall (n :: Nat). IntN n -> IntN n -> Bool
    compare :: IntN n -> IntN n -> Ordering
    $ccompare :: forall (n :: Nat). IntN n -> IntN n -> Ordering
    $cp1Ord :: forall (n :: Nat). Eq (IntN n)
    Ord)

    -- | A symbolic signed bit-vector carrying its size info
    type SInt (n :: Nat) = SBV (IntN n)

    -- | Show instance for 'IntN'
    instance Show (IntN n) where
      show :: IntN n -> String
    show (IntN v :: Integer
    v) = Integer -> String
    forall a. Show a => a -> String
    show Integer
    v

    -- | 'IntN' has a kind
    instance (KnownNat n, IsNonZero n) => HasKind (IntN n) where
      kindOf :: IntN n -> Kind
    kindOf _ = Bool -> Int -> Kind
    KBounded Bool
    True (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n))

    -- | 'SymVal' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => SymVal (IntN n) where
       literal :: IntN n -> SBV (IntN n)
    literal  x :: IntN n
    x = Kind -> IntN n -> SBV (IntN n)
    forall a b. Integral a => Kind -> a -> SBV b
    genLiteral  (IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf IntN n
    x) IntN n
    x
       mkSymVal :: Maybe Quantifier -> Maybe String -> m (SBV (IntN n))
    mkSymVal   = Kind -> Maybe Quantifier -> Maybe String -> m (SBV (IntN n))
    forall (m :: * -> *) a.
    MonadSymbolic m =>
    Kind -> Maybe Quantifier -> Maybe String -> m (SBV a)
    genMkSymVar (IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (IntN n
    forall a. HasCallStack => a
    undefined :: IntN n))
       fromCV :: CV -> IntN n
    fromCV     = CV -> IntN n
    forall a. Integral a => CV -> a
    genFromCV

    -- Lift a unary operation via SVal
    lift1 :: (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal) -> bv n -> bv n
    lift1 :: String -> (SVal -> SVal) -> bv n -> bv n
    lift1 nm :: String
    nm op :: SVal -> SVal
    op x :: bv n
    x = SVal -> bv n
    uc (SVal -> bv n) -> SVal -> bv n
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal
    op (bv n -> SVal
    c bv n
    x)
      where k :: Kind
    k = bv n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf bv n
    x
            c :: bv n -> SVal
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV))
    -> (bv n -> CV) -> bv n -> Either CV (Cached SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> CVal
    CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . bv n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
            uc :: SVal -> bv n
    uc (SVal _ (Left (CV _ (CInteger v :: Integer
    v)))) = Integer -> bv n
    forall a. Num a => Integer -> a
    fromInteger Integer
    v
            uc r :: SVal
    r                                   = String -> bv n
    forall a. HasCallStack => String -> a
    error (String -> bv n) -> String -> bv n
    forall a b. (a -> b) -> a -> b
    $ "Impossible happened while lifting " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " over " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, bv n, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, bv n
    x, SVal
    r)

    -- Lift a binary operation via SVal
    lift2 :: (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 :: String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 nm :: String
    nm op :: SVal -> SVal -> SVal
    op x :: bv n
    x y :: bv n
    y = SVal -> bv n
    uc (SVal -> bv n) -> SVal -> bv n
    forall a b. (a -> b) -> a -> b
    $ bv n -> SVal
    c bv n
    x SVal -> SVal -> SVal
    `op` bv n -> SVal
    c bv n
    y
      where k :: Kind
    k = bv n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf bv n
    x
            c :: bv n -> SVal
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV))
    -> (bv n -> CV) -> bv n -> Either CV (Cached SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> CVal
    CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . bv n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
            uc :: SVal -> bv n
    uc (SVal _ (Left (CV _ (CInteger v :: Integer
    v)))) = Integer -> bv n
    forall a. Num a => Integer -> a
    fromInteger Integer
    v
            uc r :: SVal
    r                                   = String -> bv n
    forall a. HasCallStack => String -> a
    error (String -> bv n) -> String -> bv n
    forall a b. (a -> b) -> a -> b
    $ "Impossible happened while lifting " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " over " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, bv n, bv n, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, bv n
    x, bv n
    y, SVal
    r)

    -- Lift a binary operation via SVal where second argument is an Int
    lift2I :: (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I :: String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I nm :: String
    nm op :: SVal -> Int -> SVal
    op x :: bv n
    x i :: Int
    i = SVal -> bv n
    uc (SVal -> bv n) -> SVal -> bv n
    forall a b. (a -> b) -> a -> b
    $ bv n -> SVal
    c bv n
    x SVal -> Int -> SVal
    `op` Int
    i
      where k :: Kind
    k = bv n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf bv n
    x
            c :: bv n -> SVal
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV))
    -> (bv n -> CV) -> bv n -> Either CV (Cached SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> CVal
    CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . bv n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
            uc :: SVal -> bv n
    uc (SVal _ (Left (CV _ (CInteger v :: Integer
    v)))) = Integer -> bv n
    forall a. Num a => Integer -> a
    fromInteger Integer
    v
            uc r :: SVal
    r                                   = String -> bv n
    forall a. HasCallStack => String -> a
    error (String -> bv n) -> String -> bv n
    forall a b. (a -> b) -> a -> b
    $ "Impossible happened while lifting " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " over " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, bv n, Int, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, bv n
    x, Int
    i, SVal
    r)

    -- Lift a binary operation via SVal where second argument is an Int and returning a Bool
    lift2IB :: (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
    lift2IB :: String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
    lift2IB nm :: String
    nm op :: SVal -> Int -> SVal
    op x :: bv n
    x i :: Int
    i = SVal -> Bool
    uc (SVal -> Bool) -> SVal -> Bool
    forall a b. (a -> b) -> a -> b
    $ bv n -> SVal
    c bv n
    x SVal -> Int -> SVal
    `op` Int
    i
      where k :: Kind
    k = bv n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf bv n
    x
            c :: bv n -> SVal
    c = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal)
    -> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left (CV -> Either CV (Cached SV))
    -> (bv n -> CV) -> bv n -> Either CV (Cached SV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> CVal
    CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . bv n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
            uc :: SVal -> Bool
    uc (SVal _ (Left v :: CV
    v)) = CV -> Bool
    cvToBool CV
    v
            uc r :: SVal
    r                 = String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "Impossible happened while lifting " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    nm String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " over " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, bv n, Int, SVal) -> String
    forall a. Show a => a -> String
    show (Kind
    k, bv n
    x, Int
    i, SVal
    r)

    -- | 'Bounded' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => Bounded (WordN n) where
       minBound :: WordN n
    minBound = Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN 0
       maxBound :: WordN n
    maxBound = let sz :: Int
    sz = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n) in Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN (Integer -> WordN n) -> Integer -> WordN n
    forall a b. (a -> b) -> a -> b
    $ 2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    sz Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1

    -- | 'Bounded' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => Bounded (IntN n) where
       minBound :: IntN n
    minBound = let sz1 :: Int
    sz1 = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1 in Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> Integer -> IntN n
    forall a b. (a -> b) -> a -> b
    $ - (2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    sz1)
       maxBound :: IntN n
    maxBound = let sz1 :: Int
    sz1 = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1 in Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> Integer -> IntN n
    forall a b. (a -> b) -> a -> b
    $ 2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    sz1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1

    -- | 'Num' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => Num (WordN n) where
       + :: WordN n -> WordN n -> WordN n
    (+)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 "(+)"    SVal -> SVal -> SVal
    svPlus
       (-)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 "(*)"    SVal -> SVal -> SVal
    svMinus
       * :: WordN n -> WordN n -> WordN n
    (*)         = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 "(*)"    SVal -> SVal -> SVal
    svTimes
       negate :: WordN n -> WordN n
    negate      = String -> (SVal -> SVal) -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 "signum" SVal -> SVal
    svUNeg
       abs :: WordN n -> WordN n
    abs         = String -> (SVal -> SVal) -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 "abs"    SVal -> SVal
    svAbs
       signum :: WordN n -> WordN n
    signum      = Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN (Integer -> WordN n) -> (WordN n -> Integer) -> WordN n -> WordN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    forall a. Num a => a -> a
    signum   (Integer -> Integer) -> (WordN n -> Integer) -> WordN n -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
       fromInteger :: Integer -> WordN n
    fromInteger = Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN (Integer -> WordN n) -> (Integer -> Integer) -> Integer -> WordN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Integer -> Integer
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Integer -> Integer)
    -> (Integer -> Maybe Integer) -> Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SVal -> Maybe Integer
    svAsInteger (SVal -> Maybe Integer)
    -> (Integer -> SVal) -> Integer -> Maybe Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> Integer -> SVal
    svInteger (WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (WordN n
    forall a. HasCallStack => a
    undefined :: WordN n))

    -- | 'Num' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => Num (IntN n) where
       + :: IntN n -> IntN n -> IntN n
    (+)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 "(+)"    SVal -> SVal -> SVal
    svPlus
       (-)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 "(*)"    SVal -> SVal -> SVal
    svMinus
       * :: IntN n -> IntN n -> IntN n
    (*)         = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2 "(*)"    SVal -> SVal -> SVal
    svTimes
       negate :: IntN n -> IntN n
    negate      = String -> (SVal -> SVal) -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 "signum" SVal -> SVal
    svUNeg
       abs :: IntN n -> IntN n
    abs         = String -> (SVal -> SVal) -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1 "abs"    SVal -> SVal
    svAbs
       signum :: IntN n -> IntN n
    signum      = Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> (IntN n -> Integer) -> IntN n -> IntN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    forall a. Num a => a -> a
    signum   (Integer -> Integer) -> (IntN n -> Integer) -> IntN n -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger
       fromInteger :: Integer -> IntN n
    fromInteger = Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN (Integer -> IntN n) -> (Integer -> Integer) -> Integer -> IntN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Integer -> Integer
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Integer -> Integer)
    -> (Integer -> Maybe Integer) -> Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SVal -> Maybe Integer
    svAsInteger (SVal -> Maybe Integer)
    -> (Integer -> SVal) -> Integer -> Maybe Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> Integer -> SVal
    svInteger (IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (IntN n
    forall a. HasCallStack => a
    undefined :: IntN n))

    -- | 'Enum' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => Enum (WordN n) where
       toEnum :: Int -> WordN n
    toEnum   = Integer -> WordN n
    forall a. Num a => Integer -> a
    fromInteger  (Integer -> WordN n) -> (Int -> Integer) -> Int -> WordN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger
       fromEnum :: WordN n -> Int
    fromEnum = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Int) -> (WordN n -> Integer) -> WordN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | 'Enum' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => Enum (IntN n) where
       toEnum :: Int -> IntN n
    toEnum   = Integer -> IntN n
    forall a. Num a => Integer -> a
    fromInteger  (Integer -> IntN n) -> (Int -> Integer) -> Int -> IntN n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger
       fromEnum :: IntN n -> Int
    fromEnum = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | 'Real' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => Real (WordN n) where
       toRational :: WordN n -> Rational
    toRational (WordN x :: Integer
    x) = Integer -> Rational
    forall a. Real a => a -> Rational
    toRational Integer
    x

    -- | 'Real' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => Real (IntN n) where
       toRational :: IntN n -> Rational
    toRational (IntN x :: Integer
    x) = Integer -> Rational
    forall a. Real a => a -> Rational
    toRational Integer
    x

    -- | 'Integral' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => Integral (WordN n) where
       toInteger :: WordN n -> Integer
    toInteger (WordN x :: Integer
    x)           = Integer
    x
       quotRem :: WordN n -> WordN n -> (WordN n, WordN n)
    quotRem   (WordN x :: Integer
    x) (WordN y :: Integer
    y) = let (q :: Integer
    q, r :: Integer
    r) = Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    quotRem Integer
    x Integer
    y in (Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN Integer
    q, Integer -> WordN n
    forall (n :: Nat). Integer -> WordN n
    WordN Integer
    r)

    -- | 'Integral' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => Integral (IntN n) where
       toInteger :: IntN n -> Integer
    toInteger (IntN x :: Integer
    x)          = Integer
    x
       quotRem :: IntN n -> IntN n -> (IntN n, IntN n)
    quotRem   (IntN x :: Integer
    x) (IntN y :: Integer
    y) = let (q :: Integer
    q, r :: Integer
    r) = Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    quotRem Integer
    x Integer
    y in (Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN Integer
    q, Integer -> IntN n
    forall (n :: Nat). Integer -> IntN n
    IntN Integer
    r)

    --  'Bits' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => Bits (WordN n) where
       .&. :: WordN n -> WordN n -> WordN n
    (.&.)        = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   "(.&.)"      SVal -> SVal -> SVal
    svAnd
       .|. :: WordN n -> WordN n -> WordN n
    (.|.)        = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   "(.|.)"      SVal -> SVal -> SVal
    svOr
       xor :: WordN n -> WordN n -> WordN n
    xor          = String -> (SVal -> SVal -> SVal) -> WordN n -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   "xor"        SVal -> SVal -> SVal
    svXOr
       complement :: WordN n -> WordN n
    complement   = String -> (SVal -> SVal) -> WordN n -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1   "complement" SVal -> SVal
    svNot
       shiftL :: WordN n -> Int -> WordN n
    shiftL       = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  "shiftL"     SVal -> Int -> SVal
    svShl
       shiftR :: WordN n -> Int -> WordN n
    shiftR       = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  "shiftR"     SVal -> Int -> SVal
    svShr
       rotateL :: WordN n -> Int -> WordN n
    rotateL      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  "rotateL"    SVal -> Int -> SVal
    svRol
       rotateR :: WordN n -> Int -> WordN n
    rotateR      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  "rotateR"    SVal -> Int -> SVal
    svRor
       testBit :: WordN n -> Int -> Bool
    testBit      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> Bool
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
    lift2IB "svTestBit"  SVal -> Int -> SVal
    svTestBit
       bitSizeMaybe :: WordN n -> Maybe Int
    bitSizeMaybe = Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> (WordN n -> Int) -> WordN n -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> WordN n -> Int
    forall a b. a -> b -> a
    const (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n))
       bitSize :: WordN n -> Int
    bitSize _    = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n)
       isSigned :: WordN n -> Bool
    isSigned     = Kind -> Bool
    forall a. HasKind a => a -> Bool
    hasSign (Kind -> Bool) -> (WordN n -> Kind) -> WordN n -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf
       bit :: Int -> WordN n
    bit i :: Int
    i        = 1 WordN n -> Int -> WordN n
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    i
       popCount :: WordN n -> Int
    popCount     = Int -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Int) -> (WordN n -> Int) -> WordN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Bits a => a -> Int
    popCount (Integer -> Int) -> (WordN n -> Integer) -> WordN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WordN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    --  'Bits' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => Bits (IntN n) where
       .&. :: IntN n -> IntN n -> IntN n
    (.&.)        = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   "(.&.)"      SVal -> SVal -> SVal
    svAnd
       .|. :: IntN n -> IntN n -> IntN n
    (.|.)        = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   "(.|.)"      SVal -> SVal -> SVal
    svOr
       xor :: IntN n -> IntN n -> IntN n
    xor          = String -> (SVal -> SVal -> SVal) -> IntN n -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
    lift2   "xor"        SVal -> SVal -> SVal
    svXOr
       complement :: IntN n -> IntN n
    complement   = String -> (SVal -> SVal) -> IntN n -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> SVal) -> bv n -> bv n
    lift1   "complement" SVal -> SVal
    svNot
       shiftL :: IntN n -> Int -> IntN n
    shiftL       = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  "shiftL"     SVal -> Int -> SVal
    svShl
       shiftR :: IntN n -> Int -> IntN n
    shiftR       = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  "shiftR"     SVal -> Int -> SVal
    svShr
       rotateL :: IntN n -> Int -> IntN n
    rotateL      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  "rotateL"    SVal -> Int -> SVal
    svRol
       rotateR :: IntN n -> Int -> IntN n
    rotateR      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
    lift2I  "rotateR"    SVal -> Int -> SVal
    svRor
       testBit :: IntN n -> Int -> Bool
    testBit      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> Bool
    forall (n :: Nat) (bv :: Nat -> *).
    (KnownNat n, IsNonZero n, HasKind (bv n), Integral (bv n),
     Show (bv n)) =>
    String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
    lift2IB "svTestBit"  SVal -> Int -> SVal
    svTestBit
       bitSizeMaybe :: IntN n -> Maybe Int
    bitSizeMaybe = Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> (IntN n -> Int) -> IntN n -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> IntN n -> Int
    forall a b. a -> b -> a
    const (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n))
       bitSize :: IntN n -> Int
    bitSize _    = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n)
       isSigned :: IntN n -> Bool
    isSigned     = Kind -> Bool
    forall a. HasKind a => a -> Bool
    hasSign (Kind -> Bool) -> (IntN n -> Kind) -> IntN n -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf
       bit :: Int -> IntN n
    bit i :: Int
    i        = 1 IntN n -> Int -> IntN n
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    i
       popCount :: IntN n -> Int
    popCount     = Int -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Int) -> (IntN n -> Int) -> IntN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Bits a => a -> Int
    popCount (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntN n -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    -- | 'SIntegral' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => SIntegral (WordN n)

    -- | 'SIntegral' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => SIntegral (IntN n)

    -- | 'SDivisible' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => SDivisible (WordN n) where
      sQuotRem :: WordN n -> WordN n -> (WordN n, WordN n)
    sQuotRem x :: WordN n
    x 0 = (0, WordN n
    x)
      sQuotRem x :: WordN n
    x y :: WordN n
    y = WordN n
    x WordN n -> WordN n -> (WordN n, WordN n)
    forall a. Integral a => a -> a -> (a, a)
    `quotRem` WordN n
    y
      sDivMod :: WordN n -> WordN n -> (WordN n, WordN n)
    sDivMod  x :: WordN n
    x 0 = (0, WordN n
    x)
      sDivMod  x :: WordN n
    x y :: WordN n
    y = WordN n
    x WordN n -> WordN n -> (WordN n, WordN n)
    forall a. Integral a => a -> a -> (a, a)
    `divMod` WordN n
    y

    -- | 'SDivisible' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => SDivisible (IntN n) where
      sQuotRem :: IntN n -> IntN n -> (IntN n, IntN n)
    sQuotRem x :: IntN n
    x 0 = (0, IntN n
    x)
      sQuotRem x :: IntN n
    x y :: IntN n
    y = IntN n
    x IntN n -> IntN n -> (IntN n, IntN n)
    forall a. Integral a => a -> a -> (a, a)
    `quotRem` IntN n
    y
      sDivMod :: IntN n -> IntN n -> (IntN n, IntN n)
    sDivMod  x :: IntN n
    x 0 = (0, IntN n
    x)
      sDivMod  x :: IntN n
    x y :: IntN n
    y = IntN n
    x IntN n -> IntN n -> (IntN n, IntN n)
    forall a. Integral a => a -> a -> (a, a)
    `divMod` IntN n
    y

    -- | 'SDivisible' instance for 'SWord'
    instance (KnownNat n, IsNonZero n) => SDivisible (SWord n) where
      sQuotRem :: SWord n -> SWord n -> (SWord n, SWord n)
    sQuotRem = SWord n -> SWord n -> (SWord n, SWord n)
    forall a. (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
    liftQRem
      sDivMod :: SWord n -> SWord n -> (SWord n, SWord n)
    sDivMod  = SWord n -> SWord n -> (SWord n, SWord n)
    forall a.
    (Ord a, SymVal a, Num a, SDivisible (SBV a)) =>
    SBV a -> SBV a -> (SBV a, SBV a)
    liftDMod

    -- | 'SDivisible' instance for 'SInt'
    instance (KnownNat n, IsNonZero n) => SDivisible (SInt n) where
      sQuotRem :: SInt n -> SInt n -> (SInt n, SInt n)
    sQuotRem = SInt n -> SInt n -> (SInt n, SInt n)
    forall a. (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
    liftQRem
      sDivMod :: SInt n -> SInt n -> (SInt n, SInt n)
    sDivMod  = SInt n -> SInt n -> (SInt n, SInt n)
    forall a.
    (Ord a, SymVal a, Num a, SDivisible (SBV a)) =>
    SBV a -> SBV a -> (SBV a, SBV a)
    liftDMod

    -- | 'SFiniteBits' instance for 'WordN'
    instance (KnownNat n, IsNonZero n) => SFiniteBits (WordN n) where
       sFiniteBitSize :: SBV (WordN n) -> Int
    sFiniteBitSize _ = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n)

    -- | 'SFiniteBits' instance for 'IntN'
    instance (KnownNat n, IsNonZero n) => SFiniteBits (IntN n) where
       sFiniteBitSize :: SBV (IntN n) -> Int
    sFiniteBitSize _ = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n)

    -- | Constructing models for 'WordN'
    instance (KnownNat n, IsNonZero n) => SatModel (WordN n) where
      parseCVs :: [CV] -> Maybe (WordN n, [CV])
    parseCVs = Kind -> [CV] -> Maybe (WordN n, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    genParse (WordN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (WordN n
    forall a. HasCallStack => a
    undefined :: WordN n))

    -- | Constructing models for 'IntN'
    instance (KnownNat n, IsNonZero n) => SatModel (IntN n) where
      parseCVs :: [CV] -> Maybe (IntN n, [CV])
    parseCVs = Kind -> [CV] -> Maybe (IntN n, [CV])
    forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
    genParse (IntN n -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (IntN n
    forall a. HasCallStack => a
    undefined :: IntN n))

    -- | Optimizing 'WordN'
    instance (KnownNat n, IsNonZero n) => Metric (WordN n)

    -- | Optimizing 'IntN'
    instance (KnownNat n, IsNonZero n) => Metric (IntN n) where
      type MetricSpace (IntN n) = WordN n
      toMetricSpace :: SBV (IntN n) -> SBV (MetricSpace (IntN n))
    toMetricSpace    x :: SBV (IntN n)
    x        = SBV (IntN n) -> SBV (WordN n)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SBV (IntN n)
    x SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    forall a. Num a => a -> a -> a
    + 2 SBV (WordN n) -> Int -> SBV (WordN n)
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)
      fromMetricSpace :: SBV (MetricSpace (IntN n)) -> SBV (IntN n)
    fromMetricSpace  x :: SBV (MetricSpace (IntN n))
    x        = SBV (WordN n) -> SBV (IntN n)
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SBV (MetricSpace (IntN n))
    SBV (WordN n)
    x SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    forall a. Num a => a -> a -> a
    - 2 SBV (IntN n) -> Int -> SBV (IntN n)
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)

    -- | Generalization of 'Data.SBV.sWord'
    sWord :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SWord n)
    sWord :: String -> m (SWord n)
    sWord = String -> m (SWord n)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    symbolic

    -- | Generalization of 'Data.SBV.sWord_'
    sWord_ :: (KnownNat n, IsNonZero n) => MonadSymbolic m => m (SWord n)
    sWord_ :: m (SWord n)
    sWord_ = m (SWord n)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    free_

    -- | Generalization of 'Data.SBV.sWord64s'
    sWords :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]
    sWords :: [String] -> m [SWord n]
    sWords = [String] -> m [SWord n]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [String] -> m [SBV a]
    symbolics

    -- | Generalization of 'Data.SBV.sInt'
    sInt :: (KnownNat n, IsNonZero n) => MonadSymbolic m => String -> m (SInt n)
    sInt :: String -> m (SInt n)
    sInt = String -> m (SInt n)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    symbolic

    -- | Generalization of 'Data.SBV.sInt_'
    sInt_ :: (KnownNat n, IsNonZero n) => MonadSymbolic m => m (SInt n)
    sInt_ :: m (SInt n)
    sInt_ = m (SInt n)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    free_

    -- | Generalization of 'Data.SBV.sInts'
    sInts :: (KnownNat n, IsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]
    sInts :: [String] -> m [SInt n]
    sInts = [String] -> m [SInt n]
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    [String] -> m [SBV a]
    symbolics

    -- | Extract a portion of bits to form a smaller bit-vector.
    --
    -- >>> prove $ \x -> bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)
    -- Q.E.D.
    bvExtract :: forall i j n bv proxy. ( KnownNat n, IsNonZero n, SymVal (bv n)
                                        , KnownNat i
                                        , KnownNat j
                                        , i + 1 <= n
                                        , j <= i
                                        , IsNonZero (i - j + 1)
                                        ) => proxy i                -- ^ @i@: Start position, numbered from @n-1@ to @0@
                                          -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold
                                          -> SBV (bv n)             -- ^ Input bit vector of size @n@
                                          -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@
    bvExtract :: proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract start :: proxy i
    start end :: proxy j
    end = SVal -> SBV (bv ((i - j) + 1))
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv ((i - j) + 1)))
    -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> SVal -> SVal
    svExtract Int
    i Int
    j (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV
       where i :: Int
    i  = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (proxy i -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy i
    start)
             j :: Int
    j  = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (proxy j -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy j
    end)

    -- | Join two bitvectors.
    --
    -- >>> prove $ \x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71))
    -- Q.E.D.
    (#) :: ( KnownNat n, IsNonZero n, SymVal (bv n)
           , KnownNat m, IsNonZero m, SymVal (bv m)
           ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side
             -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side
             -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@
    n :: SBV (bv n)
    n # :: SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # m :: SBV (bv m)
    m = SVal -> SBV (bv (n + m))
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv (n + m))) -> SVal -> SBV (bv (n + m))
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    svJoin (SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv n)
    n) (SBV (bv m) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv m)
    m)
    infixr 5 #

    -- | Zero extend a bit-vector.
    --
    -- >>> prove $ \x -> bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0
    -- Q.E.D.
    zeroExtend :: forall n m bv. ( KnownNat n, IsNonZero n, SymVal (bv n)
                                 , KnownNat m, IsNonZero m, SymVal (bv m)
                                 , n + 1 <= m
                                 , SIntegral (bv (m - n))
                                 , IsNonZero (m - n)
                                 ) => SBV (bv n)    -- ^ Input, of size @n@
                                   -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold
    zeroExtend :: SBV (bv n) -> SBV (bv m)
    zeroExtend n :: SBV (bv n)
    n = SVal -> SBV (bv m)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv m)) -> SVal -> SBV (bv m)
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    svJoin (SBV (bv (m - n)) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv (m - n))
    zero) (SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv n)
    n)
      where zero :: SBV (bv (m - n))
            zero :: SBV (bv (m - n))
    zero = bv (m - n) -> SBV (bv (m - n))
    forall a. SymVal a => a -> SBV a
    literal 0

    -- | Sign extend a bit-vector.
    --
    -- >>> prove $ \x -> sNot (msb x) .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== 0
    -- Q.E.D.
    -- >>> prove $ \x ->       msb x  .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== complement 0
    -- Q.E.D.
    signExtend :: forall n m bv. ( KnownNat n, IsNonZero n, SymVal (bv n)
                                 , KnownNat m, IsNonZero m, SymVal (bv m)
                                 , n + 1 <= m
                                 , SFiniteBits (bv n)
                                 , SIntegral   (bv (m - n))
                                 , IsNonZero   (m - n)
                                 ) => SBV (bv n)  -- ^ Input, of size @n@
                                   -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold
    signExtend :: SBV (bv n) -> SBV (bv m)
    signExtend n :: SBV (bv n)
    n = SVal -> SBV (bv m)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv m)) -> SVal -> SBV (bv m)
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal -> SVal
    svJoin (SBV (bv (m - n)) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv (m - n))
    ext) (SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV SBV (bv n)
    n)
      where zero, ones, ext :: SBV (bv (m - n))
            zero :: SBV (bv (m - n))
    zero = bv (m - n) -> SBV (bv (m - n))
    forall a. SymVal a => a -> SBV a
    literal 0
            ones :: SBV (bv (m - n))
    ones = SBV (bv (m - n)) -> SBV (bv (m - n))
    forall a. Bits a => a -> a
    complement SBV (bv (m - n))
    zero
            ext :: SBV (bv (m - n))
    ext  = SBool -> SBV (bv (m - n)) -> SBV (bv (m - n)) -> SBV (bv (m - n))
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV (bv n) -> SBool
    forall a. SFiniteBits a => SBV a -> SBool
    msb SBV (bv n)
    n) SBV (bv (m - n))
    ones SBV (bv (m - n))
    zero

    -- | Drop bits from the top of a bit-vector.
    --
    -- >>> prove $ \x -> bvDrop (Proxy @0) (x :: SWord 43) .== x
    -- Q.E.D.
    -- >>> prove $ \x -> bvDrop (Proxy @20) (x :: SWord 21) .== ite (lsb x) 1 0
    -- Q.E.D.
    bvDrop :: forall i n m bv proxy. ( KnownNat n, IsNonZero n
                                     , KnownNat i
                                     , i + 1 <= n
                                     , i + m - n <= 0
                                     , IsNonZero (n - i)
                                     ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.
                                       -> SBV (bv n)                 -- ^ Input, of size @n@
                                       -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.
    bvDrop :: proxy i -> SBV (bv n) -> SBV (bv m)
    bvDrop i :: proxy i
    i = SVal -> SBV (bv m)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv m))
    -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv m)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> SVal -> SVal
    svExtract Int
    start 0 (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV
      where nv :: Int
    nv    = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n)
            start :: Int
    start = Int
    nv Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (proxy i -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy i
    i) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1

    -- | Take bits from the top of a bit-vector.
    --
    -- >>> prove $ \x -> bvTake (Proxy @13) (x :: SWord 13) .== x
    -- Q.E.D.
    -- >>> prove $ \x -> bvTake (Proxy @1) (x :: SWord 13) .== ite (msb x) 1 0
    -- Q.E.D.
    -- >>> prove $ \x -> bvTake (Proxy @4) x # bvDrop (Proxy @4) x .== (x :: SWord 23)
    -- Q.E.D.
    bvTake :: forall i n bv proxy. ( KnownNat n, IsNonZero n
                                   , KnownNat i, IsNonZero i
                                   , i <= n
                                   ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.
                                     -> SBV (bv n)               -- ^ Input, of size @n@
                                     -> SBV (bv i)               -- ^ Output, of size @i@
    bvTake :: proxy i -> SBV (bv n) -> SBV (bv i)
    bvTake i :: proxy i
    i = SVal -> SBV (bv i)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (bv i))
    -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv i)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> SVal -> SVal
    svExtract Int
    start Int
    end (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV (bv n) -> SVal
    forall a. SBV a -> SVal
    unSBV
      where nv :: Int
    nv    = Proxy n -> Int
    forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy (Proxy n
    forall k (t :: k). Proxy t
    Proxy @n)
            start :: Int
    start = Int
    nv Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1
            end :: Int
    end   = Int
    start Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (proxy i -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy i
    i) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1

    -- | A helper class to convert sized bit-vectors to/from bytes.
    class ByteConverter a where
       -- | Convert to a sequence of bytes
       --
       -- >>> prove $ \a b c d -> toBytes ((fromBytes [a, b, c, d]) :: SWord 32) .== [a, b, c, d]
       -- Q.E.D.
       toBytes   :: a -> [SWord 8]

       -- | Convert from a sequence of bytes
       --
       -- >>> prove $ \r -> fromBytes (toBytes r) .== (r :: SWord 64)
       -- Q.E.D.
       fromBytes :: [SWord 8] -> a

    -- NB. The following instances are automatically generated by buildUtils/genByteConverter.hs
    -- It is possible to write these more compactly indeed, but this explicit form generates
    -- better C code, and hence we allow the verbosity here.

    -- | 'SWord' 8 instance for 'ByteConverter'
    instance ByteConverter (SWord 8) where
       toBytes :: SWord 8 -> [SWord 8]
    toBytes a :: SWord 8
    a = [SWord 8
    a]

       fromBytes :: [SWord 8] -> SWord 8
    fromBytes [x :: SWord 8
    x] = SWord 8
    x
       fromBytes as :: [SWord 8]
    as  = String -> SWord 8
    forall a. HasCallStack => String -> a
    error (String -> SWord 8) -> String -> SWord 8
    forall a b. (a -> b) -> a -> b
    $ "fromBytes:SWord 8: Incorrect number of bytes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([SWord 8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord 8]
    as)

    -- | 'SWord' 16 instance for 'ByteConverter'
    instance ByteConverter (SWord 16) where
       toBytes :: SWord 16 -> [SWord 8]
    toBytes a :: SWord 16
    a = [ Proxy 15 -> Proxy 8 -> SWord 16 -> SBV (WordN ((15 - 8) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 15
    forall k (t :: k). Proxy t
    Proxy @15) (Proxy 8
    forall k (t :: k). Proxy t
    Proxy  @8) SWord 16
    a
                   , Proxy 7 -> Proxy 0 -> SWord 16 -> SBV (WordN ((7 - 0) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 7
    forall k (t :: k). Proxy t
    Proxy  @7) (Proxy 0
    forall k (t :: k). Proxy t
    Proxy  @0) SWord 16
    a
                   ]

       fromBytes :: [SWord 8] -> SWord 16
    fromBytes as :: [SWord 8]
    as
         | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 2
         = ([SWord 8] -> SWord 8
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes :: [SWord 8] -> SWord 8) (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    take 1 [SWord 8]
    as) SWord 8 -> SWord 8 -> SBV (WordN (8 + 8))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
     SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # [SWord 8] -> SWord 8
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    drop 1 [SWord 8]
    as)
         | Bool
    True
         = String -> SWord 16
    forall a. HasCallStack => String -> a
    error (String -> SWord 16) -> String -> SWord 16
    forall a b. (a -> b) -> a -> b
    $ "fromBytes:SWord 16: Incorrect number of bytes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l
         where l :: Int
    l = [SWord 8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord 8]
    as

    -- | 'SWord' 32 instance for 'ByteConverter'
    instance ByteConverter (SWord 32) where
       toBytes :: SWord 32 -> [SWord 8]
    toBytes a :: SWord 32
    a = [ Proxy 31 -> Proxy 24 -> SWord 32 -> SBV (WordN ((31 - 24) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 31
    forall k (t :: k). Proxy t
    Proxy @31) (Proxy 24
    forall k (t :: k). Proxy t
    Proxy @24) SWord 32
    a, Proxy 23 -> Proxy 16 -> SWord 32 -> SBV (WordN ((23 - 16) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 23
    forall k (t :: k). Proxy t
    Proxy @23) (Proxy 16
    forall k (t :: k). Proxy t
    Proxy @16) SWord 32
    a, Proxy 15 -> Proxy 8 -> SWord 32 -> SBV (WordN ((15 - 8) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 15
    forall k (t :: k). Proxy t
    Proxy @15) (Proxy 8
    forall k (t :: k). Proxy t
    Proxy  @8) SWord 32
    a, Proxy 7 -> Proxy 0 -> SWord 32 -> SBV (WordN ((7 - 0) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 7
    forall k (t :: k). Proxy t
    Proxy  @7) (Proxy 0
    forall k (t :: k). Proxy t
    Proxy  @0) SWord 32
    a
                   ]

       fromBytes :: [SWord 8] -> SWord 32
    fromBytes as :: [SWord 8]
    as
         | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 4
         = ([SWord 8] -> SWord 16
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes :: [SWord 8] -> SWord 16) (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    take 2 [SWord 8]
    as) SWord 16 -> SWord 16 -> SBV (WordN (16 + 16))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
     SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # [SWord 8] -> SWord 16
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    drop 2 [SWord 8]
    as)
         | Bool
    True
         = String -> SWord 32
    forall a. HasCallStack => String -> a
    error (String -> SWord 32) -> String -> SWord 32
    forall a b. (a -> b) -> a -> b
    $ "fromBytes:SWord 32: Incorrect number of bytes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l
         where l :: Int
    l = [SWord 8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord 8]
    as

    -- | 'SWord' 64 instance for 'ByteConverter'
    instance ByteConverter (SWord 64) where
       toBytes :: SWord 64 -> [SWord 8]
    toBytes a :: SWord 64
    a = [ Proxy 63 -> Proxy 56 -> SWord 64 -> SBV (WordN ((63 - 56) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 63
    forall k (t :: k). Proxy t
    Proxy @63) (Proxy 56
    forall k (t :: k). Proxy t
    Proxy @56) SWord 64
    a, Proxy 55 -> Proxy 48 -> SWord 64 -> SBV (WordN ((55 - 48) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 55
    forall k (t :: k). Proxy t
    Proxy @55) (Proxy 48
    forall k (t :: k). Proxy t
    Proxy @48) SWord 64
    a, Proxy 47 -> Proxy 40 -> SWord 64 -> SBV (WordN ((47 - 40) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 47
    forall k (t :: k). Proxy t
    Proxy @47) (Proxy 40
    forall k (t :: k). Proxy t
    Proxy @40) SWord 64
    a, Proxy 39 -> Proxy 32 -> SWord 64 -> SBV (WordN ((39 - 32) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 39
    forall k (t :: k). Proxy t
    Proxy @39) (Proxy 32
    forall k (t :: k). Proxy t
    Proxy @32) SWord 64
    a
                   , Proxy 31 -> Proxy 24 -> SWord 64 -> SBV (WordN ((31 - 24) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 31
    forall k (t :: k). Proxy t
    Proxy @31) (Proxy 24
    forall k (t :: k). Proxy t
    Proxy @24) SWord 64
    a, Proxy 23 -> Proxy 16 -> SWord 64 -> SBV (WordN ((23 - 16) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 23
    forall k (t :: k). Proxy t
    Proxy @23) (Proxy 16
    forall k (t :: k). Proxy t
    Proxy @16) SWord 64
    a, Proxy 15 -> Proxy 8 -> SWord 64 -> SBV (WordN ((15 - 8) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 15
    forall k (t :: k). Proxy t
    Proxy @15) (Proxy 8
    forall k (t :: k). Proxy t
    Proxy  @8) SWord 64
    a, Proxy 7 -> Proxy 0 -> SWord 64 -> SBV (WordN ((7 - 0) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 7
    forall k (t :: k). Proxy t
    Proxy  @7) (Proxy 0
    forall k (t :: k). Proxy t
    Proxy  @0) SWord 64
    a
                   ]

       fromBytes :: [SWord 8] -> SWord 64
    fromBytes as :: [SWord 8]
    as
         | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 8
         = ([SWord 8] -> SWord 32
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes :: [SWord 8] -> SWord 32) (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    take 4 [SWord 8]
    as) SWord 32 -> SWord 32 -> SBV (WordN (32 + 32))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
     SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # [SWord 8] -> SWord 32
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    drop 4 [SWord 8]
    as)
         | Bool
    True
         = String -> SWord 64
    forall a. HasCallStack => String -> a
    error (String -> SWord 64) -> String -> SWord 64
    forall a b. (a -> b) -> a -> b
    $ "fromBytes:SWord 64: Incorrect number of bytes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l
         where l :: Int
    l = [SWord 8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord 8]
    as

    -- | 'SWord' 128 instance for 'ByteConverter'
    instance ByteConverter (SWord 128) where
       toBytes :: SWord 128 -> [SWord 8]
    toBytes a :: SWord 128
    a = [ Proxy 127
    -> Proxy 120 -> SWord 128 -> SBV (WordN ((127 - 120) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 127
    forall k (t :: k). Proxy t
    Proxy @127) (Proxy 120
    forall k (t :: k). Proxy t
    Proxy @120) SWord 128
    a, Proxy 119
    -> Proxy 112 -> SWord 128 -> SBV (WordN ((119 - 112) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 119
    forall k (t :: k). Proxy t
    Proxy @119) (Proxy 112
    forall k (t :: k). Proxy t
    Proxy @112) SWord 128
    a, Proxy 111
    -> Proxy 104 -> SWord 128 -> SBV (WordN ((111 - 104) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 111
    forall k (t :: k). Proxy t
    Proxy @111) (Proxy 104
    forall k (t :: k). Proxy t
    Proxy @104) SWord 128
    a, Proxy 103 -> Proxy 96 -> SWord 128 -> SBV (WordN ((103 - 96) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 103
    forall k (t :: k). Proxy t
    Proxy @103) (Proxy 96
    forall k (t :: k). Proxy t
    Proxy  @96) SWord 128
    a
                   , Proxy 95 -> Proxy 88 -> SWord 128 -> SBV (WordN ((95 - 88) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 95
    forall k (t :: k). Proxy t
    Proxy  @95) (Proxy 88
    forall k (t :: k). Proxy t
    Proxy  @88) SWord 128
    a, Proxy 87 -> Proxy 80 -> SWord 128 -> SBV (WordN ((87 - 80) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 87
    forall k (t :: k). Proxy t
    Proxy  @87) (Proxy 80
    forall k (t :: k). Proxy t
    Proxy  @80) SWord 128
    a, Proxy 79 -> Proxy 72 -> SWord 128 -> SBV (WordN ((79 - 72) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 79
    forall k (t :: k). Proxy t
    Proxy  @79) (Proxy 72
    forall k (t :: k). Proxy t
    Proxy  @72) SWord 128
    a, Proxy 71 -> Proxy 64 -> SWord 128 -> SBV (WordN ((71 - 64) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 71
    forall k (t :: k). Proxy t
    Proxy  @71) (Proxy 64
    forall k (t :: k). Proxy t
    Proxy  @64) SWord 128
    a
                   , Proxy 63 -> Proxy 56 -> SWord 128 -> SBV (WordN ((63 - 56) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 63
    forall k (t :: k). Proxy t
    Proxy  @63) (Proxy 56
    forall k (t :: k). Proxy t
    Proxy  @56) SWord 128
    a, Proxy 55 -> Proxy 48 -> SWord 128 -> SBV (WordN ((55 - 48) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 55
    forall k (t :: k). Proxy t
    Proxy  @55) (Proxy 48
    forall k (t :: k). Proxy t
    Proxy  @48) SWord 128
    a, Proxy 47 -> Proxy 40 -> SWord 128 -> SBV (WordN ((47 - 40) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 47
    forall k (t :: k). Proxy t
    Proxy  @47) (Proxy 40
    forall k (t :: k). Proxy t
    Proxy  @40) SWord 128
    a, Proxy 39 -> Proxy 32 -> SWord 128 -> SBV (WordN ((39 - 32) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 39
    forall k (t :: k). Proxy t
    Proxy  @39) (Proxy 32
    forall k (t :: k). Proxy t
    Proxy  @32) SWord 128
    a
                   , Proxy 31 -> Proxy 24 -> SWord 128 -> SBV (WordN ((31 - 24) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 31
    forall k (t :: k). Proxy t
    Proxy  @31) (Proxy 24
    forall k (t :: k). Proxy t
    Proxy  @24) SWord 128
    a, Proxy 23 -> Proxy 16 -> SWord 128 -> SBV (WordN ((23 - 16) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 23
    forall k (t :: k). Proxy t
    Proxy  @23) (Proxy 16
    forall k (t :: k). Proxy t
    Proxy  @16) SWord 128
    a, Proxy 15 -> Proxy 8 -> SWord 128 -> SBV (WordN ((15 - 8) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 15
    forall k (t :: k). Proxy t
    Proxy  @15) (Proxy 8
    forall k (t :: k). Proxy t
    Proxy   @8) SWord 128
    a, Proxy 7 -> Proxy 0 -> SWord 128 -> SBV (WordN ((7 - 0) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 7
    forall k (t :: k). Proxy t
    Proxy   @7) (Proxy 0
    forall k (t :: k). Proxy t
    Proxy   @0) SWord 128
    a
                   ]

       fromBytes :: [SWord 8] -> SWord 128
    fromBytes as :: [SWord 8]
    as
         | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 16
         = ([SWord 8] -> SWord 64
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes :: [SWord 8] -> SWord 64) (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    take 8 [SWord 8]
    as) SWord 64 -> SWord 64 -> SBV (WordN (64 + 64))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
     SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # [SWord 8] -> SWord 64
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    drop 8 [SWord 8]
    as)
         | Bool
    True
         = String -> SWord 128
    forall a. HasCallStack => String -> a
    error (String -> SWord 128) -> String -> SWord 128
    forall a b. (a -> b) -> a -> b
    $ "fromBytes:SWord 128: Incorrect number of bytes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l
         where l :: Int
    l = [SWord 8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord 8]
    as

    -- | 'SWord' 256 instance for 'ByteConverter'
    instance ByteConverter (SWord 256) where
       toBytes :: SWord 256 -> [SWord 8]
    toBytes a :: SWord 256
    a = [ Proxy 255
    -> Proxy 248 -> SWord 256 -> SBV (WordN ((255 - 248) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 255
    forall k (t :: k). Proxy t
    Proxy @255) (Proxy 248
    forall k (t :: k). Proxy t
    Proxy @248) SWord 256
    a, Proxy 247
    -> Proxy 240 -> SWord 256 -> SBV (WordN ((247 - 240) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 247
    forall k (t :: k). Proxy t
    Proxy @247) (Proxy 240
    forall k (t :: k). Proxy t
    Proxy @240) SWord 256
    a, Proxy 239
    -> Proxy 232 -> SWord 256 -> SBV (WordN ((239 - 232) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 239
    forall k (t :: k). Proxy t
    Proxy @239) (Proxy 232
    forall k (t :: k). Proxy t
    Proxy @232) SWord 256
    a, Proxy 231
    -> Proxy 224 -> SWord 256 -> SBV (WordN ((231 - 224) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 231
    forall k (t :: k). Proxy t
    Proxy @231) (Proxy 224
    forall k (t :: k). Proxy t
    Proxy @224) SWord 256
    a
                   , Proxy 223
    -> Proxy 216 -> SWord 256 -> SBV (WordN ((223 - 216) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 223
    forall k (t :: k). Proxy t
    Proxy @223) (Proxy 216
    forall k (t :: k). Proxy t
    Proxy @216) SWord 256
    a, Proxy 215
    -> Proxy 208 -> SWord 256 -> SBV (WordN ((215 - 208) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 215
    forall k (t :: k). Proxy t
    Proxy @215) (Proxy 208
    forall k (t :: k). Proxy t
    Proxy @208) SWord 256
    a, Proxy 207
    -> Proxy 200 -> SWord 256 -> SBV (WordN ((207 - 200) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 207
    forall k (t :: k). Proxy t
    Proxy @207) (Proxy 200
    forall k (t :: k). Proxy t
    Proxy @200) SWord 256
    a, Proxy 199
    -> Proxy 192 -> SWord 256 -> SBV (WordN ((199 - 192) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 199
    forall k (t :: k). Proxy t
    Proxy @199) (Proxy 192
    forall k (t :: k). Proxy t
    Proxy @192) SWord 256
    a
                   , Proxy 191
    -> Proxy 184 -> SWord 256 -> SBV (WordN ((191 - 184) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 191
    forall k (t :: k). Proxy t
    Proxy @191) (Proxy 184
    forall k (t :: k). Proxy t
    Proxy @184) SWord 256
    a, Proxy 183
    -> Proxy 176 -> SWord 256 -> SBV (WordN ((183 - 176) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 183
    forall k (t :: k). Proxy t
    Proxy @183) (Proxy 176
    forall k (t :: k). Proxy t
    Proxy @176) SWord 256
    a, Proxy 175
    -> Proxy 168 -> SWord 256 -> SBV (WordN ((175 - 168) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 175
    forall k (t :: k). Proxy t
    Proxy @175) (Proxy 168
    forall k (t :: k). Proxy t
    Proxy @168) SWord 256
    a, Proxy 167
    -> Proxy 160 -> SWord 256 -> SBV (WordN ((167 - 160) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 167
    forall k (t :: k). Proxy t
    Proxy @167) (Proxy 160
    forall k (t :: k). Proxy t
    Proxy @160) SWord 256
    a
                   , Proxy 159
    -> Proxy 152 -> SWord 256 -> SBV (WordN ((159 - 152) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 159
    forall k (t :: k). Proxy t
    Proxy @159) (Proxy 152
    forall k (t :: k). Proxy t
    Proxy @152) SWord 256
    a, Proxy 151
    -> Proxy 144 -> SWord 256 -> SBV (WordN ((151 - 144) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 151
    forall k (t :: k). Proxy t
    Proxy @151) (Proxy 144
    forall k (t :: k). Proxy t
    Proxy @144) SWord 256
    a, Proxy 143
    -> Proxy 136 -> SWord 256 -> SBV (WordN ((143 - 136) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 143
    forall k (t :: k). Proxy t
    Proxy @143) (Proxy 136
    forall k (t :: k). Proxy t
    Proxy @136) SWord 256
    a, Proxy 135
    -> Proxy 128 -> SWord 256 -> SBV (WordN ((135 - 128) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 135
    forall k (t :: k). Proxy t
    Proxy @135) (Proxy 128
    forall k (t :: k). Proxy t
    Proxy @128) SWord 256
    a
                   , Proxy 127
    -> Proxy 120 -> SWord 256 -> SBV (WordN ((127 - 120) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 127
    forall k (t :: k). Proxy t
    Proxy @127) (Proxy 120
    forall k (t :: k). Proxy t
    Proxy @120) SWord 256
    a, Proxy 119
    -> Proxy 112 -> SWord 256 -> SBV (WordN ((119 - 112) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 119
    forall k (t :: k). Proxy t
    Proxy @119) (Proxy 112
    forall k (t :: k). Proxy t
    Proxy @112) SWord 256
    a, Proxy 111
    -> Proxy 104 -> SWord 256 -> SBV (WordN ((111 - 104) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 111
    forall k (t :: k). Proxy t
    Proxy @111) (Proxy 104
    forall k (t :: k). Proxy t
    Proxy @104) SWord 256
    a, Proxy 103 -> Proxy 96 -> SWord 256 -> SBV (WordN ((103 - 96) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 103
    forall k (t :: k). Proxy t
    Proxy @103) (Proxy 96
    forall k (t :: k). Proxy t
    Proxy  @96) SWord 256
    a
                   , Proxy 95 -> Proxy 88 -> SWord 256 -> SBV (WordN ((95 - 88) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 95
    forall k (t :: k). Proxy t
    Proxy  @95) (Proxy 88
    forall k (t :: k). Proxy t
    Proxy  @88) SWord 256
    a, Proxy 87 -> Proxy 80 -> SWord 256 -> SBV (WordN ((87 - 80) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 87
    forall k (t :: k). Proxy t
    Proxy  @87) (Proxy 80
    forall k (t :: k). Proxy t
    Proxy  @80) SWord 256
    a, Proxy 79 -> Proxy 72 -> SWord 256 -> SBV (WordN ((79 - 72) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 79
    forall k (t :: k). Proxy t
    Proxy  @79) (Proxy 72
    forall k (t :: k). Proxy t
    Proxy  @72) SWord 256
    a, Proxy 71 -> Proxy 64 -> SWord 256 -> SBV (WordN ((71 - 64) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 71
    forall k (t :: k). Proxy t
    Proxy  @71) (Proxy 64
    forall k (t :: k). Proxy t
    Proxy  @64) SWord 256
    a
                   , Proxy 63 -> Proxy 56 -> SWord 256 -> SBV (WordN ((63 - 56) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 63
    forall k (t :: k). Proxy t
    Proxy  @63) (Proxy 56
    forall k (t :: k). Proxy t
    Proxy  @56) SWord 256
    a, Proxy 55 -> Proxy 48 -> SWord 256 -> SBV (WordN ((55 - 48) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 55
    forall k (t :: k). Proxy t
    Proxy  @55) (Proxy 48
    forall k (t :: k). Proxy t
    Proxy  @48) SWord 256
    a, Proxy 47 -> Proxy 40 -> SWord 256 -> SBV (WordN ((47 - 40) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 47
    forall k (t :: k). Proxy t
    Proxy  @47) (Proxy 40
    forall k (t :: k). Proxy t
    Proxy  @40) SWord 256
    a, Proxy 39 -> Proxy 32 -> SWord 256 -> SBV (WordN ((39 - 32) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 39
    forall k (t :: k). Proxy t
    Proxy  @39) (Proxy 32
    forall k (t :: k). Proxy t
    Proxy  @32) SWord 256
    a
                   , Proxy 31 -> Proxy 24 -> SWord 256 -> SBV (WordN ((31 - 24) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 31
    forall k (t :: k). Proxy t
    Proxy  @31) (Proxy 24
    forall k (t :: k). Proxy t
    Proxy  @24) SWord 256
    a, Proxy 23 -> Proxy 16 -> SWord 256 -> SBV (WordN ((23 - 16) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 23
    forall k (t :: k). Proxy t
    Proxy  @23) (Proxy 16
    forall k (t :: k). Proxy t
    Proxy  @16) SWord 256
    a, Proxy 15 -> Proxy 8 -> SWord 256 -> SBV (WordN ((15 - 8) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 15
    forall k (t :: k). Proxy t
    Proxy  @15) (Proxy 8
    forall k (t :: k). Proxy t
    Proxy   @8) SWord 256
    a, Proxy 7 -> Proxy 0 -> SWord 256 -> SBV (WordN ((7 - 0) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 7
    forall k (t :: k). Proxy t
    Proxy   @7) (Proxy 0
    forall k (t :: k). Proxy t
    Proxy   @0) SWord 256
    a
                   ]

       fromBytes :: [SWord 8] -> SWord 256
    fromBytes as :: [SWord 8]
    as
         | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 32
         = ([SWord 8] -> SWord 128
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes :: [SWord 8] -> SWord 128) (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    take 16 [SWord 8]
    as) SWord 128 -> SWord 128 -> SBV (WordN (128 + 128))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
     SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # [SWord 8] -> SWord 128
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    drop 16 [SWord 8]
    as)
         | Bool
    True
         = String -> SWord 256
    forall a. HasCallStack => String -> a
    error (String -> SWord 256) -> String -> SWord 256
    forall a b. (a -> b) -> a -> b
    $ "fromBytes:SWord 256: Incorrect number of bytes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l
         where l :: Int
    l = [SWord 8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord 8]
    as

    -- | 'SWord' 512 instance for 'ByteConverter'
    instance ByteConverter (SWord 512) where
       toBytes :: SWord 512 -> [SWord 8]
    toBytes a :: SWord 512
    a = [ Proxy 511
    -> Proxy 504 -> SWord 512 -> SBV (WordN ((511 - 504) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 511
    forall k (t :: k). Proxy t
    Proxy @511) (Proxy 504
    forall k (t :: k). Proxy t
    Proxy @504) SWord 512
    a, Proxy 503
    -> Proxy 496 -> SWord 512 -> SBV (WordN ((503 - 496) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 503
    forall k (t :: k). Proxy t
    Proxy @503) (Proxy 496
    forall k (t :: k). Proxy t
    Proxy @496) SWord 512
    a, Proxy 495
    -> Proxy 488 -> SWord 512 -> SBV (WordN ((495 - 488) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 495
    forall k (t :: k). Proxy t
    Proxy @495) (Proxy 488
    forall k (t :: k). Proxy t
    Proxy @488) SWord 512
    a, Proxy 487
    -> Proxy 480 -> SWord 512 -> SBV (WordN ((487 - 480) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 487
    forall k (t :: k). Proxy t
    Proxy @487) (Proxy 480
    forall k (t :: k). Proxy t
    Proxy @480) SWord 512
    a
                   , Proxy 479
    -> Proxy 472 -> SWord 512 -> SBV (WordN ((479 - 472) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 479
    forall k (t :: k). Proxy t
    Proxy @479) (Proxy 472
    forall k (t :: k). Proxy t
    Proxy @472) SWord 512
    a, Proxy 471
    -> Proxy 464 -> SWord 512 -> SBV (WordN ((471 - 464) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 471
    forall k (t :: k). Proxy t
    Proxy @471) (Proxy 464
    forall k (t :: k). Proxy t
    Proxy @464) SWord 512
    a, Proxy 463
    -> Proxy 456 -> SWord 512 -> SBV (WordN ((463 - 456) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 463
    forall k (t :: k). Proxy t
    Proxy @463) (Proxy 456
    forall k (t :: k). Proxy t
    Proxy @456) SWord 512
    a, Proxy 455
    -> Proxy 448 -> SWord 512 -> SBV (WordN ((455 - 448) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 455
    forall k (t :: k). Proxy t
    Proxy @455) (Proxy 448
    forall k (t :: k). Proxy t
    Proxy @448) SWord 512
    a
                   , Proxy 447
    -> Proxy 440 -> SWord 512 -> SBV (WordN ((447 - 440) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 447
    forall k (t :: k). Proxy t
    Proxy @447) (Proxy 440
    forall k (t :: k). Proxy t
    Proxy @440) SWord 512
    a, Proxy 439
    -> Proxy 432 -> SWord 512 -> SBV (WordN ((439 - 432) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 439
    forall k (t :: k). Proxy t
    Proxy @439) (Proxy 432
    forall k (t :: k). Proxy t
    Proxy @432) SWord 512
    a, Proxy 431
    -> Proxy 424 -> SWord 512 -> SBV (WordN ((431 - 424) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 431
    forall k (t :: k). Proxy t
    Proxy @431) (Proxy 424
    forall k (t :: k). Proxy t
    Proxy @424) SWord 512
    a, Proxy 423
    -> Proxy 416 -> SWord 512 -> SBV (WordN ((423 - 416) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 423
    forall k (t :: k). Proxy t
    Proxy @423) (Proxy 416
    forall k (t :: k). Proxy t
    Proxy @416) SWord 512
    a
                   , Proxy 415
    -> Proxy 408 -> SWord 512 -> SBV (WordN ((415 - 408) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 415
    forall k (t :: k). Proxy t
    Proxy @415) (Proxy 408
    forall k (t :: k). Proxy t
    Proxy @408) SWord 512
    a, Proxy 407
    -> Proxy 400 -> SWord 512 -> SBV (WordN ((407 - 400) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 407
    forall k (t :: k). Proxy t
    Proxy @407) (Proxy 400
    forall k (t :: k). Proxy t
    Proxy @400) SWord 512
    a, Proxy 399
    -> Proxy 392 -> SWord 512 -> SBV (WordN ((399 - 392) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 399
    forall k (t :: k). Proxy t
    Proxy @399) (Proxy 392
    forall k (t :: k). Proxy t
    Proxy @392) SWord 512
    a, Proxy 391
    -> Proxy 384 -> SWord 512 -> SBV (WordN ((391 - 384) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 391
    forall k (t :: k). Proxy t
    Proxy @391) (Proxy 384
    forall k (t :: k). Proxy t
    Proxy @384) SWord 512
    a
                   , Proxy 383
    -> Proxy 376 -> SWord 512 -> SBV (WordN ((383 - 376) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 383
    forall k (t :: k). Proxy t
    Proxy @383) (Proxy 376
    forall k (t :: k). Proxy t
    Proxy @376) SWord 512
    a, Proxy 375
    -> Proxy 368 -> SWord 512 -> SBV (WordN ((375 - 368) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 375
    forall k (t :: k). Proxy t
    Proxy @375) (Proxy 368
    forall k (t :: k). Proxy t
    Proxy @368) SWord 512
    a, Proxy 367
    -> Proxy 360 -> SWord 512 -> SBV (WordN ((367 - 360) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 367
    forall k (t :: k). Proxy t
    Proxy @367) (Proxy 360
    forall k (t :: k). Proxy t
    Proxy @360) SWord 512
    a, Proxy 359
    -> Proxy 352 -> SWord 512 -> SBV (WordN ((359 - 352) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 359
    forall k (t :: k). Proxy t
    Proxy @359) (Proxy 352
    forall k (t :: k). Proxy t
    Proxy @352) SWord 512
    a
                   , Proxy 351
    -> Proxy 344 -> SWord 512 -> SBV (WordN ((351 - 344) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 351
    forall k (t :: k). Proxy t
    Proxy @351) (Proxy 344
    forall k (t :: k). Proxy t
    Proxy @344) SWord 512
    a, Proxy 343
    -> Proxy 336 -> SWord 512 -> SBV (WordN ((343 - 336) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 343
    forall k (t :: k). Proxy t
    Proxy @343) (Proxy 336
    forall k (t :: k). Proxy t
    Proxy @336) SWord 512
    a, Proxy 335
    -> Proxy 328 -> SWord 512 -> SBV (WordN ((335 - 328) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 335
    forall k (t :: k). Proxy t
    Proxy @335) (Proxy 328
    forall k (t :: k). Proxy t
    Proxy @328) SWord 512
    a, Proxy 327
    -> Proxy 320 -> SWord 512 -> SBV (WordN ((327 - 320) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 327
    forall k (t :: k). Proxy t
    Proxy @327) (Proxy 320
    forall k (t :: k). Proxy t
    Proxy @320) SWord 512
    a
                   , Proxy 319
    -> Proxy 312 -> SWord 512 -> SBV (WordN ((319 - 312) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 319
    forall k (t :: k). Proxy t
    Proxy @319) (Proxy 312
    forall k (t :: k). Proxy t
    Proxy @312) SWord 512
    a, Proxy 311
    -> Proxy 304 -> SWord 512 -> SBV (WordN ((311 - 304) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 311
    forall k (t :: k). Proxy t
    Proxy @311) (Proxy 304
    forall k (t :: k). Proxy t
    Proxy @304) SWord 512
    a, Proxy 303
    -> Proxy 296 -> SWord 512 -> SBV (WordN ((303 - 296) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 303
    forall k (t :: k). Proxy t
    Proxy @303) (Proxy 296
    forall k (t :: k). Proxy t
    Proxy @296) SWord 512
    a, Proxy 295
    -> Proxy 288 -> SWord 512 -> SBV (WordN ((295 - 288) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 295
    forall k (t :: k). Proxy t
    Proxy @295) (Proxy 288
    forall k (t :: k). Proxy t
    Proxy @288) SWord 512
    a
                   , Proxy 287
    -> Proxy 280 -> SWord 512 -> SBV (WordN ((287 - 280) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 287
    forall k (t :: k). Proxy t
    Proxy @287) (Proxy 280
    forall k (t :: k). Proxy t
    Proxy @280) SWord 512
    a, Proxy 279
    -> Proxy 272 -> SWord 512 -> SBV (WordN ((279 - 272) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 279
    forall k (t :: k). Proxy t
    Proxy @279) (Proxy 272
    forall k (t :: k). Proxy t
    Proxy @272) SWord 512
    a, Proxy 271
    -> Proxy 264 -> SWord 512 -> SBV (WordN ((271 - 264) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 271
    forall k (t :: k). Proxy t
    Proxy @271) (Proxy 264
    forall k (t :: k). Proxy t
    Proxy @264) SWord 512
    a, Proxy 263
    -> Proxy 256 -> SWord 512 -> SBV (WordN ((263 - 256) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 263
    forall k (t :: k). Proxy t
    Proxy @263) (Proxy 256
    forall k (t :: k). Proxy t
    Proxy @256) SWord 512
    a
                   , Proxy 255
    -> Proxy 248 -> SWord 512 -> SBV (WordN ((255 - 248) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 255
    forall k (t :: k). Proxy t
    Proxy @255) (Proxy 248
    forall k (t :: k). Proxy t
    Proxy @248) SWord 512
    a, Proxy 247
    -> Proxy 240 -> SWord 512 -> SBV (WordN ((247 - 240) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 247
    forall k (t :: k). Proxy t
    Proxy @247) (Proxy 240
    forall k (t :: k). Proxy t
    Proxy @240) SWord 512
    a, Proxy 239
    -> Proxy 232 -> SWord 512 -> SBV (WordN ((239 - 232) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 239
    forall k (t :: k). Proxy t
    Proxy @239) (Proxy 232
    forall k (t :: k). Proxy t
    Proxy @232) SWord 512
    a, Proxy 231
    -> Proxy 224 -> SWord 512 -> SBV (WordN ((231 - 224) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 231
    forall k (t :: k). Proxy t
    Proxy @231) (Proxy 224
    forall k (t :: k). Proxy t
    Proxy @224) SWord 512
    a
                   , Proxy 223
    -> Proxy 216 -> SWord 512 -> SBV (WordN ((223 - 216) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 223
    forall k (t :: k). Proxy t
    Proxy @223) (Proxy 216
    forall k (t :: k). Proxy t
    Proxy @216) SWord 512
    a, Proxy 215
    -> Proxy 208 -> SWord 512 -> SBV (WordN ((215 - 208) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 215
    forall k (t :: k). Proxy t
    Proxy @215) (Proxy 208
    forall k (t :: k). Proxy t
    Proxy @208) SWord 512
    a, Proxy 207
    -> Proxy 200 -> SWord 512 -> SBV (WordN ((207 - 200) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 207
    forall k (t :: k). Proxy t
    Proxy @207) (Proxy 200
    forall k (t :: k). Proxy t
    Proxy @200) SWord 512
    a, Proxy 199
    -> Proxy 192 -> SWord 512 -> SBV (WordN ((199 - 192) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 199
    forall k (t :: k). Proxy t
    Proxy @199) (Proxy 192
    forall k (t :: k). Proxy t
    Proxy @192) SWord 512
    a
                   , Proxy 191
    -> Proxy 184 -> SWord 512 -> SBV (WordN ((191 - 184) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 191
    forall k (t :: k). Proxy t
    Proxy @191) (Proxy 184
    forall k (t :: k). Proxy t
    Proxy @184) SWord 512
    a, Proxy 183
    -> Proxy 176 -> SWord 512 -> SBV (WordN ((183 - 176) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 183
    forall k (t :: k). Proxy t
    Proxy @183) (Proxy 176
    forall k (t :: k). Proxy t
    Proxy @176) SWord 512
    a, Proxy 175
    -> Proxy 168 -> SWord 512 -> SBV (WordN ((175 - 168) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 175
    forall k (t :: k). Proxy t
    Proxy @175) (Proxy 168
    forall k (t :: k). Proxy t
    Proxy @168) SWord 512
    a, Proxy 167
    -> Proxy 160 -> SWord 512 -> SBV (WordN ((167 - 160) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 167
    forall k (t :: k). Proxy t
    Proxy @167) (Proxy 160
    forall k (t :: k). Proxy t
    Proxy @160) SWord 512
    a
                   , Proxy 159
    -> Proxy 152 -> SWord 512 -> SBV (WordN ((159 - 152) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 159
    forall k (t :: k). Proxy t
    Proxy @159) (Proxy 152
    forall k (t :: k). Proxy t
    Proxy @152) SWord 512
    a, Proxy 151
    -> Proxy 144 -> SWord 512 -> SBV (WordN ((151 - 144) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 151
    forall k (t :: k). Proxy t
    Proxy @151) (Proxy 144
    forall k (t :: k). Proxy t
    Proxy @144) SWord 512
    a, Proxy 143
    -> Proxy 136 -> SWord 512 -> SBV (WordN ((143 - 136) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 143
    forall k (t :: k). Proxy t
    Proxy @143) (Proxy 136
    forall k (t :: k). Proxy t
    Proxy @136) SWord 512
    a, Proxy 135
    -> Proxy 128 -> SWord 512 -> SBV (WordN ((135 - 128) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 135
    forall k (t :: k). Proxy t
    Proxy @135) (Proxy 128
    forall k (t :: k). Proxy t
    Proxy @128) SWord 512
    a
                   , Proxy 127
    -> Proxy 120 -> SWord 512 -> SBV (WordN ((127 - 120) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 127
    forall k (t :: k). Proxy t
    Proxy @127) (Proxy 120
    forall k (t :: k). Proxy t
    Proxy @120) SWord 512
    a, Proxy 119
    -> Proxy 112 -> SWord 512 -> SBV (WordN ((119 - 112) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 119
    forall k (t :: k). Proxy t
    Proxy @119) (Proxy 112
    forall k (t :: k). Proxy t
    Proxy @112) SWord 512
    a, Proxy 111
    -> Proxy 104 -> SWord 512 -> SBV (WordN ((111 - 104) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 111
    forall k (t :: k). Proxy t
    Proxy @111) (Proxy 104
    forall k (t :: k). Proxy t
    Proxy @104) SWord 512
    a, Proxy 103 -> Proxy 96 -> SWord 512 -> SBV (WordN ((103 - 96) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 103
    forall k (t :: k). Proxy t
    Proxy @103) (Proxy 96
    forall k (t :: k). Proxy t
    Proxy  @96) SWord 512
    a
                   , Proxy 95 -> Proxy 88 -> SWord 512 -> SBV (WordN ((95 - 88) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 95
    forall k (t :: k). Proxy t
    Proxy  @95) (Proxy 88
    forall k (t :: k). Proxy t
    Proxy  @88) SWord 512
    a, Proxy 87 -> Proxy 80 -> SWord 512 -> SBV (WordN ((87 - 80) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 87
    forall k (t :: k). Proxy t
    Proxy  @87) (Proxy 80
    forall k (t :: k). Proxy t
    Proxy  @80) SWord 512
    a, Proxy 79 -> Proxy 72 -> SWord 512 -> SBV (WordN ((79 - 72) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 79
    forall k (t :: k). Proxy t
    Proxy  @79) (Proxy 72
    forall k (t :: k). Proxy t
    Proxy  @72) SWord 512
    a, Proxy 71 -> Proxy 64 -> SWord 512 -> SBV (WordN ((71 - 64) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 71
    forall k (t :: k). Proxy t
    Proxy  @71) (Proxy 64
    forall k (t :: k). Proxy t
    Proxy  @64) SWord 512
    a
                   , Proxy 63 -> Proxy 56 -> SWord 512 -> SBV (WordN ((63 - 56) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 63
    forall k (t :: k). Proxy t
    Proxy  @63) (Proxy 56
    forall k (t :: k). Proxy t
    Proxy  @56) SWord 512
    a, Proxy 55 -> Proxy 48 -> SWord 512 -> SBV (WordN ((55 - 48) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 55
    forall k (t :: k). Proxy t
    Proxy  @55) (Proxy 48
    forall k (t :: k). Proxy t
    Proxy  @48) SWord 512
    a, Proxy 47 -> Proxy 40 -> SWord 512 -> SBV (WordN ((47 - 40) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 47
    forall k (t :: k). Proxy t
    Proxy  @47) (Proxy 40
    forall k (t :: k). Proxy t
    Proxy  @40) SWord 512
    a, Proxy 39 -> Proxy 32 -> SWord 512 -> SBV (WordN ((39 - 32) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 39
    forall k (t :: k). Proxy t
    Proxy  @39) (Proxy 32
    forall k (t :: k). Proxy t
    Proxy  @32) SWord 512
    a
                   , Proxy 31 -> Proxy 24 -> SWord 512 -> SBV (WordN ((31 - 24) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 31
    forall k (t :: k). Proxy t
    Proxy  @31) (Proxy 24
    forall k (t :: k). Proxy t
    Proxy  @24) SWord 512
    a, Proxy 23 -> Proxy 16 -> SWord 512 -> SBV (WordN ((23 - 16) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 23
    forall k (t :: k). Proxy t
    Proxy  @23) (Proxy 16
    forall k (t :: k). Proxy t
    Proxy  @16) SWord 512
    a, Proxy 15 -> Proxy 8 -> SWord 512 -> SBV (WordN ((15 - 8) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 15
    forall k (t :: k). Proxy t
    Proxy  @15) (Proxy 8
    forall k (t :: k). Proxy t
    Proxy   @8) SWord 512
    a, Proxy 7 -> Proxy 0 -> SWord 512 -> SBV (WordN ((7 - 0) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 7
    forall k (t :: k). Proxy t
    Proxy   @7) (Proxy 0
    forall k (t :: k). Proxy t
    Proxy   @0) SWord 512
    a
                   ]

       fromBytes :: [SWord 8] -> SWord 512
    fromBytes as :: [SWord 8]
    as
         | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 64
         = ([SWord 8] -> SWord 256
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes :: [SWord 8] -> SWord 256) (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    take 32 [SWord 8]
    as) SWord 256 -> SWord 256 -> SBV (WordN (256 + 256))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
     SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # [SWord 8] -> SWord 256
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    drop 32 [SWord 8]
    as)
         | Bool
    True
         = String -> SWord 512
    forall a. HasCallStack => String -> a
    error (String -> SWord 512) -> String -> SWord 512
    forall a b. (a -> b) -> a -> b
    $ "fromBytes:SWord 512: Incorrect number of bytes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l
         where l :: Int
    l = [SWord 8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord 8]
    as

    -- | 'SWord' 1024 instance for 'ByteConverter'
    instance ByteConverter (SWord 1024) where
       toBytes :: SWord 1024 -> [SWord 8]
    toBytes a :: SWord 1024
    a = [ Proxy 1023
    -> Proxy 1016 -> SWord 1024 -> SBV (WordN ((1023 - 1016) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 1023
    forall k (t :: k). Proxy t
    Proxy @1023) (Proxy 1016
    forall k (t :: k). Proxy t
    Proxy @1016) SWord 1024
    a, Proxy 1015
    -> Proxy 1008 -> SWord 1024 -> SBV (WordN ((1015 - 1008) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 1015
    forall k (t :: k). Proxy t
    Proxy @1015) (Proxy 1008
    forall k (t :: k). Proxy t
    Proxy @1008) SWord 1024
    a, Proxy 1007
    -> Proxy 1000 -> SWord 1024 -> SBV (WordN ((1007 - 1000) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 1007
    forall k (t :: k). Proxy t
    Proxy @1007) (Proxy 1000
    forall k (t :: k). Proxy t
    Proxy @1000) SWord 1024
    a, Proxy 999
    -> Proxy 992 -> SWord 1024 -> SBV (WordN ((999 - 992) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 999
    forall k (t :: k). Proxy t
    Proxy  @999) (Proxy 992
    forall k (t :: k). Proxy t
    Proxy  @992) SWord 1024
    a
                   , Proxy 991
    -> Proxy 984 -> SWord 1024 -> SBV (WordN ((991 - 984) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 991
    forall k (t :: k). Proxy t
    Proxy  @991) (Proxy 984
    forall k (t :: k). Proxy t
    Proxy  @984) SWord 1024
    a, Proxy 983
    -> Proxy 976 -> SWord 1024 -> SBV (WordN ((983 - 976) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 983
    forall k (t :: k). Proxy t
    Proxy  @983) (Proxy 976
    forall k (t :: k). Proxy t
    Proxy  @976) SWord 1024
    a, Proxy 975
    -> Proxy 968 -> SWord 1024 -> SBV (WordN ((975 - 968) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 975
    forall k (t :: k). Proxy t
    Proxy  @975) (Proxy 968
    forall k (t :: k). Proxy t
    Proxy  @968) SWord 1024
    a, Proxy 967
    -> Proxy 960 -> SWord 1024 -> SBV (WordN ((967 - 960) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 967
    forall k (t :: k). Proxy t
    Proxy  @967) (Proxy 960
    forall k (t :: k). Proxy t
    Proxy  @960) SWord 1024
    a
                   , Proxy 959
    -> Proxy 952 -> SWord 1024 -> SBV (WordN ((959 - 952) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 959
    forall k (t :: k). Proxy t
    Proxy  @959) (Proxy 952
    forall k (t :: k). Proxy t
    Proxy  @952) SWord 1024
    a, Proxy 951
    -> Proxy 944 -> SWord 1024 -> SBV (WordN ((951 - 944) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 951
    forall k (t :: k). Proxy t
    Proxy  @951) (Proxy 944
    forall k (t :: k). Proxy t
    Proxy  @944) SWord 1024
    a, Proxy 943
    -> Proxy 936 -> SWord 1024 -> SBV (WordN ((943 - 936) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 943
    forall k (t :: k). Proxy t
    Proxy  @943) (Proxy 936
    forall k (t :: k). Proxy t
    Proxy  @936) SWord 1024
    a, Proxy 935
    -> Proxy 928 -> SWord 1024 -> SBV (WordN ((935 - 928) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 935
    forall k (t :: k). Proxy t
    Proxy  @935) (Proxy 928
    forall k (t :: k). Proxy t
    Proxy  @928) SWord 1024
    a
                   , Proxy 927
    -> Proxy 920 -> SWord 1024 -> SBV (WordN ((927 - 920) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 927
    forall k (t :: k). Proxy t
    Proxy  @927) (Proxy 920
    forall k (t :: k). Proxy t
    Proxy  @920) SWord 1024
    a, Proxy 919
    -> Proxy 912 -> SWord 1024 -> SBV (WordN ((919 - 912) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 919
    forall k (t :: k). Proxy t
    Proxy  @919) (Proxy 912
    forall k (t :: k). Proxy t
    Proxy  @912) SWord 1024
    a, Proxy 911
    -> Proxy 904 -> SWord 1024 -> SBV (WordN ((911 - 904) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 911
    forall k (t :: k). Proxy t
    Proxy  @911) (Proxy 904
    forall k (t :: k). Proxy t
    Proxy  @904) SWord 1024
    a, Proxy 903
    -> Proxy 896 -> SWord 1024 -> SBV (WordN ((903 - 896) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 903
    forall k (t :: k). Proxy t
    Proxy  @903) (Proxy 896
    forall k (t :: k). Proxy t
    Proxy  @896) SWord 1024
    a
                   , Proxy 895
    -> Proxy 888 -> SWord 1024 -> SBV (WordN ((895 - 888) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 895
    forall k (t :: k). Proxy t
    Proxy  @895) (Proxy 888
    forall k (t :: k). Proxy t
    Proxy  @888) SWord 1024
    a, Proxy 887
    -> Proxy 880 -> SWord 1024 -> SBV (WordN ((887 - 880) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 887
    forall k (t :: k). Proxy t
    Proxy  @887) (Proxy 880
    forall k (t :: k). Proxy t
    Proxy  @880) SWord 1024
    a, Proxy 879
    -> Proxy 872 -> SWord 1024 -> SBV (WordN ((879 - 872) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 879
    forall k (t :: k). Proxy t
    Proxy  @879) (Proxy 872
    forall k (t :: k). Proxy t
    Proxy  @872) SWord 1024
    a, Proxy 871
    -> Proxy 864 -> SWord 1024 -> SBV (WordN ((871 - 864) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 871
    forall k (t :: k). Proxy t
    Proxy  @871) (Proxy 864
    forall k (t :: k). Proxy t
    Proxy  @864) SWord 1024
    a
                   , Proxy 863
    -> Proxy 856 -> SWord 1024 -> SBV (WordN ((863 - 856) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 863
    forall k (t :: k). Proxy t
    Proxy  @863) (Proxy 856
    forall k (t :: k). Proxy t
    Proxy  @856) SWord 1024
    a, Proxy 855
    -> Proxy 848 -> SWord 1024 -> SBV (WordN ((855 - 848) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 855
    forall k (t :: k). Proxy t
    Proxy  @855) (Proxy 848
    forall k (t :: k). Proxy t
    Proxy  @848) SWord 1024
    a, Proxy 847
    -> Proxy 840 -> SWord 1024 -> SBV (WordN ((847 - 840) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 847
    forall k (t :: k). Proxy t
    Proxy  @847) (Proxy 840
    forall k (t :: k). Proxy t
    Proxy  @840) SWord 1024
    a, Proxy 839
    -> Proxy 832 -> SWord 1024 -> SBV (WordN ((839 - 832) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 839
    forall k (t :: k). Proxy t
    Proxy  @839) (Proxy 832
    forall k (t :: k). Proxy t
    Proxy  @832) SWord 1024
    a
                   , Proxy 831
    -> Proxy 824 -> SWord 1024 -> SBV (WordN ((831 - 824) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 831
    forall k (t :: k). Proxy t
    Proxy  @831) (Proxy 824
    forall k (t :: k). Proxy t
    Proxy  @824) SWord 1024
    a, Proxy 823
    -> Proxy 816 -> SWord 1024 -> SBV (WordN ((823 - 816) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 823
    forall k (t :: k). Proxy t
    Proxy  @823) (Proxy 816
    forall k (t :: k). Proxy t
    Proxy  @816) SWord 1024
    a, Proxy 815
    -> Proxy 808 -> SWord 1024 -> SBV (WordN ((815 - 808) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 815
    forall k (t :: k). Proxy t
    Proxy  @815) (Proxy 808
    forall k (t :: k). Proxy t
    Proxy  @808) SWord 1024
    a, Proxy 807
    -> Proxy 800 -> SWord 1024 -> SBV (WordN ((807 - 800) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 807
    forall k (t :: k). Proxy t
    Proxy  @807) (Proxy 800
    forall k (t :: k). Proxy t
    Proxy  @800) SWord 1024
    a
                   , Proxy 799
    -> Proxy 792 -> SWord 1024 -> SBV (WordN ((799 - 792) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 799
    forall k (t :: k). Proxy t
    Proxy  @799) (Proxy 792
    forall k (t :: k). Proxy t
    Proxy  @792) SWord 1024
    a, Proxy 791
    -> Proxy 784 -> SWord 1024 -> SBV (WordN ((791 - 784) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 791
    forall k (t :: k). Proxy t
    Proxy  @791) (Proxy 784
    forall k (t :: k). Proxy t
    Proxy  @784) SWord 1024
    a, Proxy 783
    -> Proxy 776 -> SWord 1024 -> SBV (WordN ((783 - 776) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 783
    forall k (t :: k). Proxy t
    Proxy  @783) (Proxy 776
    forall k (t :: k). Proxy t
    Proxy  @776) SWord 1024
    a, Proxy 775
    -> Proxy 768 -> SWord 1024 -> SBV (WordN ((775 - 768) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 775
    forall k (t :: k). Proxy t
    Proxy  @775) (Proxy 768
    forall k (t :: k). Proxy t
    Proxy  @768) SWord 1024
    a
                   , Proxy 767
    -> Proxy 760 -> SWord 1024 -> SBV (WordN ((767 - 760) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 767
    forall k (t :: k). Proxy t
    Proxy  @767) (Proxy 760
    forall k (t :: k). Proxy t
    Proxy  @760) SWord 1024
    a, Proxy 759
    -> Proxy 752 -> SWord 1024 -> SBV (WordN ((759 - 752) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 759
    forall k (t :: k). Proxy t
    Proxy  @759) (Proxy 752
    forall k (t :: k). Proxy t
    Proxy  @752) SWord 1024
    a, Proxy 751
    -> Proxy 744 -> SWord 1024 -> SBV (WordN ((751 - 744) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 751
    forall k (t :: k). Proxy t
    Proxy  @751) (Proxy 744
    forall k (t :: k). Proxy t
    Proxy  @744) SWord 1024
    a, Proxy 743
    -> Proxy 736 -> SWord 1024 -> SBV (WordN ((743 - 736) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 743
    forall k (t :: k). Proxy t
    Proxy  @743) (Proxy 736
    forall k (t :: k). Proxy t
    Proxy  @736) SWord 1024
    a
                   , Proxy 735
    -> Proxy 728 -> SWord 1024 -> SBV (WordN ((735 - 728) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 735
    forall k (t :: k). Proxy t
    Proxy  @735) (Proxy 728
    forall k (t :: k). Proxy t
    Proxy  @728) SWord 1024
    a, Proxy 727
    -> Proxy 720 -> SWord 1024 -> SBV (WordN ((727 - 720) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 727
    forall k (t :: k). Proxy t
    Proxy  @727) (Proxy 720
    forall k (t :: k). Proxy t
    Proxy  @720) SWord 1024
    a, Proxy 719
    -> Proxy 712 -> SWord 1024 -> SBV (WordN ((719 - 712) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 719
    forall k (t :: k). Proxy t
    Proxy  @719) (Proxy 712
    forall k (t :: k). Proxy t
    Proxy  @712) SWord 1024
    a, Proxy 711
    -> Proxy 704 -> SWord 1024 -> SBV (WordN ((711 - 704) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 711
    forall k (t :: k). Proxy t
    Proxy  @711) (Proxy 704
    forall k (t :: k). Proxy t
    Proxy  @704) SWord 1024
    a
                   , Proxy 703
    -> Proxy 696 -> SWord 1024 -> SBV (WordN ((703 - 696) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 703
    forall k (t :: k). Proxy t
    Proxy  @703) (Proxy 696
    forall k (t :: k). Proxy t
    Proxy  @696) SWord 1024
    a, Proxy 695
    -> Proxy 688 -> SWord 1024 -> SBV (WordN ((695 - 688) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 695
    forall k (t :: k). Proxy t
    Proxy  @695) (Proxy 688
    forall k (t :: k). Proxy t
    Proxy  @688) SWord 1024
    a, Proxy 687
    -> Proxy 680 -> SWord 1024 -> SBV (WordN ((687 - 680) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 687
    forall k (t :: k). Proxy t
    Proxy  @687) (Proxy 680
    forall k (t :: k). Proxy t
    Proxy  @680) SWord 1024
    a, Proxy 679
    -> Proxy 672 -> SWord 1024 -> SBV (WordN ((679 - 672) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 679
    forall k (t :: k). Proxy t
    Proxy  @679) (Proxy 672
    forall k (t :: k). Proxy t
    Proxy  @672) SWord 1024
    a
                   , Proxy 671
    -> Proxy 664 -> SWord 1024 -> SBV (WordN ((671 - 664) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 671
    forall k (t :: k). Proxy t
    Proxy  @671) (Proxy 664
    forall k (t :: k). Proxy t
    Proxy  @664) SWord 1024
    a, Proxy 663
    -> Proxy 656 -> SWord 1024 -> SBV (WordN ((663 - 656) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 663
    forall k (t :: k). Proxy t
    Proxy  @663) (Proxy 656
    forall k (t :: k). Proxy t
    Proxy  @656) SWord 1024
    a, Proxy 655
    -> Proxy 648 -> SWord 1024 -> SBV (WordN ((655 - 648) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 655
    forall k (t :: k). Proxy t
    Proxy  @655) (Proxy 648
    forall k (t :: k). Proxy t
    Proxy  @648) SWord 1024
    a, Proxy 647
    -> Proxy 640 -> SWord 1024 -> SBV (WordN ((647 - 640) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 647
    forall k (t :: k). Proxy t
    Proxy  @647) (Proxy 640
    forall k (t :: k). Proxy t
    Proxy  @640) SWord 1024
    a
                   , Proxy 639
    -> Proxy 632 -> SWord 1024 -> SBV (WordN ((639 - 632) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 639
    forall k (t :: k). Proxy t
    Proxy  @639) (Proxy 632
    forall k (t :: k). Proxy t
    Proxy  @632) SWord 1024
    a, Proxy 631
    -> Proxy 624 -> SWord 1024 -> SBV (WordN ((631 - 624) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 631
    forall k (t :: k). Proxy t
    Proxy  @631) (Proxy 624
    forall k (t :: k). Proxy t
    Proxy  @624) SWord 1024
    a, Proxy 623
    -> Proxy 616 -> SWord 1024 -> SBV (WordN ((623 - 616) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 623
    forall k (t :: k). Proxy t
    Proxy  @623) (Proxy 616
    forall k (t :: k). Proxy t
    Proxy  @616) SWord 1024
    a, Proxy 615
    -> Proxy 608 -> SWord 1024 -> SBV (WordN ((615 - 608) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 615
    forall k (t :: k). Proxy t
    Proxy  @615) (Proxy 608
    forall k (t :: k). Proxy t
    Proxy  @608) SWord 1024
    a
                   , Proxy 607
    -> Proxy 600 -> SWord 1024 -> SBV (WordN ((607 - 600) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 607
    forall k (t :: k). Proxy t
    Proxy  @607) (Proxy 600
    forall k (t :: k). Proxy t
    Proxy  @600) SWord 1024
    a, Proxy 599
    -> Proxy 592 -> SWord 1024 -> SBV (WordN ((599 - 592) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 599
    forall k (t :: k). Proxy t
    Proxy  @599) (Proxy 592
    forall k (t :: k). Proxy t
    Proxy  @592) SWord 1024
    a, Proxy 591
    -> Proxy 584 -> SWord 1024 -> SBV (WordN ((591 - 584) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 591
    forall k (t :: k). Proxy t
    Proxy  @591) (Proxy 584
    forall k (t :: k). Proxy t
    Proxy  @584) SWord 1024
    a, Proxy 583
    -> Proxy 576 -> SWord 1024 -> SBV (WordN ((583 - 576) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 583
    forall k (t :: k). Proxy t
    Proxy  @583) (Proxy 576
    forall k (t :: k). Proxy t
    Proxy  @576) SWord 1024
    a
                   , Proxy 575
    -> Proxy 568 -> SWord 1024 -> SBV (WordN ((575 - 568) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 575
    forall k (t :: k). Proxy t
    Proxy  @575) (Proxy 568
    forall k (t :: k). Proxy t
    Proxy  @568) SWord 1024
    a, Proxy 567
    -> Proxy 560 -> SWord 1024 -> SBV (WordN ((567 - 560) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 567
    forall k (t :: k). Proxy t
    Proxy  @567) (Proxy 560
    forall k (t :: k). Proxy t
    Proxy  @560) SWord 1024
    a, Proxy 559
    -> Proxy 552 -> SWord 1024 -> SBV (WordN ((559 - 552) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 559
    forall k (t :: k). Proxy t
    Proxy  @559) (Proxy 552
    forall k (t :: k). Proxy t
    Proxy  @552) SWord 1024
    a, Proxy 551
    -> Proxy 544 -> SWord 1024 -> SBV (WordN ((551 - 544) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 551
    forall k (t :: k). Proxy t
    Proxy  @551) (Proxy 544
    forall k (t :: k). Proxy t
    Proxy  @544) SWord 1024
    a
                   , Proxy 543
    -> Proxy 536 -> SWord 1024 -> SBV (WordN ((543 - 536) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 543
    forall k (t :: k). Proxy t
    Proxy  @543) (Proxy 536
    forall k (t :: k). Proxy t
    Proxy  @536) SWord 1024
    a, Proxy 535
    -> Proxy 528 -> SWord 1024 -> SBV (WordN ((535 - 528) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 535
    forall k (t :: k). Proxy t
    Proxy  @535) (Proxy 528
    forall k (t :: k). Proxy t
    Proxy  @528) SWord 1024
    a, Proxy 527
    -> Proxy 520 -> SWord 1024 -> SBV (WordN ((527 - 520) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 527
    forall k (t :: k). Proxy t
    Proxy  @527) (Proxy 520
    forall k (t :: k). Proxy t
    Proxy  @520) SWord 1024
    a, Proxy 519
    -> Proxy 512 -> SWord 1024 -> SBV (WordN ((519 - 512) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 519
    forall k (t :: k). Proxy t
    Proxy  @519) (Proxy 512
    forall k (t :: k). Proxy t
    Proxy  @512) SWord 1024
    a
                   , Proxy 511
    -> Proxy 504 -> SWord 1024 -> SBV (WordN ((511 - 504) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 511
    forall k (t :: k). Proxy t
    Proxy  @511) (Proxy 504
    forall k (t :: k). Proxy t
    Proxy  @504) SWord 1024
    a, Proxy 503
    -> Proxy 496 -> SWord 1024 -> SBV (WordN ((503 - 496) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 503
    forall k (t :: k). Proxy t
    Proxy  @503) (Proxy 496
    forall k (t :: k). Proxy t
    Proxy  @496) SWord 1024
    a, Proxy 495
    -> Proxy 488 -> SWord 1024 -> SBV (WordN ((495 - 488) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 495
    forall k (t :: k). Proxy t
    Proxy  @495) (Proxy 488
    forall k (t :: k). Proxy t
    Proxy  @488) SWord 1024
    a, Proxy 487
    -> Proxy 480 -> SWord 1024 -> SBV (WordN ((487 - 480) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 487
    forall k (t :: k). Proxy t
    Proxy  @487) (Proxy 480
    forall k (t :: k). Proxy t
    Proxy  @480) SWord 1024
    a
                   , Proxy 479
    -> Proxy 472 -> SWord 1024 -> SBV (WordN ((479 - 472) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 479
    forall k (t :: k). Proxy t
    Proxy  @479) (Proxy 472
    forall k (t :: k). Proxy t
    Proxy  @472) SWord 1024
    a, Proxy 471
    -> Proxy 464 -> SWord 1024 -> SBV (WordN ((471 - 464) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 471
    forall k (t :: k). Proxy t
    Proxy  @471) (Proxy 464
    forall k (t :: k). Proxy t
    Proxy  @464) SWord 1024
    a, Proxy 463
    -> Proxy 456 -> SWord 1024 -> SBV (WordN ((463 - 456) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 463
    forall k (t :: k). Proxy t
    Proxy  @463) (Proxy 456
    forall k (t :: k). Proxy t
    Proxy  @456) SWord 1024
    a, Proxy 455
    -> Proxy 448 -> SWord 1024 -> SBV (WordN ((455 - 448) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 455
    forall k (t :: k). Proxy t
    Proxy  @455) (Proxy 448
    forall k (t :: k). Proxy t
    Proxy  @448) SWord 1024
    a
                   , Proxy 447
    -> Proxy 440 -> SWord 1024 -> SBV (WordN ((447 - 440) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 447
    forall k (t :: k). Proxy t
    Proxy  @447) (Proxy 440
    forall k (t :: k). Proxy t
    Proxy  @440) SWord 1024
    a, Proxy 439
    -> Proxy 432 -> SWord 1024 -> SBV (WordN ((439 - 432) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 439
    forall k (t :: k). Proxy t
    Proxy  @439) (Proxy 432
    forall k (t :: k). Proxy t
    Proxy  @432) SWord 1024
    a, Proxy 431
    -> Proxy 424 -> SWord 1024 -> SBV (WordN ((431 - 424) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 431
    forall k (t :: k). Proxy t
    Proxy  @431) (Proxy 424
    forall k (t :: k). Proxy t
    Proxy  @424) SWord 1024
    a, Proxy 423
    -> Proxy 416 -> SWord 1024 -> SBV (WordN ((423 - 416) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 423
    forall k (t :: k). Proxy t
    Proxy  @423) (Proxy 416
    forall k (t :: k). Proxy t
    Proxy  @416) SWord 1024
    a
                   , Proxy 415
    -> Proxy 408 -> SWord 1024 -> SBV (WordN ((415 - 408) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 415
    forall k (t :: k). Proxy t
    Proxy  @415) (Proxy 408
    forall k (t :: k). Proxy t
    Proxy  @408) SWord 1024
    a, Proxy 407
    -> Proxy 400 -> SWord 1024 -> SBV (WordN ((407 - 400) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 407
    forall k (t :: k). Proxy t
    Proxy  @407) (Proxy 400
    forall k (t :: k). Proxy t
    Proxy  @400) SWord 1024
    a, Proxy 399
    -> Proxy 392 -> SWord 1024 -> SBV (WordN ((399 - 392) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 399
    forall k (t :: k). Proxy t
    Proxy  @399) (Proxy 392
    forall k (t :: k). Proxy t
    Proxy  @392) SWord 1024
    a, Proxy 391
    -> Proxy 384 -> SWord 1024 -> SBV (WordN ((391 - 384) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 391
    forall k (t :: k). Proxy t
    Proxy  @391) (Proxy 384
    forall k (t :: k). Proxy t
    Proxy  @384) SWord 1024
    a
                   , Proxy 383
    -> Proxy 376 -> SWord 1024 -> SBV (WordN ((383 - 376) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 383
    forall k (t :: k). Proxy t
    Proxy  @383) (Proxy 376
    forall k (t :: k). Proxy t
    Proxy  @376) SWord 1024
    a, Proxy 375
    -> Proxy 368 -> SWord 1024 -> SBV (WordN ((375 - 368) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 375
    forall k (t :: k). Proxy t
    Proxy  @375) (Proxy 368
    forall k (t :: k). Proxy t
    Proxy  @368) SWord 1024
    a, Proxy 367
    -> Proxy 360 -> SWord 1024 -> SBV (WordN ((367 - 360) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 367
    forall k (t :: k). Proxy t
    Proxy  @367) (Proxy 360
    forall k (t :: k). Proxy t
    Proxy  @360) SWord 1024
    a, Proxy 359
    -> Proxy 352 -> SWord 1024 -> SBV (WordN ((359 - 352) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 359
    forall k (t :: k). Proxy t
    Proxy  @359) (Proxy 352
    forall k (t :: k). Proxy t
    Proxy  @352) SWord 1024
    a
                   , Proxy 351
    -> Proxy 344 -> SWord 1024 -> SBV (WordN ((351 - 344) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 351
    forall k (t :: k). Proxy t
    Proxy  @351) (Proxy 344
    forall k (t :: k). Proxy t
    Proxy  @344) SWord 1024
    a, Proxy 343
    -> Proxy 336 -> SWord 1024 -> SBV (WordN ((343 - 336) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 343
    forall k (t :: k). Proxy t
    Proxy  @343) (Proxy 336
    forall k (t :: k). Proxy t
    Proxy  @336) SWord 1024
    a, Proxy 335
    -> Proxy 328 -> SWord 1024 -> SBV (WordN ((335 - 328) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 335
    forall k (t :: k). Proxy t
    Proxy  @335) (Proxy 328
    forall k (t :: k). Proxy t
    Proxy  @328) SWord 1024
    a, Proxy 327
    -> Proxy 320 -> SWord 1024 -> SBV (WordN ((327 - 320) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 327
    forall k (t :: k). Proxy t
    Proxy  @327) (Proxy 320
    forall k (t :: k). Proxy t
    Proxy  @320) SWord 1024
    a
                   , Proxy 319
    -> Proxy 312 -> SWord 1024 -> SBV (WordN ((319 - 312) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 319
    forall k (t :: k). Proxy t
    Proxy  @319) (Proxy 312
    forall k (t :: k). Proxy t
    Proxy  @312) SWord 1024
    a, Proxy 311
    -> Proxy 304 -> SWord 1024 -> SBV (WordN ((311 - 304) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 311
    forall k (t :: k). Proxy t
    Proxy  @311) (Proxy 304
    forall k (t :: k). Proxy t
    Proxy  @304) SWord 1024
    a, Proxy 303
    -> Proxy 296 -> SWord 1024 -> SBV (WordN ((303 - 296) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 303
    forall k (t :: k). Proxy t
    Proxy  @303) (Proxy 296
    forall k (t :: k). Proxy t
    Proxy  @296) SWord 1024
    a, Proxy 295
    -> Proxy 288 -> SWord 1024 -> SBV (WordN ((295 - 288) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 295
    forall k (t :: k). Proxy t
    Proxy  @295) (Proxy 288
    forall k (t :: k). Proxy t
    Proxy  @288) SWord 1024
    a
                   , Proxy 287
    -> Proxy 280 -> SWord 1024 -> SBV (WordN ((287 - 280) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 287
    forall k (t :: k). Proxy t
    Proxy  @287) (Proxy 280
    forall k (t :: k). Proxy t
    Proxy  @280) SWord 1024
    a, Proxy 279
    -> Proxy 272 -> SWord 1024 -> SBV (WordN ((279 - 272) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 279
    forall k (t :: k). Proxy t
    Proxy  @279) (Proxy 272
    forall k (t :: k). Proxy t
    Proxy  @272) SWord 1024
    a, Proxy 271
    -> Proxy 264 -> SWord 1024 -> SBV (WordN ((271 - 264) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 271
    forall k (t :: k). Proxy t
    Proxy  @271) (Proxy 264
    forall k (t :: k). Proxy t
    Proxy  @264) SWord 1024
    a, Proxy 263
    -> Proxy 256 -> SWord 1024 -> SBV (WordN ((263 - 256) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 263
    forall k (t :: k). Proxy t
    Proxy  @263) (Proxy 256
    forall k (t :: k). Proxy t
    Proxy  @256) SWord 1024
    a
                   , Proxy 255
    -> Proxy 248 -> SWord 1024 -> SBV (WordN ((255 - 248) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 255
    forall k (t :: k). Proxy t
    Proxy  @255) (Proxy 248
    forall k (t :: k). Proxy t
    Proxy  @248) SWord 1024
    a, Proxy 247
    -> Proxy 240 -> SWord 1024 -> SBV (WordN ((247 - 240) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 247
    forall k (t :: k). Proxy t
    Proxy  @247) (Proxy 240
    forall k (t :: k). Proxy t
    Proxy  @240) SWord 1024
    a, Proxy 239
    -> Proxy 232 -> SWord 1024 -> SBV (WordN ((239 - 232) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 239
    forall k (t :: k). Proxy t
    Proxy  @239) (Proxy 232
    forall k (t :: k). Proxy t
    Proxy  @232) SWord 1024
    a, Proxy 231
    -> Proxy 224 -> SWord 1024 -> SBV (WordN ((231 - 224) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 231
    forall k (t :: k). Proxy t
    Proxy  @231) (Proxy 224
    forall k (t :: k). Proxy t
    Proxy  @224) SWord 1024
    a
                   , Proxy 223
    -> Proxy 216 -> SWord 1024 -> SBV (WordN ((223 - 216) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 223
    forall k (t :: k). Proxy t
    Proxy  @223) (Proxy 216
    forall k (t :: k). Proxy t
    Proxy  @216) SWord 1024
    a, Proxy 215
    -> Proxy 208 -> SWord 1024 -> SBV (WordN ((215 - 208) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 215
    forall k (t :: k). Proxy t
    Proxy  @215) (Proxy 208
    forall k (t :: k). Proxy t
    Proxy  @208) SWord 1024
    a, Proxy 207
    -> Proxy 200 -> SWord 1024 -> SBV (WordN ((207 - 200) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 207
    forall k (t :: k). Proxy t
    Proxy  @207) (Proxy 200
    forall k (t :: k). Proxy t
    Proxy  @200) SWord 1024
    a, Proxy 199
    -> Proxy 192 -> SWord 1024 -> SBV (WordN ((199 - 192) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 199
    forall k (t :: k). Proxy t
    Proxy  @199) (Proxy 192
    forall k (t :: k). Proxy t
    Proxy  @192) SWord 1024
    a
                   , Proxy 191
    -> Proxy 184 -> SWord 1024 -> SBV (WordN ((191 - 184) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 191
    forall k (t :: k). Proxy t
    Proxy  @191) (Proxy 184
    forall k (t :: k). Proxy t
    Proxy  @184) SWord 1024
    a, Proxy 183
    -> Proxy 176 -> SWord 1024 -> SBV (WordN ((183 - 176) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 183
    forall k (t :: k). Proxy t
    Proxy  @183) (Proxy 176
    forall k (t :: k). Proxy t
    Proxy  @176) SWord 1024
    a, Proxy 175
    -> Proxy 168 -> SWord 1024 -> SBV (WordN ((175 - 168) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 175
    forall k (t :: k). Proxy t
    Proxy  @175) (Proxy 168
    forall k (t :: k). Proxy t
    Proxy  @168) SWord 1024
    a, Proxy 167
    -> Proxy 160 -> SWord 1024 -> SBV (WordN ((167 - 160) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 167
    forall k (t :: k). Proxy t
    Proxy  @167) (Proxy 160
    forall k (t :: k). Proxy t
    Proxy  @160) SWord 1024
    a
                   , Proxy 159
    -> Proxy 152 -> SWord 1024 -> SBV (WordN ((159 - 152) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 159
    forall k (t :: k). Proxy t
    Proxy  @159) (Proxy 152
    forall k (t :: k). Proxy t
    Proxy  @152) SWord 1024
    a, Proxy 151
    -> Proxy 144 -> SWord 1024 -> SBV (WordN ((151 - 144) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 151
    forall k (t :: k). Proxy t
    Proxy  @151) (Proxy 144
    forall k (t :: k). Proxy t
    Proxy  @144) SWord 1024
    a, Proxy 143
    -> Proxy 136 -> SWord 1024 -> SBV (WordN ((143 - 136) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 143
    forall k (t :: k). Proxy t
    Proxy  @143) (Proxy 136
    forall k (t :: k). Proxy t
    Proxy  @136) SWord 1024
    a, Proxy 135
    -> Proxy 128 -> SWord 1024 -> SBV (WordN ((135 - 128) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 135
    forall k (t :: k). Proxy t
    Proxy  @135) (Proxy 128
    forall k (t :: k). Proxy t
    Proxy  @128) SWord 1024
    a
                   , Proxy 127
    -> Proxy 120 -> SWord 1024 -> SBV (WordN ((127 - 120) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 127
    forall k (t :: k). Proxy t
    Proxy  @127) (Proxy 120
    forall k (t :: k). Proxy t
    Proxy  @120) SWord 1024
    a, Proxy 119
    -> Proxy 112 -> SWord 1024 -> SBV (WordN ((119 - 112) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 119
    forall k (t :: k). Proxy t
    Proxy  @119) (Proxy 112
    forall k (t :: k). Proxy t
    Proxy  @112) SWord 1024
    a, Proxy 111
    -> Proxy 104 -> SWord 1024 -> SBV (WordN ((111 - 104) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 111
    forall k (t :: k). Proxy t
    Proxy  @111) (Proxy 104
    forall k (t :: k). Proxy t
    Proxy  @104) SWord 1024
    a, Proxy 103 -> Proxy 96 -> SWord 1024 -> SBV (WordN ((103 - 96) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 103
    forall k (t :: k). Proxy t
    Proxy  @103) (Proxy 96
    forall k (t :: k). Proxy t
    Proxy   @96) SWord 1024
    a
                   , Proxy 95 -> Proxy 88 -> SWord 1024 -> SBV (WordN ((95 - 88) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 95
    forall k (t :: k). Proxy t
    Proxy   @95) (Proxy 88
    forall k (t :: k). Proxy t
    Proxy   @88) SWord 1024
    a, Proxy 87 -> Proxy 80 -> SWord 1024 -> SBV (WordN ((87 - 80) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 87
    forall k (t :: k). Proxy t
    Proxy   @87) (Proxy 80
    forall k (t :: k). Proxy t
    Proxy   @80) SWord 1024
    a, Proxy 79 -> Proxy 72 -> SWord 1024 -> SBV (WordN ((79 - 72) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 79
    forall k (t :: k). Proxy t
    Proxy   @79) (Proxy 72
    forall k (t :: k). Proxy t
    Proxy   @72) SWord 1024
    a, Proxy 71 -> Proxy 64 -> SWord 1024 -> SBV (WordN ((71 - 64) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 71
    forall k (t :: k). Proxy t
    Proxy   @71) (Proxy 64
    forall k (t :: k). Proxy t
    Proxy   @64) SWord 1024
    a
                   , Proxy 63 -> Proxy 56 -> SWord 1024 -> SBV (WordN ((63 - 56) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 63
    forall k (t :: k). Proxy t
    Proxy   @63) (Proxy 56
    forall k (t :: k). Proxy t
    Proxy   @56) SWord 1024
    a, Proxy 55 -> Proxy 48 -> SWord 1024 -> SBV (WordN ((55 - 48) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 55
    forall k (t :: k). Proxy t
    Proxy   @55) (Proxy 48
    forall k (t :: k). Proxy t
    Proxy   @48) SWord 1024
    a, Proxy 47 -> Proxy 40 -> SWord 1024 -> SBV (WordN ((47 - 40) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 47
    forall k (t :: k). Proxy t
    Proxy   @47) (Proxy 40
    forall k (t :: k). Proxy t
    Proxy   @40) SWord 1024
    a, Proxy 39 -> Proxy 32 -> SWord 1024 -> SBV (WordN ((39 - 32) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 39
    forall k (t :: k). Proxy t
    Proxy   @39) (Proxy 32
    forall k (t :: k). Proxy t
    Proxy   @32) SWord 1024
    a
                   , Proxy 31 -> Proxy 24 -> SWord 1024 -> SBV (WordN ((31 - 24) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 31
    forall k (t :: k). Proxy t
    Proxy   @31) (Proxy 24
    forall k (t :: k). Proxy t
    Proxy   @24) SWord 1024
    a, Proxy 23 -> Proxy 16 -> SWord 1024 -> SBV (WordN ((23 - 16) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 23
    forall k (t :: k). Proxy t
    Proxy   @23) (Proxy 16
    forall k (t :: k). Proxy t
    Proxy   @16) SWord 1024
    a, Proxy 15 -> Proxy 8 -> SWord 1024 -> SBV (WordN ((15 - 8) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 15
    forall k (t :: k). Proxy t
    Proxy   @15) (Proxy 8
    forall k (t :: k). Proxy t
    Proxy    @8) SWord 1024
    a, Proxy 7 -> Proxy 0 -> SWord 1024 -> SBV (WordN ((7 - 0) + 1))
    forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
           (proxy :: Nat -> *).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
     (i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
    proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
    bvExtract (Proxy 7
    forall k (t :: k). Proxy t
    Proxy    @7) (Proxy 0
    forall k (t :: k). Proxy t
    Proxy    @0) SWord 1024
    a
                   ]

       fromBytes :: [SWord 8] -> SWord 1024
    fromBytes as :: [SWord 8]
    as
         | Int
    l Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 128
         = ([SWord 8] -> SWord 512
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes :: [SWord 8] -> SWord 512) (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    take 64 [SWord 8]
    as) SWord 512 -> SWord 512 -> SBV (WordN (512 + 512))
    forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
    (KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
     SymVal (bv m)) =>
    SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
    # [SWord 8] -> SWord 512
    forall a. ByteConverter a => [SWord 8] -> a
    fromBytes (Int -> [SWord 8] -> [SWord 8]
    forall a. Int -> [a] -> [a]
    drop 64 [SWord 8]
    as)
         | Bool
    True
         = String -> SWord 1024
    forall a. HasCallStack => String -> a
    error (String -> SWord 1024) -> String -> SWord 1024
    forall a b. (a -> b) -> a -> b
    $ "fromBytes:SWord 1024: Incorrect number of bytes: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l
         where l :: Int
    l = [SWord 8] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SWord 8]
    as