ByteString.hs.hquals

// for unfoldrN 
qualif PLenNat(v:GHC.Ptr.Ptr a)              : (0 <= plen v)

// for UnpackFoldrINLINED
qualif UnpackFoldrINLINED(v:List a, n:int, acc:List a): (len v = n + 1 + (len acc))

// for ByteString.inits
qualif BLenGt(v:Data.ByteString.Internal.ByteString, n:int): ((bLength v) > n)

// for ByteString.concat
qualif BLens(v:List Data.ByteString.Internal.ByteString) : 
  (0 <= bLengths v)

qualif BLenLE(v:GHC.Ptr.Ptr a, bs:List Data.ByteString.Internal.ByteString):
  (bLengths bs <= plen v) 

// for ByteString.splitWith
qualif SplitWith(v:List Data.ByteString.Internal.ByteString, l:int):
  ((bLengths v) + (len v) - 1 = l)

// for ByteString.unfoldrN
qualif PtrDiff(v:int, i:int, p:GHC.Ptr.Ptr a): 
  (i - v <= plen p)


// for ByteString.split
qualif BSValidOff(v:int,l:int,p:GHC.ForeignPtr.ForeignPtr a): 
  (v + l <= fplen p) 

qualif SplitLoop(v:List Data.ByteString.Internal.ByteString, l:int, n:int): 
  ((bLengths v) + (len v) - 1 = l - n)