Lines Matching refs:Plus
21 // A semiring is specified by two binary operations Plus and Times and
23 // Plus: associative, commutative, and has Zero as its identity.
24 // Times: associative and has identity One, distributes w.r.t. Plus, and
59 // --> Reverse(Plus(a, b)) = Plus(Reverse(a), Reverse(b))
68 // Idempotent: for all a: Plus(a, a) == a.
69 // Path Property: for all a, b: Plus(a, b) == a or Plus(a, b) == b.
94 // For all a,b,c: Times(c, Plus(a,b)) = Plus(Times(c,a), Times(c, b))
97 // For all a,b,c: Times(Plus(a,b), c) = Plus(Times(a,c), Times(b, c))
105 // For all a: Plus(a, a) = a
108 // For all a,b: Plus(a,b) = a or Plus(a,b) = b
122 // idempotent. It is trivially monotonic for plus. It is left
143 return (Plus(w1, w2) == w1) && w1 != w2;
