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)