Lines Matching refs:NonNegative
24 $ \(Positive m) (NonNegative a) -> modF2m m a == modF2m m (modF2m m a)
26 $ \(Positive m) (NonNegative a) -> modF2m m a < 2 ^ log2 m
30 $ \(Positive m) (NonNegative a) -> modF2m m a >= 0
34 $ \(Positive m) (NonNegative a) (NonNegative b)
40 $ \(Positive m) (NonNegative a) (NonNegative b) -> mulF2m m a b == mulF2m m b a
42 $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
45 $ \(Positive m) (NonNegative a) -> mulF2m m a 1 == modF2m m a
47 $ \(Positive m) (NonNegative a) -> mulF2m m a 0 == 0
49 $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
55 $ \(Positive m) (NonNegative a) -> mulF2m m a a == squareF2m m a
68 $ \(Positive m) (NonNegative a) -> powF2m m a 2 == squareF2m m a
70 $ \(Positive m) (NonNegative a) -> powF2m m a 1 == modF2m m a
72 $ \(Positive m) (NonNegative a) -> powF2m m a 0 == modF2m m 1
74 $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
77 $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
80 $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
86 $ \(Positive m) (NonNegative a)
89 $ \(NonNegative a) -> a < 2 || invF2m (squareF2m' a `addF2m` 1) a == Just a
94 $ \(Positive m) (NonNegative a) -> divF2m m 1 a == invF2m m a
96 $ \(Positive m) (NonNegative a) (NonNegative b)
99 $ \(Positive m) (NonNegative a) (NonNegative b)