Axiomatizing the identities of binoid languages

We present a nontrivial axiomatization for the equational theory of binoid languages, the subsets of a free binoid. In doing so, we prove that a conjecture given in our previous paper was true: the identical laws of ordinary (string) languages, written separately using ‘horizontal’ and ‘vertical’ operation symbols form a required complete system of axioms.