Lines Matching refs:NonNegative
23 $ \(Positive m) (NonNegative a) -> modF2m m a == modF2m m (modF2m m a)
25 $ \(Positive m) (NonNegative a) -> modF2m m a < 2 ^ log2 m
29 $ \(Positive m) (NonNegative a) -> modF2m m a >= 0
33 $ \(Positive m) (NonNegative a) (NonNegative b)
39 $ \(Positive m) (NonNegative a) (NonNegative b) -> mulF2m m a b == mulF2m m b a
41 $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
44 $ \(Positive m) (NonNegative a) -> mulF2m m a 1 == modF2m m a
46 $ \(Positive m) (NonNegative a) -> mulF2m m a 0 == 0
48 $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
54 $ \(Positive m) (NonNegative a) -> mulF2m m a a == squareF2m m a
59 $ \(Positive m) (NonNegative a)
62 $ \(NonNegative a) -> a < 2 || invF2m (squareF2m' a `addF2m` 1) a == Just a
67 $ \(Positive m) (NonNegative a) -> divF2m m 1 a == invF2m m a
69 $ \(Positive m) (NonNegative a) (NonNegative b)
72 $ \(Positive m) (NonNegative a) (NonNegative b)