Lines Matching refs:Plus
19 // A semiring is specified by two binary operations Plus and Times and
21 // Plus: associative, commutative, and has Zero as its identity.
22 // Times: associative and has identity One, distributes w.r.t. Plus, and
52 // --> Reverse(Plus(a, b)) = Plus(Reverse(a), Reverse(b))
61 // Idempotent: for all a: Plus(a, a) == a.
62 // Path Property: for all a, b: Plus(a, b) == a or Plus(a, b) == b.
86 // For all a,b,c: Times(c, Plus(a,b)) = Plus(Times(c,a), Times(c, b))
89 // For all a,b,c: Times(Plus(a,b), c) = Plus(Times(a,c), Times(b, c))
97 // For all a: Plus(a, a) = a
100 // For all a,b: Plus(a,b) = a or Plus(a,b) = b
133 return (Plus(w1, w2) == w1) && w1 != w2;
