haskell - Haskell 中国剰余定理

Question

この関数が機能するためには、crtHasSolution が最初に true でなければならないことを理解しています。n が解決策になる可能性があることを証明するのに苦労しています。

N の条件は、0 以上で、すべての mod ベースの積である m より小さい必要があることを知っています。

crtHasSolution :: [Integer] -> [Integer] -> Bool
crtHasSolution as ms = length as > 0 &&
                       length ms > 0 &&
                       length as == length ms &&
                       all (>=0) as &&
                       all (>=2) ms &&
                       pairwise_coprime ms

-- Is a given number a solution to a CRT problem?
-- usage: crtIsSolution n as ms = ans
-- assures: ans == True, if crtHasSolution as ms == True and n is a solution
--          ans == False, otherwise

crtIsSolution :: Integer -> [Integer] -> [Integer] -> Bool
crtIsSolution n as ms = crtHasSolution as ms &&
                        n >= 0 &&
                        n < m
                        where m =

コード