a more abstract characterisation in the setting of semirings. Formally, a domain semiring is a semiring S extended by a domain operation d : S → S which, for all x, y ∈ S, satisfies the axioms x ≤ d(x)x, d(xy) = d(xd(y)), d(x) ≤ 1, d(0) = 0, d(x + y) = d(x) + d(y). Domain semirings are automatically idempotent. This justifies the inequality signs in the axioms. The elements of d(S) are called domain elements. The domain axioms hold on all models discussed; their irredundancy can easily be verified with automated tools [8]. A notion of codomain is dual with respect to semiring opposition. It can be obtained from the domain axioms by swapping the order of multiplication. Many natural laws follow from the axioms, e.g., domain is isotone and domain elements are least left invariants, i.e., x = px ⇔ d(x) ≤ p holds for all x ∈ S and p ∈ d(S), hence d(x) = inf(p ∈ d(S) : x = px). This seems to be a central property: multiplying an element at the left by its domain element...